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

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

Require Import Relations_1.
Require Import Relations_2.

Theorem Rstar_reflexive :
 forall (U : Type) (R : Relation U), Reflexive U (Rstar U R).
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
auto.
Qed.

Theorem Rplus_contains_R :
 forall (U : Type) (R : Relation U), contains U (Rplus U R) R.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
auto.
Qed.

Theorem Rstar_contains_R :
 forall (U : Type) (R : Relation U), contains U (Rstar U R) R.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros U R; red in |- *; intros x y H'; apply Rstar_n with y; auto.
Qed.

Theorem Rstar_contains_Rplus :
 forall (U : Type) (R : Relation U), contains U (Rstar U R) (Rplus U R).
(* Goal: forall (U : Type) (R : Relation U), Transitive U (Rstar U R) *)
intros U R; red in |- *.
(* Goal: forall (x y : U) (_ : Rplus U R x y), Rstar U R x y *)
intros x y H'; elim H'.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
generalize Rstar_contains_R; intro T; red in T; auto.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto.
Qed.

Theorem Rstar_transitive :
 forall (U : Type) (R : Relation U), Transitive U (Rstar U R).
(* Goal: forall (U : Type) (R : Relation U), Transitive U (Rstar U R) *)
intros U R; red in |- *.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x y z H'; elim H'; auto.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto.
Qed.

Theorem Rstar_cases :
 forall (U : Type) (R : Relation U) (x y : U),
 Rstar U R x y -> x = y :>U \/ (exists u : U, R x u /\ Rstar U R u y).
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros U R x y H'; elim H'; auto.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto.
Qed.

Theorem Rstar_equiv_Rstar1 :
 forall (U : Type) (R : Relation U), same_relation U (Rstar U R) (Rstar1 U R).
(* Goal: forall (U : Type) (R : Relation U), same_relation U (Rstar U R) (Rstar1 U R) *)
generalize Rstar_contains_R; intro T; red in T.
(* Goal: forall (U : Type) (R : Relation U), same_relation U (Rstar U R) (Rstar1 U R) *)
intros U R; unfold same_relation, contains in |- *.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
split; intros x y H'; elim H'; auto.
(* Goal: forall (U : Type) (R : Relation U) (x y z : U) (_ : Rstar U R x y) (_ : Rplus U R y z), @ex U (fun u : U => and (R x u) (Rstar U R u z)) *)
generalize Rstar_transitive; intro T1; red in T1.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto.
Qed.

Theorem Rsym_imp_Rstarsym :
 forall (U : Type) (R : Relation U), Symmetric U R -> Symmetric U (Rstar U R).
(* Goal: forall (U : Type) (R : Relation U) (_ : Symmetric U R), Symmetric U (Rstar U R) *)
intros U R H'; red in |- *.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x y H'0; elim H'0; auto.
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : Rstar U R z y), Rstar U R z x *)
intros x0 y0 z H'1 H'2 H'3.
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : Rstar U S y z), Rstar U S x z *)
generalize Rstar_transitive; intro T; red in T.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
apply T with y0; auto.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
apply Rstar_n with x0; auto.
Qed.

Theorem Sstar_contains_Rstar :
 forall (U : Type) (R S : Relation U),
 contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R).
(* Goal: forall (U : Type) (R S : Relation U) (_ : contains U (Rstar U S) R), contains U (Rstar U S) (Rstar U R) *)
unfold contains in |- *.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros U R S H' x y H'0; elim H'0; auto.
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : Rstar U S y z), Rstar U S x z *)
generalize Rstar_transitive; intro T; red in T.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x0 y0 z H'1 H'2 H'3; apply T with y0; auto.
Qed.

Theorem star_monotone :
 forall (U : Type) (R S : Relation U),
 contains U S R -> contains U (Rstar U S) (Rstar U R).
(* Goal: forall (U : Type) (R S : Relation U) (_ : contains U S R), contains U (Rstar U S) (Rstar U R) *)
intros U R S H'.
(* Goal: contains U (Rstar U S) (Rstar U R) *)
apply Sstar_contains_Rstar.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
generalize (Rstar_contains_R U S); auto.
Qed.

Theorem RstarRplus_RRstar :
 forall (U : Type) (R : Relation U) (x y z : U),
 Rstar U R x y -> Rplus U R y z -> exists u : U, R x u /\ Rstar U R u z.
(* Goal: forall (U : Type) (R : Relation U) (x y z : U) (_ : Rstar U R x y) (_ : Rplus U R y z), @ex U (fun u : U => and (R x u) (Rstar U R u z)) *)
generalize Rstar_contains_Rplus; intro T; red in T.
(* Goal: forall (U : Type) (R : Relation U) (x y z : U) (_ : Rstar U R x y) (_ : Rplus U R y z), @ex U (fun u : U => and (R x u) (Rstar U R u z)) *)
generalize Rstar_transitive; intro T1; red in T1.
(* Goal: forall (U : Type) (R : Relation U) (x y z : U) (_ : Rstar U R x y) (_ : Rplus U R y z), @ex U (fun u : U => and (R x u) (Rstar U R u z)) *)
intros U R x y z H'; elim H'.
(* Goal: forall (x : U) (_ : Rplus U R x z), @ex U (fun u : U => and (R x u) (Rstar U R u z)) *)
(* Goal: forall (x y z0 : U) (_ : R x y) (_ : Rstar U R y z0) (_ : forall _ : Rplus U R z0 z, @ex U (fun u : U => and (R y u) (Rstar U R u z))) (_ : Rplus U R z0 z), @ex U (fun u : U => and (R x u) (Rstar U R u z)) *)
intros x0 H'0; elim H'0.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros; exists y0; auto.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros; exists y0; auto.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros; exists y0; auto.
(* Goal: and (R x0 y0) (Rstar U R y0 z) *)
split; [ try assumption | idtac ].
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
apply T1 with z0; auto.
Qed.

Theorem Lemma1 :
 forall (U : Type) (R : Relation U),
 Strongly_confluent U R ->
 forall x b : U,
 Rstar U R x b -> forall a : U, R x a -> exists z : U, Rstar U R a z /\ R b z.
(* Goal: forall (U : Type) (R : Relation U) (_ : Strongly_confluent U R) (x b : U) (_ : Rstar U R x b) (a : U) (_ : R x a), @ex U (fun z : U => and (Rstar U R a z) (R b z)) *)
intros U R H' x b H'0; elim H'0.
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
intros x0 a H'1; exists a; auto.
(* Goal: forall (x y z : U) (_ : R x y) (_ : Rstar U R y z) (_ : forall (a : U) (_ : R y a), @ex U (fun z0 : U => and (Rstar U R a z0) (R z z0))) (a : U) (_ : R x a), @ex U (fun z0 : U => and (Rstar U R a z0) (R z z0)) *)
intros x0 y z H'1 H'2 H'3 a H'4.
(* Goal: @ex U (fun z0 : U => and (Rstar U R a z0) (R z z0)) *)
red in H'.
generalize (H' x0 a y); intro h; lapply h;
 [ intro H'5; lapply H'5;
    [ intro h0; elim h0; intros t h1; elim h1; intros H'6 H'7;
       clear h H'5 h0 h1; try exact H'6
    | clear h ]
 | clear h ]; auto 10.
generalize (H'3 t); intro h; lapply h;
 [ intro h0; elim h0; intros z1 h1; elim h1; intros H'5 H'8; clear h h0 h1;
    try exact H'5
 | clear h ]; auto 10.
(* Goal: @ex U (fun z0 : U => and (Rstar U R a z0) (R z z0)) *)
intros; exists z1; split; [ idtac | assumption ].
(* Goal: forall (U : Type) (R : Relation U), contains U (Rplus U R) R *)
apply Rstar_n with t; auto.
Qed.