如何描述 Coq 中的一对多关系？

Posted 2023-05-08

【中文标题】如何描述 Coq 中的一对多关系？

【英文标题】：How to describe the one-many relations in Coq?

【发布时间】：2014-10-18 03:04:28

【问题描述】：

我正在阅读 B.Russell 的《数学哲学导论》一书，并试图将其中描述的所有定理形式化。

一对多关系由以下文本描述（contexts on book）。

一对多关系可以定义为这样的关系，如果 x 有 与 y 的关系，没有其他项 x' 也具有 与 y 的关系。

或者，同样，它们可以定义如下：给定 两个项 x 和 x'，与 x 具有给定关系的项和 x' 所拥有的那些没有共同的成员。

或者，再次，他们可能 被定义为这样的关系，使得其中一个的相对乘积 反之则意味着同一性，其中两个的“相对乘积” 关系 R 和 S 是在 x 和 z 之间成立的关系，当 有一个中间项 y，使得 x 与 y 有关系 并且 y 具有 S 与 z 的关系。

它提出了三种定义方式。我已经成功地描述了前两个并证明了它们的等价性。当我被困在第三个时，我试图摆脱“相对产品”的概念，直接进入它的内涵，但也失败了。

以下是我的定义，我犯了什么错误吗？

Definition one_many X (R : relation X) : Prop :=
  forall x y, R x y -> forall x', x <> x' -> ~(R x' y).

Definition one_many' X (R : relation X) : Prop :=
  forall x x' y, R x y -> R x' y -> x = x'.

Inductive relative_product
          X (R: relation X) (S: relation X) : relation X :=
  | rp0 : forall x y, forall z, R x y -> S y z -> relative_product R S x z.
Inductive converse X (R : relation X) : relation X :=
  | cv0 : forall x y, R x y -> converse R y x.
Inductive id X : relation X :=
  | id0 : forall x, id x x.

Definition one_many'' X (R : relation X) : Prop :=
  forall x y, relative_product R (converse R) x y <-> id x y.

以下是我对第三个定义的解释，我也未能证明它们的等价性。

Goal forall X (R : relation X),
    one_many'' R <-> (forall x y, R x y -> forall x', converse R y x' -> x = x').
Proof.
  intros. unfold one_many''. split.

  intros.
  assert (relative_product R (converse R) x x' <-> id x x'). apply H.
  inversion H2. apply id_eqv. apply H3.
  apply rp0 with y. assumption. assumption.

  intros.
  split. intro.
  inversion H0. subst.
  apply id_eqv. apply H with y0.
  assumption. assumption.

   (* I'm stuck here. This subgoal is obviously not provable. *)

其中的证明id_eqv是Lemma id_eqv : forall X (x:X) (y:X), x = y <-> id x y，容易提前证明。

有人可以帮我找出或提示我哪里出错了吗？提前致谢。

【问题讨论】：

你如何定义relation？你能分享你的其余定义吗？

sinan：relation直接取自标准库Relationship，即Definition relation (X:Type) := X -> X -> Prop。

id_eqv 是否也在 stdlib 中定义？我无法找到所需的定义。

思南：对不起，我错过了。我自己证明了id_eqv。 Lemma id_eqv : forall X (x:X) (y:X), x = y <-> id x y.

在逆关系的定义中是否需要R x y <-> converse R y x，或者根据该定义是否容易证明converse R y x -> R x y？

【参考方案1】：

我认为你误译了第三个定义。原文说：

或者，再一次，它们可以被定义为这样的关系，使得其中一个的相对乘积及其逆暗示同一性

（强调我的）。这将翻译为：

forall x y, relative_product R (converse R) x y -> id x y

也就是说，它应该是一个直接的暗示，而不是你断言的等价。您不能希望从其他任何一个中证明您的第三个陈述，因为它不等价：考虑非空集合上的空关系。这当然是一对多的关系，但其逆的相对乘积也是空的，所以不是完整的恒等关系。

【参考方案2】：

猜测，但您可能需要 R 是自反或不为空。使用你的脚本我最终不得不证明

1 subgoal
X : Type
R : relation X
H : forall x y : X, R x y -> forall x' : X, converse R y x' -> x = x'
y : X
______________________________________(1/1)
relative_product R (converse R) y y

所以你有一个关系R，和一个居民y:X。为了证明你的目标，你需要有一个见证人z，比如R y z 和R z y。没有任何其他信息，我想你唯一的机会是让R 具有自反性，z 成为y。