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

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 Newman.v                                 *)
(****************************************************************************)

(*****************************************************************************)
(*          Projet Coq  - Calculus of Inductive Constructions V5.8           *)
(*****************************************************************************)
(*                                                                           *)
(*      Meta-theory of the explicit substitution calculus lambda-env         *)
(*      Amokrane Saibi                                                       *)
(*                                                                           *)
(*      September 1993                                                       *)
(*                                                                           *)
(*****************************************************************************)


                               (* Theoreme de Newman *)

Require Import sur_les_relations.

Section NewmanS.
 Variable A : Set.
 Variable R : A -> A -> Prop.
 Hypothesis N : explicit_noetherian _ R.
 Hypothesis C : explicit_local_confluence _ R.

   Theorem Newman : explicit_confluence _ R.
   unfold explicit_confluence in |- *; intro x; pattern x in |- *;
    apply (noetherian_induction1 A R N).
(* Goal: forall (y : A) (_ : forall (z : A) (_ : R y z), confluence_en A R z), confluence_en A R y *)
   intros y H1; unfold confluence_en in |- *.
(* Goal: forall (y0 z : A) (_ : explicit_star A R y y0) (_ : explicit_star A R y z), @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   intros y0 z H2 H3; elim (star_case A R y z H3); intro H4.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   exists y0; split.
(* Goal: explicit_star A R z z *)
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   apply star_refl.
(* Goal: explicit_star A R z y0 *)
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   rewrite <- H4; assumption.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   elim (star_case A R y y0 H2); intro H5.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   exists z; split.
(* Goal: explicit_star A R y0 z *)
(* Goal: explicit_star A R z z *)
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   rewrite <- H5; assumption.
(* Goal: explicit_star A R z z *)
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   apply star_refl.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   elim H5; intros y0' H6; elim H6; intros H7 H8.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   elim H4; intros z' H9; elim H9; intros H10 H11.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   elim (C y y0' z' H7 H10); intros y' H12.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   elim H12; intros H13 H14.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   elim (H1 y0' H7 y0 y' H8 H13); intros y'' H15.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   elim H15; intros H16 H17.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   elim (H1 z' H10 y'' z (star_trans A R z' y' y'' H14 H17) H11).
(* Goal: forall (x : A) (_ : and (explicit_star A R y'' x) (explicit_star A R z x)), @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   intros u H18; elim H18; intros H19 H20.
(* Goal: @ex A (fun u : A => and (explicit_star A R y0 u) (explicit_star A R z u)) *)
   exists u; split.
(* Goal: explicit_star A R y0 u *)
(* Goal: explicit_star A R z u *)
   apply star_trans with y''; assumption.
(* Goal: explicit_star A R z u *)
   assumption.
   Qed.
End NewmanS.


