Coq：关系组合的关联性

Question

我正在研究基于关系代数的系统验证。我发现 D. Pous 的关系代数库在 Coq 社区很受欢迎。

https://github.com/damien-pous/relation-algebra

在此页面上，二元关系 hrel 与其关系组合 hrel_dot 一起定义。

http://perso.ens-lyon.fr/damien.pous/ra/html/RelationAlgebra.rel.html

在此库中，二元关系定义为

Universe U.
Definition hrel (n m: Type@{U}) := n -> m -> Prop.

而两个二元关系的关系组合定义为

Definition hrel_dot n m p (x: hrel n m) (y: hrel m p): hrel n p :=
  fun i j => exists2 k, x i k & y k j.

我相信关系组合是关联的，即

Lemma dot_assoc:
  forall m n p q (x: hrel m n) (y: hrel n p) (z: hrel p q),
  hrel_dot m p q (hrel_dot m n p x y) z = hrel_dot m n q x (hrel_dot n p q y z).

我已经到了我认为表达式的 LHS 和 RHS 等效的地方，但我对接下来的步骤一无所知。

______________________________________(1/1)
(exists2 k : p,
   exists2 k0 : n, x x0 k0 & y k0 k & z k x1) =
(exists2 k : n,
   x x0 k & exists2 k0 : p, y k k0 & z k0 x1)

我不知道如何推理嵌套 exists2，尽管通过交换变量 k 和 k0.

结果看起来很简单

提前致谢！

Answer 1

正如 Ana 所指出的，不假设额外的公理就不可能证明这个等式。一种可能性是使用功能和命题的外延性：

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.PropExtensionality.

Universe U.
Definition hrel (n m: Type@{U}) := n -> m -> Prop.

Definition hrel_dot n m p (x: hrel n m) (y: hrel m p): hrel n p :=
  fun i j => exists2 k, x i k & y k j.

Lemma dot_assoc:
  forall m n p q (x: hrel m n) (y: hrel n p) (z: hrel p q),
  hrel_dot m p q (hrel_dot m n p x y) z = hrel_dot m n q x (hrel_dot n p q y z).
Proof.
intros m n p q x y z.
apply functional_extensionality. intros a.
apply functional_extensionality. intros b.
apply propositional_extensionality.
unfold hrel_dot; split.
- intros [c [d ? ?] ?]. eauto.
- intros [c ? [d ? ?]]. eauto.
Qed.

Coq：关系组合的关联性

Coq: Associativity of relational composition

functional-programming

coq

algebra

formal-verification

formal-methods