(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(* This contribution was updated for Coq V5.10 by the COQ workgroup.        *)
(* January 1995                                                             *)
(****************************************************************************)
(*                           Relations_3_facts.v                            *)
(****************************************************************************)

Require Import Relations_1.
Require Import Relations_2.
Require Import Relations_3.
Require Import Relations_2_facts.

Theorem Rstar_imp_coherent :
 forall (U : Type) (R : Relation U) (x y : U),
 Rstar U R x y -> coherent U R x y.
(* Goal: forall (U : Type) (R : Relation U) (x y : U) (_ : Rstar U R x y), coherent U R x y *)
intros U R x y H'; red in |- *.
(* Goal: @ex U (fun z : U => and (Rstar U R x z) (Rstar U R y z)) *)
exists y; auto.
Qed.
Hint Resolve Rstar_imp_coherent.

Theorem coherent_symmetric :
 forall (U : Type) (R : Relation U), Symmetric U (coherent U R).
(* Goal: forall _ : Rstar U R x b, coherent U R a b *)
unfold coherent at 1 in |- *.
(* Goal: forall (U : Type) (R : Relation U), Symmetric U (fun x y : U => @ex U (fun z : U => and (Rstar U R x z) (Rstar U R y z))) *)
intros U R; red in |- *.
(* Goal: forall (x y : U) (_ : @ex U (fun z : U => and (Rstar U R x z) (Rstar U R y z))), @ex U (fun z : U => and (Rstar U R y z) (Rstar U R x z)) *)
intros x y h; elim h; intros z h0; elim h0; intros H' H'0; clear h h0.
(* Goal: @ex U (fun z : U => and (Rstar U R y z) (Rstar U R x z)) *)
exists z; auto.
Qed.

Theorem Strong_confluence :
 forall (U : Type) (R : Relation U), Strongly_confluent U R -> Confluent U R.
(* Goal: forall (U : Type) (R : Relation U) (_ : Strongly_confluent U R), Confluent U R *)
intros U R H'; red in |- *.
(* Goal: forall x : U, confluent U R x *)
intro x; red in |- *; intros a b H'0.
(* Goal: forall _ : Rstar U R x b, coherent U R a b *)
unfold coherent at 1 in |- *.
(* Goal: forall _ : Rstar U R x b, @ex U (fun z : U => and (Rstar U R a z) (Rstar U R b z)) *)
generalize b; clear b.
(* Goal: forall (b : U) (_ : Rstar U R x b), @ex U (fun z : U => and (Rstar U R a z) (Rstar U R b z)) *)
elim H'0; clear H'0.
(* Goal: forall (x b : U) (_ : Rstar U R x b), @ex U (fun z : U => and (Rstar U R x z) (Rstar U R b z)) *)
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : forall (b : U) (_ : Rstar U R y b), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0))) (b : U) (_ : Rstar U R x b), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0)) *)
intros x0 b H'1; exists b; auto.
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : forall (b : U) (_ : Rstar U R y b), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0))) (b : U) (_ : Rstar U R x b), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0)) *)
intros x0 y z H'1 H'2 H'3 b H'4.
generalize (Lemma1 U R); intro h; lapply h;
 [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0;
    [ intro H'5; generalize (H'5 y); intro h1; lapply h1;
       [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7;
          clear h h0 h1 h2 h3
       | clear h h0 h1 ]
    | clear h h0 ]
 | clear h ]; auto.
generalize (H'3 z0); intro h; lapply h;
 [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1
 | clear h ]; auto.
(* Goal: @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0)) *)
exists z1; split; auto.
(* Goal: Rstar U R b z1 *)
apply Rstar_n with z0; auto.
Qed.

Theorem Strong_confluence_direct :
 forall (U : Type) (R : Relation U), Strongly_confluent U R -> Confluent U R.
(* Goal: forall (U : Type) (R : Relation U) (_ : Strongly_confluent U R), Confluent U R *)
intros U R H'; red in |- *.
(* Goal: forall x : U, confluent U R x *)
intro x; red in |- *; intros a b H'0.
(* Goal: forall _ : Rstar U R x b, coherent U R a b *)
unfold coherent at 1 in |- *.
(* Goal: forall _ : Rstar U R x b, @ex U (fun z : U => and (Rstar U R a z) (Rstar U R b z)) *)
generalize b; clear b.
(* Goal: forall (b : U) (_ : Rstar U R x b), @ex U (fun z : U => and (Rstar U R a z) (Rstar U R b z)) *)
elim H'0; clear H'0.
(* Goal: forall (x b : U) (_ : Rstar U R x b), @ex U (fun z : U => and (Rstar U R x z) (Rstar U R b z)) *)
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : forall (b : U) (_ : Rstar U R y b), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0))) (b : U) (_ : Rstar U R x b), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0)) *)
intros x0 b H'1; exists b; auto.
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : forall (b : U) (_ : Rstar U R y b), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0))) (b : U) (_ : Rstar U R x b), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0)) *)
intros x0 y z H'1 H'2 H'3 b H'4.
(* Goal: @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0)) *)
cut (exists t : U, Rstar U R y t /\ R b t).
(* Goal: forall _ : @ex U (fun t : U => and (Rstar U R y t) (R b t)), @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0)) *)
(* Goal: @ex U (fun t : U => and (Rstar U R y t) (R b t)) *)
intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0.
generalize (H'3 t); intro h; lapply h;
 [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1
 | clear h ]; auto.
(* Goal: @ex U (fun z0 : U => and (Rstar U R z z0) (Rstar U R b z0)) *)
(* Goal: @ex U (fun t : U => and (Rstar U R y t) (R b t)) *)
exists z0; split; [ assumption | idtac ].
(* Goal: Rstar U R b z0 *)
(* Goal: @ex U (fun t : U => and (Rstar U R y t) (R b t)) *)
apply Rstar_n with t; auto.
(* Goal: @ex U (fun t : U => and (Rstar U R y t) (R b t)) *)
generalize H'1; generalize y; clear H'1.
(* Goal: forall (y : U) (_ : R x0 y), @ex U (fun t : U => and (Rstar U R y t) (R b t)) *)
elim H'4.
(* Goal: forall (x y : U) (_ : R x y), @ex U (fun t : U => and (Rstar U R y t) (R x t)) *)
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : forall (y0 : U) (_ : R y y0), @ex U (fun t : U => and (Rstar U R y0 t) (R z t))) (y0 : U) (_ : R x y0), @ex U (fun t : U => and (Rstar U R y0 t) (R z t)) *)
intros x1 y0 H'0; exists y0; auto.
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : forall (y0 : U) (_ : R y y0), @ex U (fun t : U => and (Rstar U R y0 t) (R z t))) (y0 : U) (_ : R x y0), @ex U (fun t : U => and (Rstar U R y0 t) (R z t)) *)
intros x1 y0 z0 H'0 H'1 H'5 y1 H'6.
(* Goal: @ex U (fun t : U => and (Rstar U R y1 t) (R z0 t)) *)
red in H'.
generalize (H' x1 y0 y1); intro h; lapply h;
 [ intro H'7; lapply H'7;
    [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9;
       clear h H'7 h0 h1
    | clear h ]
 | clear h ]; auto.
generalize (H'5 z1); intro h; lapply h;
 [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1
 | clear h ]; auto.
(* Goal: @ex U (fun t : U => and (Rstar U R y1 t) (R z0 t)) *)
exists t; split; auto.
(* Goal: Rstar U R y1 t *)
apply Rstar_n with z1; auto.
Qed.
(* Warming up *)

Theorem Noetherian_contains_Noetherian :
 forall (U : Type) (R R' : Relation U),
 Noetherian U R -> contains U R R' -> Noetherian U R'.
(* Goal: forall (U : Type) (R R' : Relation U) (_ : Noetherian U R) (_ : contains U R R'), Noetherian U R' *)
unfold Noetherian in |- *.
(* Goal: forall (U : Type) (R R' : Relation U) (_ : forall x : U, noetherian U R x) (_ : contains U R R') (x : U), noetherian U R' x *)
intros U R R' H' H'0 x.
(* Goal: noetherian U R' x *)
elim (H' x); auto.
Qed.

Theorem Newman :
 forall (U : Type) (R : Relation U),
 Noetherian U R -> Locally_confluent U R -> Confluent U R.
(* Goal: forall (U : Type) (R : Relation U) (_ : Noetherian U R) (_ : Locally_confluent U R), Confluent U R *)
intros U R H' H'0; red in |- *; intro x.
(* Goal: confluent U R x *)
elim (H' x); unfold confluent in |- *.
(* Goal: forall (x : U) (_ : forall (y : U) (_ : R x y), noetherian U R y) (_ : forall (y : U) (_ : R x y) (y0 z : U) (_ : Rstar U R y y0) (_ : Rstar U R y z), coherent U R y0 z) (y z : U) (_ : Rstar U R x y) (_ : Rstar U R x z), coherent U R y z *)
intros x0 H'1 H'2 y z H'3 H'4.
generalize (Rstar_cases U R x0 y); intro h; lapply h;
 [ intro h0; elim h0;
    [ clear h h0; intro h1
    | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6;
       clear h h0 h1 h2 ]
 | clear h ]; auto.
(* Goal: coherent U R y z *)
(* Goal: coherent U R y z *)
elim h1; auto.
generalize (Rstar_cases U R x0 z); intro h; lapply h;
 [ intro h0; elim h0;
    [ clear h h0; intro h1
    | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8;
       clear h h0 h1 h2 ]
 | clear h ]; auto.
(* Goal: coherent U R y z *)
(* Goal: coherent U R y z *)
elim h1; generalize coherent_symmetric; intro t; red in t; auto.
(* Goal: coherent U R y z *)
unfold Locally_confluent, locally_confluent, coherent in H'0.
generalize (H'0 x0 u v); intro h; lapply h;
 [ intro H'9; lapply H'9;
    [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11;
       clear h H'9 h0 h1
    | clear h ]
 | clear h ]; auto.
(* Goal: coherent U R y z *)
clear H'0.
(* Goal: coherent U R y z *)
unfold coherent at 1 in H'2.
generalize (H'2 u); intro h; lapply h;
 [ intro H'0; generalize (H'0 y t); intro h0; lapply h0;
    [ intro H'9; lapply H'9;
       [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13;
          clear h h0 H'9 h1 h2
       | clear h h0 ]
    | clear h h0 ]
 | clear h ]; auto.
(* Goal: coherent U R y z *)
generalize Rstar_transitive; intro T; red in T.
generalize (H'2 v); intro h; lapply h;
 [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0;
    [ intro H'14; lapply H'14;
       [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16;
          clear h h0 H'14 h1 h2
       | clear h h0 ]
    | clear h h0 ]
 | clear h ]; auto.
(* Goal: coherent U R y z *)
(* Goal: Rstar U R v y1 *)
red in |- *; (exists z1; split); auto.
(* Goal: Rstar U R y z1 *)
(* Goal: Rstar U R v y1 *)
apply T with y1; auto.
(* Goal: Rstar U R v y1 *)
apply T with t; auto.
Qed.
