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

Require Export nf2_defs.

(* NOTE: The bad design of pr2_delta forbids to use pr2 here as we should *)
      Inductive sn3 [c:C]: T -> Prop :=
         | sn3_sing: (t1:?) ((t2:?) (t1 = t2 -> (P:Prop) P) -> (pr3 c t1 t2) -> (sn3 c t2) ) -> (sn3 c t1).

      Fixpoint sns3 [c:C; ts:TList] : Prop := Cases ts of
         | TNil         => True
         | (TCons t ts) => (sn3 c t) /\ (sns3 c ts)
      end.

   Section sn3_gen_base. (***************************************************)

      Lemma sn3_gen_bind: (b:?; c:?; u,t:?) (sn3 c (THead (Bind b) u t)) ->
                          (sn3 c u) /\ (sn3 (CHead c (Bind b) u) t).
      Proof.
      Intros; InsertEq H '(THead (Bind b) u t); UnIntro H t; UnIntro H u.
      XElim H; Clear y; Intros; Rename x0 into t; Rename x into u.
      Subst; Split; Apply sn3_sing; Intros.
(* case 1.1: sn3_sing, first conclusion *)
      LApply (H0 (THead (Bind b) t2 t));
      [ Clear H0; Intros H0 | Intros; XInv; Subst; EApply H1; XDEAuto 1 ].
      LApply H0; [ Clear H0; Intros H0 | XDEAuto 2 ].
      LApply (H0 t2 t); [ Clear H0; Intros H0 | XAuto ].
      XDecompose H0; XAuto.
(* case 1.2: sn3_sing, second conclusion *)
      LApply (H0 (THead (Bind b) u t2));
      [ Clear H0; Intros H0 | Intros; XInv; Subst; EApply H1; XDEAuto 1 ].
      LApply H0; [ Clear H0; Intros H0 | XDEAuto 2 ].
      LApply (H0 u t2); [ Clear H0; Intros H0 | XAuto ].
      XDecompose H0; XAuto.
      Qed.

      Lemma sn3_gen_flat: (f:?; c:?; u,t:?) (sn3 c (THead (Flat f) u t)) ->
                          (sn3 c u) /\ (sn3 c t).
      Proof.
      Intros; InsertEq H '(THead (Flat f) u t); UnIntro H t; UnIntro H u.
      XElim H; Clear y; Intros; Rename x0 into t; Rename x into u.
      Subst; Split; Apply sn3_sing; Intros.
(* case 1.1: sn3_sing, first conclusion *)
      LApply (H0 (THead (Flat f) t2 t));
      [ Clear H0; Intros H0 | Intros; XInv; Subst; EApply H1; XDEAuto 1 ].
      LApply H0; [ Clear H0; Intros H0 | XDEAuto 2 ].
      LApply (H0 t2 t); [ Clear H0; Intros H0 | XAuto ].
      XDecompose H0; XAuto.
(* case 1.2: sn3_sing, second conclusion *)
      LApply (H0 (THead (Flat f) u t2));
      [ Clear H0; Intros H0 | Intros; XInv; Subst; EApply H1; XDEAuto 1 ].
      LApply H0; [ Clear H0; Intros H0 | XDEAuto 2 ].
      LApply (H0 u t2); [ Clear H0; Intros H0 | XAuto ].
      XDecompose H0; XAuto.
      Qed.

      Lemma sn3_gen_head: (k:?; c:?; u,t:?)
                          (sn3 c (THead k u t)) -> (sn3 c u).
      Proof.
      XElim k; Intros;
      [ XDecomPoseClear H '(sn3_gen_bind ? ? ? ? H)
      | XDecomPoseClear H '(sn3_gen_flat ? ? ? ? H)
      ]; XAuto.
      Qed.

      Hints Resolve sn3_sing : ld.

      Lemma sn3_gen_cflat: (f:?; c:?; u,t:?)
                           (sn3 (CHead c (Flat f) u) t) -> (sn3 c t).
      Proof.
      Intros; XElim H; Clear t; Intros; XDEAuto 4.
      Qed.

   End sn3_gen_base.

      Tactic Definition SN3GenBase := (
         Match Context With
            | [ H: (sn3 ? (THead (Bind ?) ? ?)) |- ? ] ->
               XDecomPose '(sn3_gen_bind ? ? ? ? H)
            | [ H: (sn3 ? (THead (Flat ?) ? ?)) |- ? ] ->
               XDecomPose '(sn3_gen_flat ? ? ? ? H)
            | [ H: (sn3 (CHead ? (Flat ?) ?) ?) |- ? ] ->
               XPoseClear H '(sn3_gen_cflat ? ? ? ? H)
            | [ H: (sn3 ? (THead ? ? ?)) |- ? ] ->
               XPoseClear H '(sn3_gen_head ? ? ? ? H)
         ).

   Section sn3_props. (******************************************************)

      Lemma sn3_nf2: (c:?; t:?) (nf2 c t) -> (sn3 c t).
      Proof.
      Intros; Apply sn3_sing; Intros.
      NF2Unfold3; EApply H0; XAuto.
      Qed.

      Lemma sn3_pr3_trans: (c:?; t1:?) (sn3 c t1) -> (t2:?) (pr3 c t1 t2) ->
                           (sn3 c t2).
      Proof.
      Intros until 1; XElim H; Clear t1; Intros.
(* single case: sn3_sing *)
      Apply sn3_sing; Intros.
      XDecomPose '(term_dec t1 t2); Subst; XDEAuto 3.
      Qed.

      Hints Resolve sn3_pr3_trans : ld.

      Lemma sn3_pr2_intro: (c:?; t1:?)
                           ((t2:?) (t1 = t2 -> (P:Prop) P) ->
                            (pr2 c t1 t2) -> (sn3 c t2)
                           ) -> (sn3 c t1).
      Proof.
      Intros; EApply sn3_sing; Intros.
      Impl H1 H0; Impl H1 H.
      XElim H1; Clear t1 t2; Intros.
(* case 1: pr3_refl *)
      XDEAuto 3.
(* case 2: pr3_sing *)
      XDecomPose '(term_dec t1 t2); Subst; XDEAuto 3.
      Qed.

      Hints Resolve sn3_sing sn3_pr2_intro : ld.

      Theorem sn3_cast: (c:?; u:?) (sn3 c u) -> (t:?) (sn3 c t) ->
                        (sn3 c (THead (Flat Cast) u t)).
      Proof.
      Intros until 1; XElim H; Clear u; Intros; XElim H1; Clear u1; Intros.
(* single case: sn3_sing *)
      EApply sn3_pr2_intro; Intros.
      Pr2GenBase; Subst.
(* case 1: pr0_comp *)
      XDecomPose '(term_dec x0 t1); Subst.
(* case 1.1: x0 = t1 *)
      XDecomPose '(term_dec t0 x1); Subst; [ EApply H3 | Idtac ]; XDEAuto 3.
(* case 1.2: x0 <> t1 *)
      EApply H0; Intros; Subst; [ EApply H4; XAuto | XAuto | Idtac ].
      XDecomPose '(term_dec t0 x1); Subst; XDEAuto 3.
(* case 2: pr0_cast *)
      XDEAuto 4.
      Qed.

      Hints Resolve pr2_gen_cflat : ld.

      Lemma sn3_cflat: (c:?; t:?) (sn3 c t) ->
                       (f:?; u:?) (sn3 (CHead c (Flat f) u) t).
      Proof.
      Intros; XElim H; Clear t; Intros; XDEAuto 5.
      Qed.

      Lemma sn3_shift: (b:?; c:?; v,t:?) (sn3 c (THead (Bind b) v t)) ->
                       (sn3 (CHead c (Bind b) v) t).
      Proof.
      Intros; SN3GenBase; XAuto.
      Qed.

      Hints Resolve pr2_change : ld.

      Lemma sn3_change: (b:?) ~b=Abbr ->
                        (c:?; v1,t:?) (sn3 (CHead c (Bind b) v1) t) ->
                        (v2:?) (sn3 (CHead c (Bind b) v2) t).
      Proof.
      Intros; XElim H0; Clear t; XDEAuto 5.
      Qed.

   End sn3_props.

      Hints Resolve sn3_nf2 sn3_cast sn3_cflat : ld.