半合流が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に相当）での定理を証明するのが少し簡単だと思います。 2つのケースがあります：反射的ケースと実際に "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.