(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require tlt_defs.
Require lift_gen.
Require lift_tlt.
Require subst0_gen.
Require subst0_confluence.
Require pr0_defs.
Require pr0_lift.
Require pr0_gen.
Require pr0_subst0.

   Section pr0_confluence. (*************************************************)

      Tactic Definition SSubstInv := (
         Match Context With
            | [ H0: (THead ? ? ?) = (THead ? ? ?) |- ? ] -> XInv
            | [ H0: (pr0 (THead (Bind ?1) ?2 ?3) ?) |- ? ] ->
               Inversion H0; Clear H0
            | [ |- ? ] -> EqFalse Orelse LiftGen Orelse Pr0Gen
         ).

      Tactic Definition SSubstBack := (
         Match Context With
            | [ H0: Abst = ?1; H1:? |- ? ] ->
               Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
            | [ H0: Abbr = ?1; H1:? |- ? ] ->
               Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
            | [ H0: (? ?) = ?1; H1:? |- ? ] ->
               Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
            | [ H0: (? ? ? ?) = ?1; H1:? |- ? ] ->
               Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
         ).

      Tactic Definition SSubst := (
         Match Context With
            | [ H0: ?1 = ?; H1:? |- ? ] ->
               Rewrite H0 in H1 Orelse Rewrite H0 Orelse Clear H0 ?1
         ).

      Tactic Definition XSubst :=
         Repeat (SSubstInv Orelse SSubstBack Orelse SSubst).

      Tactic Definition IH := (
         Match Context With
            | [ H0: (pr0 ?1 ?2); H1: (pr0 ?1 ?3) |- ? ] ->
               LApply (H ?1); [ Intros H_x | XDEAuto 2 ];
               LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];
               LApply (H_x ?3); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Clear H0 H1; Intros
         ).

(* case pr0_cong pr0_upsilon pr0_refl ***************************************)

      Remark pr0_cong_upsilon_refl: (b:?) ~ b = Abst ->
                                    (u0,u3:?) (pr0 u0 u3) ->
                                    (t4,t5:?) (pr0 t4 t5) ->
                                    (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
                                    (EX t | (pr0 (THead (Flat Appl) u2 (THead (Bind b) u0 t4)) t) &
                                            (pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (1) (0) v2) t5)) t)).
      Proof.
      Intros.
      Apply ex2_intro with x:=(THead (Bind b) u3 (THead (Flat Appl) (lift (1) (0) x) t5)); XAuto.
      Qed.

(* case pr0_cong pr0_upsilon pr0_cong ***************************************)

      Remark pr0_cong_upsilon_cong: (b:?) ~ b = Abst ->
                                    (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
                                    (t2,t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
                                    (u5,u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
                                    (EX t | (pr0 (THead (Flat Appl) u2 (THead (Bind b) u5 t2)) t) &
                                            (pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (1) (0) v2) t5)) t)).
      Proof.
      Intros.
      Apply ex2_intro with x:=(THead (Bind b) x1 (THead (Flat Appl) (lift (1) (0) x) x0)); XAuto.
      Qed.

(* case pr0_cong pr0_upsilon pr0_delta **************************************)

      Remark pr0_cong_upsilon_delta: ~ Abbr = Abst ->
                                     (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
                                     (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
                                     (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
                                     (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
                                     (EX t | (pr0 (THead (Flat Appl) u2 (THead (Bind Abbr) u5 w)) t) &
                                             (pr0 (THead (Bind Abbr) u3 (THead (Flat Appl) (lift (1) (0) v2) t5)) t)).
      Proof.
      Intros; Pr0Subst0.
(* case 1: x0 is a lift *)
      Apply ex2_intro with x:=(THead (Bind Abbr) x1 (THead (Flat Appl) (lift (1) (0) x) x0)); XAuto.
(* case 2: x0 is not a lift *)
      Apply ex2_intro with x:=(THead (Bind Abbr) x1 (THead (Flat Appl) (lift (1) (0) x) x2)); XDEAuto 5.
      Qed.

(* case pr0_cong pr0_upsilon pr0_zeta ***************************************)

      Remark pr0_cong_upsilon_zeta: (b:?) ~ b = Abst ->
                                    (u0,u3:?) (pr0 u0 u3) ->
                                    (u2,v2,x0:?) (pr0 u2 x0) -> (pr0 v2 x0) ->
                                    (x,t3,x1:?) (pr0 x x1) -> (pr0 t3 x1) ->
                                    (EX t | (pr0 (THead (Flat Appl) u2 t3) t) &
                                            (pr0 (THead (Bind b) u3 (THead (Flat Appl) (lift (1) (0) v2) (lift (1) (0) x))) t)).
      Proof.
      Intros; LiftHeadRwBack; XDEAuto 5.
      Qed.

(* case pr0_cong pr0_delta **************************************************)

      Remark pr0_cong_delta: (u3,t5,w:?) (subst0 (0) u3 t5 w) ->
                             (u2,x:?) (pr0 u2 x) -> (pr0 u3 x) ->
                             (t3,x0:?) (pr0 t3 x0) -> (pr0 t5 x0) ->
                             (EX t | (pr0 (THead (Bind Abbr) u2 t3) t) &
                                     (pr0 (THead (Bind Abbr) u3 w) t)).
      Proof.
      Intros; Pr0Subst0; XDEAuto 4.
      Qed.

(* case pr0_upsilon pr0_upsilon *********************************************)

      Remark pr0_upsilon_upsilon: (b:?) ~ b = Abst ->
                                  (v1,v2,x0:?) (pr0 v1 x0) -> (pr0 v2 x0) ->
                                  (u1,u2,x1:?) (pr0 u1 x1) -> (pr0 u2 x1) ->
                                  (t1,t2,x2:?) (pr0 t1 x2) -> (pr0 t2 x2) ->
                                  (EX t | (pr0 (THead (Bind b) u1 (THead (Flat Appl) (lift (1) (0) v1) t1)) t) &
                                          (pr0 (THead (Bind b) u2 (THead (Flat Appl) (lift (1) (0) v2) t2)) t)).
      Proof.
      Intros.
      Apply ex2_intro with x:=(THead (Bind b) x1 (THead (Flat Appl) (lift (1) (0) x0) x2)); XAuto.
      Qed.

(* case pr0_delta pr0_delta *************************************************)

      Remark pr0_delta_delta: (u2,t3,w:?) (subst0 (0) u2 t3 w) ->
                              (u3,t5,w0:?) (subst0 (0) u3 t5 w0) ->
                              (x:?) (pr0 u2 x) -> (pr0 u3 x) ->
                              (x0:?) (pr0 t3 x0) -> (pr0 t5 x0) ->
                              (EX t | (pr0 (THead (Bind Abbr) u2 w) t) &
                                      (pr0 (THead (Bind Abbr) u3 w0) t)).
      Proof.
      Intros; Pr0Subst0; Pr0Subst0; Try Subst0Confluence; XSubst; XDEAuto 4.
      Qed.

(* case pr0_delta pr0_tau ***********************************************)

      Remark pr0_delta_tau: (u2,t3,w:?) (subst0 (0) u2 t3 w) ->
                                (t4:?) (pr0 (lift (1) (0) t4) t3) ->
                                (t2:?) (EX t | (pr0 (THead (Bind Abbr) u2 w) t) & (pr0 t2 t)).
      Proof.
      Intros; Pr0Gen; XSubst; Subst0Gen.
      Qed.

(* main *********************************************************************)

      Hints Resolve pr0_cong_upsilon_refl pr0_cong_upsilon_cong : ld.
      Hints Resolve pr0_cong_upsilon_delta pr0_cong_upsilon_zeta : ld.
      Hints Resolve pr0_cong_delta : ld.
      Hints Resolve pr0_upsilon_upsilon : ld.
      Hints Resolve pr0_delta_delta pr0_delta_tau : ld.
      Hints Resolve ex2_sym tlt_trans : ld.

      Theorem pr0_confluence: (t0,t1:?) (pr0 t0 t1) -> (t2:?) (pr0 t0 t2) ->
                              (EX t | (pr0 t1 t) & (pr0 t2 t)).
      Proof.
      XElimUsing tlt_wf_ind t0; Intros.
      Inversion H0; Inversion H1; Clear H0 H1;
      XSubst; Repeat IH; XDEAuto 4.
      Qed.

   End pr0_confluence.

      Tactic Definition Pr0Confluence := (
         Match Context With
            | [ H1: (pr0 ?1 ?2); H2: (pr0 ?1 ?3) |-? ] ->
               LApply (pr0_confluence ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
         ).