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

      Inductive B: Set :=
         | Abbr: B
         | Abst: B
         | Void: B.

      Inductive F: Set :=
         | Appl: F
         | Cast: F.

      Inductive K: Set :=
         | Bind: B -> K
         | Flat: F -> K.

      Inductive T: Set :=
         | TSort: nat -> T
         | TLRef: nat -> T
         | THead: K -> T -> T -> T.

      Hint f3KTT : ld := Resolve (f_equal3 K T T).

      Definition s: K -> nat -> nat := [k,i:?] Cases k of
         | (Bind _) => (S i)
         | (Flat _) => i
      end.

   Section terms_props. (****************************************************)

      Lemma not_abbr_abst: ~Abbr=Abst.
      Proof.
      Unfold not; Intros; XInv.
      Qed.

      Lemma not_void_abst: ~Void=Abst.
      Proof.
      Unfold not; Intros; XInv.
      Qed.

      Lemma not_abbr_void: ~Abbr=Void.
      Proof.
      Unfold not; Intros; XInv.
      Qed.

      Lemma not_abst_void: ~Abst=Void.
      Proof.
      Unfold not; Intros; XInv.
      Qed.

      Remark bind_dec: (b1,b2:B) b1 = b2 \/ (b1 = b2 -> (P:Prop) P).
      Proof.
      XElim b1; XElim b2; Intros;
      Try Solve [ DecFalse ]; XAuto.
      Qed.

      Lemma bind_dec_not: (b1,b2:B) b1 = b2 \/ ~b1=b2.
      Proof.
      Unfold not; Intros; XDecomPose '(bind_dec b1 b2);
      [ XAuto | Right; Intros; Apply H; XAuto ].
      Qed.

      Remark flat_dec: (f1,f2:F) f1 = f2 \/ (f1 = f2 -> (P:Prop) P).
      Proof.
      XElim f1; XElim f2; Intros;
      Try Solve [ DecFalse ]; XAuto.
      Qed.

      Remark kind_dec: (k1,k2:K) k1 = k2 \/ (k1 = k2 -> (P:Prop) P).
      Proof.
      XElim k1; XElim k2; Intros;
      Try Solve [ DecFalse ].
(* case 1: Bind *)
      XDecomPose '(bind_dec b b0); Subst;
      [ XAuto | DecFalse; EApply H; XDEAuto 1 ].
(* case 2: Flat *)
      XDecomPose '(flat_dec f f0); Subst;
      [ XAuto | DecFalse; EApply H; XDEAuto 1 ].
      Qed.

      Lemma term_dec: (t1,t2:T) t1 = t2 \/ (t1 = t2 -> (P:Prop) P).
      Proof.
      XElim t1; XElim t2; Intros;
      Try Solve [ Right; Intros; XInv ].
(* case 1: TSort, TSort *)
      XDecomPose '(nat_dec n n0); Subst;
      [ XAuto | DecFalse; EApply H; XDEAuto 1 ].
(* case 2: TLRef, TLRef *)
      XDecomPose '(nat_dec n n0); Subst;
      [ XAuto | DecFalse; EApply H; XDEAuto 1 ].
(* case 3: THead, THead *)
      XDecomPoseClear H '(H t1); Subst.
(* case 3.1: t = t1 *)
      XDecomPoseClear H0 '(H0 t2); Subst.
(* case 3.1.1: t0 = t2 *)
      XDecomPose '(kind_dec k k0); Subst;
      [ XAuto | DecFalse; EApply H; XDEAuto 1 ].
(* case 3.1.2: t0 <> t2 *)
      DecFalse; EApply H; XAuto.
(* case 3.2: t <> t1 *)
      DecFalse; EApply H3; XAuto.
      Qed.

      Lemma binder_dec: (t:?) (EX b w u | t = (THead (Bind b) w u)) \/
                        (b:?; w,u:?) (t = (THead (Bind b) w u) -> (P:Prop) P).
      Proof.
      XElim t.
(* case 1: TSort *)
      Right; Intros; XInv.
(* case 2: TLRef *)
      Right; Intros; XInv.
(* case 3: THead *)
      NewInduction k.
(* case 3.1: Bind *)
      XDEAuto 3.
(* case 3.2: Flat *)
      Right; Intros; XInv.
      Qed.

      Lemma abst_dec: (u,v:?) (EX t | u = (THead (Bind Abst) v t)) \/
                      ((t:?) u = (THead (Bind Abst) v t) -> (P:Prop) P).
      Proof.
      XElim u; Intros.
(* case 1: TSort *)
      Right; Intros; XInv.
(* case 2: TLRef *)
      Right; Intros; XInv.
(* case 3: THead *)
      XDecomPose '(kind_dec k (Bind Abst)); Subst.
(* case 3.1: k = (Bind Abst) *)
      XDecomPose '(term_dec t v); Subst.
(* case 3.1.1: t = v *)
      XDEAuto 3.
(* case 3.1.2: t <> v *)
      Right; Intros; XInv; EApply H1; XAuto.
(* case 3.2: k <> (Bind Abst) *)
      Right; Intros; XInv; EApply H1; XAuto.
      Qed.

      Lemma thead_x_y_y: (k:?; v,t:?) (THead k v t) = t -> (P:Prop) P.
      Proof.
      XElim t; Intros; XInv.
(* case 3: THead *)
      Rewrite H2 in H0; Rewrite H3 in H0; Clear H H2 H3 k v. (**)
      EApply H0; XDEAuto 2.
      Qed.

   End terms_props.

      Hints Resolve not_abbr_abst not_void_abst
                    not_abbr_void not_abst_void : ld.

      Tactic Definition TInvBase := (
         Match Context With
            | [ _: (THead ? ? ?0) = ?0 |- ? ] ->
               EApply thead_x_y_y; XDEAuto 2
         ).

   Section s_props. (********************************************************)

      Lemma s_S: (k:?; i:?) (s k (S i)) = (S (s k i)).
      Proof.
      XElim k; XAuto.
      Qed.

      Lemma s_plus: (k:?; i,j:?) (s k (plus i j)) = (plus (s k i) j).
      Proof.
      XElim k; XAuto.
      Qed.

      Lemma s_plus_sym: (k:?; i,j:?) (s k (plus i j)) = (plus i (s k j)).
      Proof.
      XElim k; [ Intros; Simpl; Rewrite plus_n_Sm | Idtac ]; XAuto.
      Qed.

      Lemma s_minus: (k:?; i,j:?) (le j i) ->
                       (s k (minus i j)) = (minus (s k i) j).
      Proof.
      XElim k; [ Intros; Unfold s; Cbv Iota | XAuto ].
      Rewrite minus_Sn_m; XAuto.
      Qed.

      Lemma minus_s_s: (k:?; i,j:?) (minus (s k i) (s k j)) = (minus i j).
      Proof.
      XElim k; XAuto.
      Qed.

      Lemma s_le: (k:?; i,j:?) (le i j) -> (le (s k i) (s k j)).
      Proof.
      XElim k; Simpl; XAuto.
      Qed.

      Lemma s_lt: (k:?; i,j:?) (lt i j) -> (lt (s k i) (s k j)).
      Proof.
      XElim k; Simpl; XAuto.
      Qed.

      Hints Resolve eq_add_S : ld.

      Lemma s_inj: (k:?; i,j:?) (s k i) = (s k j) -> i = j.
      Proof.
      XElim k; XDEAuto 2.
      Qed.

      Hints Resolve le_S_n : ld.

      Lemma s_le_gen: (k:?; i,j:?) (le (s k i) (s k j)) -> (le i j).
      Proof.
      XElim k; XAuto.
      Qed.

      Lemma s_lt_gen: (k:?; i,j:?) (lt (s k i) (s k j)) -> (lt i j).
      Proof.
      XElim k; XAuto.
      Qed.

      Lemma s_inc: (k:?; i:?) (le i (s k i)).
      Proof.
      XElim k; XAuto.
      Qed.

   End s_props.

      Hints Resolve s_le s_lt s_inc : ld.

      Tactic Definition SRw :=
         Repeat (Rewrite s_S Orelse Rewrite s_plus_sym).

      Tactic Definition SRwIn H :=
         Repeat (Rewrite s_S in H Orelse Rewrite s_plus in H).

      Tactic Definition SRwBack :=
         Repeat (Rewrite <- s_S Orelse Rewrite <- s_plus Orelse Rewrite <- s_plus_sym Orelse Rewrite <- s_minus).

      Tactic Definition SRwBackIn H :=
         Repeat (Rewrite <- s_S in H Orelse Rewrite <- s_plus in H Orelse Rewrite <- s_plus_sym in H).

      Tactic Definition SGen := (
         Match Context With
            | [ H: (s ?0 ?) = (s ?0 ?) |- ? ] ->
               XPoseClear H '(s_inj ? ? ? H); Subst
            | [ H: (le (s ?0 ?) (s ?0 ?)) |- ? ] ->
               XPoseClear H '(s_le_gen ? ? ? H)
            | [ H: (lt (s ?0 ?) (s ?0 ?)) |- ? ] ->
               XPoseClear H '(s_lt_gen ? ? ? H)
         ).

   Section s_arith. (********************************************************)

      Lemma s_arith0: (k:?; i:?) (minus (s k i) (s k (0))) = i.
      Proof.
      Intros; Rewrite minus_s_s; Rewrite <- minus_n_O; XAuto.
      Qed.

      Lemma s_arith1: (b:?; i:?) (minus (s (Bind b) i) (1)) = i.
      Proof.
      Intros; Simpl; Rewrite <- minus_n_O; XAuto.
      Qed.

   End s_arith.