Coq：关系组合的关联性答案

【问题标题】：Coq: Associativity of relational compositionCoq：关系组合的关联性
【发布时间】：2022-01-19 10:14:11
【问题描述】：

我正在验证基于关系代数的系统。我发现 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 看起来很简单。

提前致谢！

【问题讨论】：

我不确定您是否可以证明这两个表达式的 相等性，至少在没有证明不相关的情况下不能证明。如果您将目标重写为逻辑等价，事情应该会更容易。
二元关系代数不是关系代数。

标签： functional-programming coq algebra formal-verification formal-methods

【解决方案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.

【讨论】：