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

Question

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

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

One-many relations may be defined as relations such that, if x has the relation in question to y, there is no other term x' which also has the relation to y.

Or, again, they may be defined as follows: Given two terms x and x', the terms to which x has the given relation and those to which x' has it have no member in common.

Or, again, they may be defined as relations such that the relative product of one of them and its converse implies identity, where the “relative product” of two relations R and S is that relation which holds between x and z when there is an intermediate term y, such that x has the relation R to y and y has the relation S to 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 , 很容易提前证明。

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

Answer 1

我认为您误译了第三个定义。原文说:

Or, again, they may be defined as relations such that the relative product of one of them and its converse implies identity

(强调我的)。这将翻译为:

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

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