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

Require iso_defs.
Require getl_props.
Require pr3_defs.
Require pr3_props.
Require pr3_gen.

   Section pr3_iso_props. (**************************************************)

      Hints Resolve pr3_t : ld.

      Lemma pr3_iso_appls_abbr: (c,d:?; w:?; i:?)
                                (getl i c (CHead d (Bind Abbr) w)) -> (vs:?)
                                let u1 = (THeads (Flat Appl) vs (TLRef i)) in
                                (u2:?) (pr3 c u1 u2) ->
                                ((iso u1 u2) -> (P:Prop) P) ->
                                (pr3 c (THeads (Flat Appl) vs (lift (S i) O w)) u2).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: nil *)
      Pr3Gen; Subst.
(* case 1.1: pr2_free *)
      Apply H1; XAuto.
(* case 1.2: pr2_delta *)
      GetLDis; XInv; Subst; GetLDrop; XDEAuto 2.
(* case 2: cons *)
      Pr3Gen; Subst.
(* case 2.1: pr0_cong *)
      EApply H2; XAuto.
(* case 2.2: pr0_beta *)
      EApply pr3_t with t2:=(THead (Bind Abbr) t x1); [ Idtac | XDEAuto 3 ]. Clear H4 H5 H7.
      EApply pr3_t with t2:=(THead (Flat Appl) t (THead (Bind Abst) x0 x1)); [ Idtac | XDEAuto 4 ].
      Apply pr3_thin_dx; Apply H0; [ XAuto | Intros; IsoGenBase ].
(* case 2.2: pr0_upsilon *)
      EApply pr3_t with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (1) (0) x4) x2)); [ Idtac | XDEAuto 4 ]. Clear H6 H8 H9.
      EApply pr3_t with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (1) (0) t) x2)); [ Idtac | XDEAuto 5 ]. Clear H7.
      EApply pr3_t with t2:=(THead (Flat Appl) t (THead (Bind x0) x1 x2)); [ Idtac | XDEAuto 4 ].
      Apply pr3_thin_dx; Apply H0; [ XAuto | Intros; IsoGenBase ].
      Qed.

      Lemma pr3_iso_appls_cast: (c:?; v,t:?; vs:?)
                                let u1 = (THeads (Flat Appl) vs (THead (Flat Cast) v t)) in
                                (u2:?) (pr3 c u1 u2) -> ((iso u1 u2) -> (P:Prop) P) ->
                                (pr3 c (THeads (Flat Appl) vs t) u2).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: nil *)
      Pr3Gen; Subst; [ Apply H0; XAuto | XAuto ].
(* case 2: cons *)
      Pr3Gen; Subst.
(* case 2.1: pr0_cong *)
      Apply H1; XAuto.
(* case 2.2: pr0_beta *)
      EApply pr3_t with t2:=(THead (Bind Abbr) t0 x1); [ Idtac | XDEAuto 3 ]. Clear H1 H3 H4 H6.
      EApply pr3_t with t2:=(THead (Flat Appl) t0 (THead (Bind Abst) x0 x1)); [ Idtac | XDEAuto 4 ].
      Apply pr3_thin_dx; Apply H; [ XAuto | Intros; IsoGenBase ].
(* case 2.2: pr0_upsilon *)
      EApply pr3_t with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (1) (0) x4) x2)); [ Idtac | XDEAuto 4 ]. Clear H1 H5 H7 H8.
      EApply pr3_t with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (1) (0) t0) x2)); [ Idtac | XDEAuto 5 ]. Clear H6.
      EApply pr3_t with t2:=(THead (Flat Appl) t0 (THead (Bind x0) x1 x2)); [ Idtac | XDEAuto 4 ].
      Apply pr3_thin_dx; Apply H; [ XAuto | Intros; IsoGenBase ].
      Qed.

      Hints Resolve pr3_pr3_pr3_t : ld.

      Lemma pr3_iso_appl_bind: (b:?) ~b=Abst -> (v1,v2,t:?)
                               let u1 = (THead (Flat Appl) v1 (THead (Bind b) v2 t)) in
                               (c:?; u2:?) (pr3 c u1 u2) -> ((iso u1 u2) -> (P:Prop) P) ->
                               (pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (1) (0) v1) t)) u2).
      Proof.
      Simpl; Intros; Pr3Gen; Subst.
(* case 1: pr0_cong *)
      Apply H1; XAuto.
(* case 2: pr0_beta *)
      EApply pr3_t; [ Idtac | XDEAuto 2 ].
      Clear H3 H1 u2; Pr3Gen.
(* case 2.1: pr0_cong *)
      XInv; Subst; EqFalse.
(* case 2.2: pr0_upsilon *)
      EApply pr3_t.
      Apply pr3_head_2; Apply pr3_flat; [ EApply pr3_lift | Idtac ]; XDEAuto 2.
      Clear H0 H4 t v1; LiftHeadRwBack.
      Apply pr3_sing with t2:=(THead (Bind Abbr) x2 x1); XAuto.
(* case 3: pr0_upsilon *)
      EApply pr3_t; [ Idtac | XDEAuto 2 ].
      Clear H5 H1 u2; Pr3Gen.
(* case 3.1: pr0_cong *)
      XInv; Subst; Clear H3.
      Apply pr3_head_21; [ XDEAuto 2 | Apply pr3_flat; XDEAuto 4 ].
(* case 3.2: pr0_upsilon *)
      EApply pr3_t.
      Apply pr3_head_2; Apply pr3_flat; [ EApply pr3_lift | Idtac ]; XDEAuto 2.
      Clear H0 H6 t v1; LiftHeadRwBack.
      Apply pr3_sing with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)); XAuto.
      Qed.

      Hints Resolve pr3_iso_appl_bind : ld.

      Lemma pr3_iso_appls_appl_bind: (b:?) ~b=Abst -> (v,u,t:?; vs:?)
                                     let u1 = (THeads (Flat Appl) vs (THead (Flat Appl) v (THead (Bind b) u t))) in
                                     (c:?; u2:?) (pr3 c u1 u2) -> ((iso u1 u2) -> (P:Prop) P) ->
                                     (pr3 c (THeads (Flat Appl) vs (THead (Bind b) u (THead (Flat Appl) (lift (S O) O v) t))) u2).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: TNil *)
      XAuto.
(* case 2: TCons *)
      Pr3Gen; Subst.
(* case 2.1: pr0_cong *)
      Apply H2; XAuto.
(* case 2.2: pr0_beta *)
      EApply pr3_t with t2:=(THead (Bind Abbr) t0 x1); [ Idtac | XDEAuto 3 ]. Clear H2 H4 H5 H7.
      EApply pr3_t with t2:=(THead (Flat Appl) t0 (THead (Bind Abst) x0 x1)); [ Idtac | XDEAuto 4 ].
      Apply pr3_thin_dx; Apply H0; [ XAuto | Intros; IsoGenBase ].
(* case 2.3: pr0_upsilon *)
      EApply pr3_t with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (1) (0) x4) x2)); [ Idtac | XDEAuto 4 ]. Clear H2 H6 H8 H9.
      EApply pr3_t with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (1) (0) t0) x2)); [ Idtac | XDEAuto 5 ]. Clear H7.
      EApply pr3_t with t2:=(THead (Flat Appl) t0 (THead (Bind x0) x1 x2)); [ Idtac | XDEAuto 4 ].
      Apply pr3_thin_dx; Apply H0; [ XAuto | Intros; IsoGenBase ].
      Qed.

      Hints Resolve pr3_iso_appls_appl_bind : ld.

      Lemma pr3_iso_appls_bind: (b:?) ~b=Abst -> (vs:?; u,t:?)
                                let u1 = (THeads (Flat Appl) vs (THead (Bind b) u t)) in
                                (c:?; u2:?) (pr3 c u1 u2) -> ((iso u1 u2) -> (P:Prop) P) ->
                                (pr3 c (THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O vs) t)) u2).
      Proof.
      XElimUsing tlist_ind_rev vs; Simpl; Intros.
(* case 1: TNil *)
      XAuto.
(* case 2: TCons *)
      Rewrite lifts_tapp; Rewrite theads_tapp.
      Rewrite theads_tapp in H1; Rewrite theads_tapp in H2.
      NewInduction ts.
(* case 2.1: TNil *)
      Clear H0; Simpl; XAuto.
(* case 2.2: TCons *)
      Clear IHts; Apply H0; [ XAuto | Clear H0 H1; Intros ].
      Apply H2; EApply iso_trans; [ Idtac | Apply H0 ].
      Simpl; XAuto.
      Qed.

      Lemma pr3_iso_beta: (v,w,t:?)
                          let u1 = (THead (Flat Appl) v (THead (Bind Abst) w t)) in
                          (c:?; u2:?) (pr3 c u1 u2) -> ((iso u1 u2) -> (P:Prop) P) ->
                          (pr3 c (THead (Bind Abbr) v t) u2).
      Proof.
      Simpl; Intros; Pr3Gen; Subst.
(* case 1: pr0_cong *)
      Apply H0; XAuto.
(* case 2: pr0_beta *)
      Pr3GenBase; XInv; Subst.
      EApply pr3_t; [ Idtac | XDEAuto 2 ].
      XDEAuto 3.
(* case 2: pr0_upsilon *)
      Pr3GenBase; XInv; Subst; EqFalse.
      Qed.

      Hints Resolve pr3_iso_beta : ld.

      Lemma pr3_iso_appls_beta: (us:?; v,w,t:?)
                                let u1 = (THeads (Flat Appl) us (THead (Flat Appl) v (THead (Bind Abst) w t))) in
                                (c:?; u2:?) (pr3 c u1 u2) -> ((iso u1 u2) -> (P:Prop) P) ->
                                (pr3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t)) u2).
      Proof.
      XElim us; Simpl; Intros.
(* case 1: TNil *)
      XDEAuto 2.
(* case 2: TCons *)
      Pr3Gen; Subst.
(* case 2.1: pr0_cong *)
      Apply H1; XAuto.
(* case 2.2: pr0_beta *)
      Apply pr3_t with t2:=(THead (Bind Abbr) t x1); [ Idtac | XDEAuto 3 ]. Clear H1 H3 H4 H6 u2 x3 x2.
      Apply pr3_t with t2:=(THead (Flat Appl) t (THead (Bind Abst) x0 x1)); [ Idtac | XAuto ].
      Apply pr3_thin_dx; EApply H; [ XDEAuto 2 | Idtac ].
      Intros; IsoGenBase.
(* case 2.3: pr0_upsilon *)
      Apply pr3_t with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)); [ Idtac | XDEAuto 4 ]. Clear H1 H5 H7 H8 u2 x3 x5.
      Apply pr3_t with t2:=(THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O t) x2)); [ Idtac | XDEAuto 5 ]. Clear H6 x4.
      Apply pr3_t with t2:=(THead (Flat Appl) t (THead (Bind x0) x1 x2)); [ Idtac | XAuto ].
      Apply pr3_thin_dx; EApply H; [ XDEAuto 2 | Idtac ].
      Intros; IsoGenBase.
      Qed.

   End pr3_iso_props.