如何证明半合流意味着Coq中的汇合？

Question

我使用Coq.Relations提供的定义，我有以下定义：

Definition joinable (x:A) (y:A) : Prop :=
  exists z, (clos_refl_trans A R x z) /\ (clos_refl_trans A R y z).

Notation "X ↓ Y" := (joinable X Y) (at level 70, right associativity).
Notation "X → Y" := (R X Y) (at level 75, right associativity).
Notation "X →* Y" := (clos_refl_trans A R X Y) (at level 75, right associativity).
Notation "X ⇆ Y" := (clos_refl_sym_trans A R X Y) (at level 75, right associativity).

Definition confluent : Prop := forall x y1 y2, (x →* y1 /\ x →* y2) -> (y1↓y2).
Definition semi_confluent : Prop := forall x y1 y2, (x → y1 /\ x →* y2) -> (y1↓y2).

以下是我所拥有的：

Theorem semi_confluent_confluent : semi_confluent -> confluent.
Proof.
  unfold confluent, semi_confluent, joinable.
  intros. destruct H0. induction H0.
  - apply H with (x := x). split. auto. auto.
  - exists y2. split. auto. auto.
  - admit.
Admitted.

我试着用归纳的方法：

• H0 :X→* y1

但我似乎还停留在最后一种情况(传递性)上。对于最后一种情况，我尝试了几种方法，比如在(x→* z)上进行归纳，但是它似乎让我找到了一条无法证明的语句。

Answer 1

我认为用归纳法证明clos_refl_trans_1n关系的定理要容易一些(它等价于clos_refl_trans)。因为它给了我们两种情况:自反情形和我们实际上“制造一个R-step”的情况，我们可以很容易地使用半合流性质，它需要一个R-step。

我稍微修改了confluent和semi_confluent的定义，以避免与连接相关的包装/解包。这不会影响任何事情，因为结果在逻辑上等同于原始结果。

我还要指出，正如在许多情况下一样，我们需要在进行归纳之前概括一下我们的发言。

Definition confluent : Prop := forall x y1 y2, x →* y1 -> x →* y2 -> (y1↓y2).
Definition semi_confluent : Prop := forall x y1 y2, x → y1 -> x →* y2 -> (y1↓y2).

Hint Constructors clos_refl_trans.

Theorem semi_confluent_confluent : semi_confluent -> confluent.
Proof.
  intros Hsemi x y1 y2 Hxy1 Hxy2.
  unfold semi_confluent, joinable in *.
  generalize dependent y2.
  induction (clos_rt_rt1n _ _ _ _ Hxy1) as [| x y1' y1 HRxy1' Hy1'y1 IH]; intros y2 Hxy2.
  - now exists y2.
  - apply clos_rt1n_rt in Hy1'y1.
    specialize (Hsemi x y1' y2 HRxy1' Hxy2) as (z & Hy1'z & Hy2z).
    specialize (IH Hy1'y1 z Hy1'z) as (w & Hy1w & Hzw).
    exists w.
    split; auto.
    now apply rt_trans with (y := z).
Qed.