(* 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                               *)
(*                                                                          *)
(****************************************************************************)
(*                             confluence_LSL.v                             *)
(****************************************************************************)

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


                 (* Confluence du lambda-sigma-lift *)

Require Import TS.
Require Import sur_les_relations.
Require Import sigma_lift.
Require Import lambda_sigma_lift.
Require Import terminaison_SL.
Require Import conf_local_SL.
Require Import betapar.
Require Import SLstar_bpar_SLstar.
Require Import conf_strong_betapar.
Require Import commutation.
Require Import Newman.
Require Import Yokouchi.


Goal forall b : wsort, explicit_confluence _ (e_relSL b).
(* Goal: forall b : wsort, explicit_confluence (TS b) (e_relSL b) *)
intros b.
(* Goal: explicit_confluence (TS b) (e_relSL b) *)
apply Newman.
(* Goal: explicit_noetherian (TS b) (e_relSL b) *)
(* Goal: explicit_strong_confluence (TS b) (e_beta_par b) *)
(* Goal: forall (f g h : TS b) (_ : e_relSL b f h) (_ : e_beta_par b f g), @ex (TS b) (fun k : TS b => and (explicit_star (TS b) (e_relSL b) g k) (Rstar_S_Rstar (TS b) (e_relSL b) (e_beta_par b) h k)) *)
apply relSL_noetherian.
(* Goal: explicit_local_confluence (TS b) (e_relSL b) *)
apply conf_local_SL.
Save confluence_SL.

Goal forall b : wsort, explicit_strong_confluence _ (e_slstar_bp_slstar b).
(* Goal: forall b : wsort, explicit_strong_confluence (TS b) (e_slstar_bp_slstar b) *)
intro b; unfold e_slstar_bp_slstar in |- *.
change
  (explicit_strong_confluence _
     (Rstar_S_Rstar (TS b) (e_relSL b) (e_beta_par b))) 
 in |- *.
(* Goal: explicit_strong_confluence (TS b) (Rstar_S_Rstar (TS b) (e_relSL b) (e_beta_par b)) *)
apply Yokouchi.
(* Goal: explicit_confluence (TS b) (e_relSL b) *)
(* Goal: explicit_noetherian (TS b) (e_relSL b) *)
(* Goal: explicit_strong_confluence (TS b) (e_beta_par b) *)
(* Goal: forall (f g h : TS b) (_ : e_relSL b f h) (_ : e_beta_par b f g), @ex (TS b) (fun k : TS b => and (explicit_star (TS b) (e_relSL b) g k) (Rstar_S_Rstar (TS b) (e_relSL b) (e_beta_par b) h k)) *)
apply confluence_SL.
(* Goal: explicit_noetherian (TS b) (e_relSL b) *)
(* Goal: explicit_strong_confluence (TS b) (e_beta_par b) *)
(* Goal: forall (f g h : TS b) (_ : e_relSL b f h) (_ : e_beta_par b f g), @ex (TS b) (fun k : TS b => and (explicit_star (TS b) (e_relSL b) g k) (Rstar_S_Rstar (TS b) (e_relSL b) (e_beta_par b) h k)) *)
apply relSL_noetherian.
(* Goal: explicit_strong_confluence (TS b) (e_beta_par b) *)
(* Goal: forall (f g h : TS b) (_ : e_relSL b f h) (_ : e_beta_par b f g), @ex (TS b) (fun k : TS b => and (explicit_star (TS b) (e_relSL b) g k) (Rstar_S_Rstar (TS b) (e_relSL b) (e_beta_par b) h k)) *)
apply sconf_betapar.
(* Goal: forall (f g h : TS b) (_ : e_relSL b f h) (_ : e_beta_par b f g), @ex (TS b) (fun k : TS b => and (explicit_star (TS b) (e_relSL b) g k) (Rstar_S_Rstar (TS b) (e_relSL b) (e_beta_par b) h k)) *)
intros f g h H H0.
(* Goal: @ex (TS b) (fun k : TS b => and (explicit_star (TS b) (e_relSL b) g k) (Rstar_S_Rstar (TS b) (e_relSL b) (e_beta_par b) h k)) *)
unfold Rstar_S_Rstar in |- *.
change (exists k : TS b, e_relSLstar _ g k /\ e_slstar_bp_slstar _ h k)
 in |- *.
(* Goal: @ex (TS b) (fun k : TS b => and (e_relSLstar b g k) (e_slstar_bp_slstar b h k)) *)
apply commutation with f; assumption.
Save strong_confluence_slbpsl.

Goal forall b : wsort, explicit_confluence _ (e_slstar_bp_slstar b).
(* Goal: forall b : wsort, explicit_confluence (TS b) (e_slstar_bp_slstar b) *)
intro b; apply strong_conf_conf; apply strong_confluence_slbpsl.
Save confluence_slbpsl.


(**********************************************)
(*        lambda-sigma-lift est confluent     *)
(**********************************************)

Theorem confluence_LSL : forall b : wsort, explicit_confluence _ (e_relLSL b).
Proof.
(* Goal: forall b : wsort, explicit_confluence (TS b) (e_relLSL b) *)
intro b; apply inclus_conf with (e_slstar_bp_slstar b).
(* Goal: explicit_inclus (TS b) (e_relLSL b) (e_slstar_bp_slstar b) *)
(* Goal: explicit_inclus (TS b) (e_slstar_bp_slstar b) (explicit_star (TS b) (e_relLSL b)) *)
(* Goal: explicit_confluence (TS b) (e_slstar_bp_slstar b) *)
apply relLSL_inclus_slbpsl.
(* Goal: explicit_inclus (TS b) (e_slstar_bp_slstar b) (explicit_star (TS b) (e_relLSL b)) *)
(* Goal: explicit_confluence (TS b) (e_slstar_bp_slstar b) *)
change (explicit_inclus _ (e_slstar_bp_slstar b) (e_relLSLstar b)) in |- *.
(* Goal: explicit_inclus (TS b) (e_slstar_bp_slstar b) (e_relLSLstar b) *)
(* Goal: explicit_confluence (TS b) (e_slstar_bp_slstar b) *)
apply slbpsl_inclus_relLSLstar.
(* Goal: explicit_confluence (TS b) (e_slstar_bp_slstar b) *)
apply confluence_slbpsl.
Qed.


