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

      Inductive A : Set :=
         | ASort: nat -> nat -> A
         | AHead: A -> A -> A.

      Fixpoint asucc [g:G; l:A] : A :=
         Cases l of
            | (ASort (0) n)   => (ASort (0) (next g n))
            | (ASort (S h) n) => (ASort h n)
            | (*#* #xp *) (AHead a1 a2)   => (AHead a1 (*#* #xp *) (asucc g a2))
         end.

      Fixpoint aplus [g:G; a:A; n:nat] : A :=
         Cases n of
            | (0)               => a
            | (*#* #xp *) (S n) => (asucc g (*#* #xp *) (aplus g a n))
         end.

      Inductive leq [g:G] : A -> A -> Prop :=
         | leq_sort: (h1,h2,n1,n2,k:?)
                     (aplus g (ASort h1 n1) k) = (aplus g (ASort h2 n2) k) ->
                     (leq g (ASort h1 n1) (ASort h2 n2))
         | leq_head: (a1,a2:?) (leq g a1 a2) ->
                     (a3,a4:?) (leq g a3 a4) ->
                     (leq g (AHead a1 a3) (AHead a2 a4)).

      Hint leq : ld := Constructors leq.

      Hint f2GA : ld := Resolve (f_equal2 G A).

   Section leq_gen_base. (**************************************************)

      Lemma leq_gen_sort1: (g:?; h1,n1:?; a2:?) (leq g (ASort h1 n1) a2) ->
                           (EX n2 h2 k | (aplus g (ASort h1 n1) k) = (aplus g (ASort h2 n2) k) &
                                         a2 = (ASort h2 n2)
                           ).
      Proof.
      Intros; InsertEq H '(ASort h1 n1); XElim H; Clear y a2;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma leq_gen_head1: (g:?; a1,a2,a:?) (leq g (AHead a1 a2) a) ->
                           (EX a3 a4 | (leq g a1 a3) & (leq g a2 a4) &
                                       a = (AHead a3 a4)
                           ).
      Proof.
      Intros; InsertEq H '(AHead a1 a2); XElim H; Clear y a;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma leq_gen_sort2: (g:?; h1,n1:?; a2:?) (leq g a2 (ASort h1 n1)) ->
                           (EX n2 h2 k | (aplus g (ASort h2 n2) k) = (aplus g (ASort h1 n1) k) &
                                         a2 = (ASort h2 n2)
                           ).
      Proof.
      Intros; InsertEq H '(ASort h1 n1); XElim H; Clear a2 y;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma leq_gen_head2: (g:?; a1,a2,a:?) (leq g a (AHead a1 a2)) ->
                           (EX a3 a4 | (leq g a3 a1) & (leq g a4 a2) &
                                       a = (AHead a3 a4)
                           ).
      Proof.
      Intros; InsertEq H '(AHead a1 a2); XElim H; Clear a y;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

   End leq_gen_base.

      Tactic Definition LEqGenBase := (
         Match Context With
            | [ H: (leq ? (ASort ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(leq_gen_sort1 ? ? ? ? H); XInv; Subst
            | [ H: (leq ? (AHead ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(leq_gen_head1 ? ? ? ? H); XInv; Subst
            | [ H: (leq ? ? (ASort ? ?)) |- ? ] ->
               XDecomPoseClear H '(leq_gen_sort2 ? ? ? ? H); XInv; Subst
            | [ H: (leq ? ? (AHead ? ?)) |- ? ] ->
               XDecomPoseClear H '(leq_gen_head2 ? ? ? ? H); XInv; Subst
         ).

   Section asucc_gen_base. (*************************************************)

      Lemma asucc_gen_sort: (g:?; h,n:?; a:?) (ASort h n) = (asucc g a) ->
                            (EX h0 n0 | a = (ASort h0 n0)).
      Proof.
      XElim a; Intros; Simpl in H; XInv; XDEAuto 2.
      Qed.

      Lemma asucc_gen_head: (g:?; a1,a2,a:?) (AHead a1 a2) = (asucc g a) ->
                            (EX a0 | a = (AHead a1 a0) & a2 = (asucc g a0)).
      Proof.
      XElim a; Intros.
(* case 1: ASort *)
      NewInduction n; Simpl in H; XInv.
(* case 2: AHead *)
      Simpl in H1; XInv; Subst; XDEAuto 2.
      Qed.

   End asucc_gen_base.

      Tactic Definition ASuccGenBase := (
         Match Context With
            | [ _: (ASort ?1 ?2) = (asucc ?0 ?3) |- ? ] ->
               LApply (asucc_gen_sort ?0 ?1 ?2 ?3); [ Intros H_x | XAuto ];
               XDecompose H_x; Subst
            | [ H: (AHead ?1 ?2) = (asucc ?0 ?3) |- ? ] ->
               LApply (asucc_gen_head ?0 ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
               XDecompose H
         ).

   Section asucc_aplus_props. (**********************************************)

      Lemma aplus_reg_r: (g:?; a1,a2:?; h1,h2:?)
                         (aplus g a1 h1) = (aplus g a2 h2) -> (h:?)
                         (aplus g a1 (plus h h1)) = (aplus g a2 (plus h h2)).
      Proof.
      XElim h; Intros; Simpl; XAuto.
      Qed.

      Lemma aplus_assoc: (g:?; a:?; h1,h2:?)
                         (aplus g (aplus g a h1) h2) =
                         (aplus g a (plus h1 h2)).
      Proof.
      XElim h1; Simpl.
(* case 1: h1 = 0 *)
      XAuto.
(* case 2: h1 > 0 *)
      XElim h2; Simpl; Intros.
(* case 2.1: h2 = 0 *)
      Rewrite <- plus_n_O; XAuto.
(* case 2.1: h2 > 0 *)
      Rewrite <- plus_n_Sm; Simpl; XAuto.
      Qed.

      Lemma aplus_asucc: (g:?; h:?; a:?) (aplus g (asucc g a) h) = (asucc g (aplus g a h)).
      Proof.
      Intros; Fold (aplus g a (1)).
      Rewrite aplus_assoc; XAuto.
      Qed.

      Lemma aplus_sort_O_S_simpl: (g:?; n,k:?)
                                  (aplus g (ASort (0) n) (S k)) =
                                  (aplus g (ASort (0) (next g n)) k).
      Proof.
      Intros; Simpl; Rewrite <- aplus_asucc; Simpl; XAuto.
      Qed.

      Lemma aplus_sort_S_S_simpl: (g:?; n,h,k:?)
                                  (aplus g (ASort (S h) n) (S k)) =
                                  (aplus g (ASort h n) k).
      Proof.
      Intros; Simpl; Rewrite <- aplus_asucc; Simpl; XAuto.
      Qed.

      Lemma asucc_repl: (g:?; a1,a2:?)
                        (leq g a1 a2) -> (leq g (asucc g a1) (asucc g a2)).
      Proof.
      Intros; XElim H; Clear a1 a2; Intros; Simpl.
(* case 1: leq_sort *)
      NewInduction h1; NewInduction h2; EApply leq_sort with k:=k.
(* case 1.1: h1 = 0, h2 = 0 *)
      Repeat Rewrite <- aplus_sort_O_S_simpl; Simpl.
      Rewrite H; Clear H; XAuto.
(* case 1.2: h1 = 0, h2 > 0 *)
      Rewrite <- aplus_sort_O_S_simpl; Rewrite <- (aplus_sort_S_S_simpl g n2); Simpl.
      Rewrite H; Clear H; XAuto.
(* case 1.3: h1 > 0, h2 = 0 *)
      Rewrite <- aplus_sort_O_S_simpl; Rewrite <- aplus_sort_S_S_simpl; Simpl.
      Rewrite H; Clear H; XAuto.
(* case 1.4: h1 > 0, h2 > 0 *)
      Rewrite <- aplus_sort_S_S_simpl; Rewrite <- (aplus_sort_S_S_simpl g n2); Simpl.
      Rewrite H; Clear H; XAuto.
(* case 2: leq_head *)
      XAuto.
      Qed.

      Lemma asucc_inj: (g:?; a1,a2:?)
                       (leq g (asucc g a1) (asucc g a2)) -> (leq g a1 a2).
      Proof.
      XElim a1; XElim a2; Intros.
(* case 1: ASort, ASort *)
      NewInduction n; NewInduction n1; Simpl in H; Simpl; LEqGenBase.
(* case 1.1: n = 0, n1 = 0 *)
      Repeat Rewrite <- aplus_sort_O_S_simpl in H0; XDEAuto 2.
(* case 1.2: n = 0, n1 > 0 *)
      Rewrite <- aplus_sort_O_S_simpl in H0; Rewrite <- (aplus_sort_S_S_simpl g n2) in H0; XDEAuto 2.
(* case 1.3: n > 0, n1 = 0 *)
      Rewrite <- aplus_sort_S_S_simpl in H0; Rewrite <- aplus_sort_O_S_simpl in H0; XDEAuto 2.
(* case 1.4: n > 0, n1 > 0 *)
      Rewrite <- aplus_sort_S_S_simpl in H0; Rewrite <- (aplus_sort_S_S_simpl g n2) in H0; XDEAuto 2.
(* case 2: ASort, AHead *)
      NewInduction n; Simpl in H1; LEqGenBase.
(* case 3: AHead, ASort *)
      NewInduction n; Simpl in H1; LEqGenBase.
(* case 4: AHead, AHead *)
      Simpl in H3; LEqGenBase; XAuto.
      Qed.

      Lemma aplus_asort_O_simpl: (g:?; h:?; n:?)
                                 (aplus g (ASort (0) n) h) = (ASort (0) (next_plus g n h)).
      Proof.
      XElim h; Simpl; Intros.
(* case 1: h = 0 *)
      XAuto.
(* case 2: h > 0 *)
      Rewrite <- aplus_asucc; Simpl.
      Rewrite <- next_plus_next; XAuto.
      Qed.

      Hints Resolve le_S_n : ld.

      Lemma aplus_asort_le_simpl: (g:?; h,k,n:?) (le h k) ->
                                  (aplus g (ASort k n) h) = (ASort (minus k h) n).
      Proof.
      XElim h; Simpl.
(* case 1: h = 0 *)
      Intros; Rewrite <- minus_n_O; XAuto.
(* case 2: h > 0 *)
      Intros h; XElim k; Intros.
(* case 2.1: k = 0 *)
      LeLtGen; XInv.
(* case 2.2: k > 0 *)
      Rewrite <- aplus_asucc; Simpl; XAuto.
      Qed.

      Hints Resolve aplus_asort_O_simpl : ld.

      Lemma aplus_asort_simpl: (g:?; h,k,n:?)
                               (aplus g (ASort k n) h) = (ASort (minus k h) (next_plus g n (minus h k))).
      Proof.
      Intros; Apply (lt_le_e k h); Intros.
(* case 1: k < h *)
      Pattern 1 h; Rewrite (le_plus_minus k h); [ Idtac | XAuto ].
      Rewrite <- aplus_assoc.
      Rewrite aplus_asort_le_simpl; [ Idtac | XAuto ].
      Rewrite <- minus_n_n.
      Rewrite (O_minus k h); XAuto.
(* case 2: k >= h *)
      Rewrite aplus_asort_le_simpl; [ Idtac | XAuto ].
      Rewrite (O_minus h k); XAuto.
      Qed.

      Lemma aplus_ahead_simpl: (g:?; h:?; a1,a2:?)
                               (aplus g (AHead a1 a2) h) = (AHead a1 (aplus g a2 h)).
      Proof.
      XElim h; Simpl; Intros.
(* case h = 0 *)
      XAuto.
(* case 2: h > 0 *)
      Repeat Rewrite <- aplus_asucc; Simpl; XAuto.
      Qed.

      Lemma aplus_asucc_false: (g:?; a:?; h:?)
                               (aplus g (asucc g a) h) = a -> (P:Prop) P.
      Proof.
      XElim a; Simpl; Intros.
(* case 1; ASort *)
      NewInduction n.
(* case 1.1: n = 0 *)
      Rewrite aplus_asort_simpl in H; XInv.
      Rewrite <- minus_n_O in H.
      EApply le_lt_false with y:=n0;
      [ Apply le_n | Pattern 2 n0; Rewrite <- H; XAuto ].
(* case 1.2: n > 0 *)
      Rewrite aplus_asort_simpl in H; XInv.
      Apply (le_Sx_x n); Rewrite <- H0; XAuto.
(* case 2; AHead *)
      Rewrite aplus_ahead_simpl in H1; XInv.
      EApply H0; XDEAuto 2.
      Qed.

      Hints Resolve sym_eq : ld.

      Lemma aplus_inj: (g:?; h1,h2:?; a:?)
                       (aplus g a h1) = (aplus g a h2) -> h1 = h2.
      Proof.
      XElim h1; XElim h2; Simpl; Intros.
(* case 1: h1 = 0; h2 = 0 *)
      XAuto.
(* case 2: h1 = 0; h2 > 0 *)
      Rewrite <- aplus_asucc in H0.
      EApply aplus_asucc_false; XDEAuto 2.
(* case 2: h1 > 0; h2 = 0 *)
      Rewrite <- aplus_asucc in H0.
      EApply aplus_asucc_false; XDEAuto 2.
(* case 4: h1 > 0; h2 > 0 *)
      Repeat Rewrite <- aplus_asucc in H1; XDEAuto 3.
      Qed.

   End asucc_aplus_props.

      Hints Resolve asucc_repl : ld.

      Tactic Definition ASuccDis := (
         Match Context With
            | [ H: (leq ? (asucc ?0 ?1) (asucc ?0 ?2)) |- ? ] ->
               LApply (asucc_inj ?0 ?1 ?2); [ Clear H; Intros H | XAuto ];
               Subst
         ).

   Section leq_props. (******************************************************)

      Lemma ahead_inj_snd: (g:?; a1,a2,a3,a4:?)
                           (leq g (AHead a1 a2) (AHead a3 a4)) ->
                           (leq g a2 a4).
      Proof.
      Intros; LEqGenBase; XAuto.
      Qed.

      Lemma leq_refl: (g:?; a:?) (leq g a a).
      Proof.
      XElim a; Intros; [ Apply leq_sort with k:=(0) | Idtac ]; XAuto.
      Qed.

      Hints Resolve leq_refl : ld.

      Lemma leq_eq: (g:?; a1,a2:?) a1 = a2 -> (leq g a1 a2).
      Proof.
      Intros; Subst; XAuto.
      Qed.

      Lemma leq_asucc: (g:?; a:?) (EX a0 | (leq g a (asucc g a0))).
      Proof.
      XElim a; Intros.
(* case 1: leq_sort *)
      Apply ex_intro with x:=(ASort (S n) n0); Simpl; XAuto.
(* case 2: leq_head *)
      XDecompose H0; Apply ex_intro with x:=(AHead a x); Simpl; XAuto.
      Qed.

      Hints Resolve sym_eq : ld.

      Lemma leq_sym: (g:?; a1,a2:?) (leq g a1 a2) -> (leq g a2 a1).
      Proof.
      Intros; XElim H; Clear a1 a2; XDEAuto 3.
      Qed.

      Hints Resolve trans_eq le_trans : ld.

      Theorem leq_trans: (g:?; a1,a2:?) (leq g a1 a2) ->
                         (a3:?) (leq g a2 a3) -> (leq g a1 a3).
      Proof.
      Intros until 1; XElim H; Clear a1 a2;
      Intros; LEqGenBase.
(* case 1: leq_sort *)
      Apply (lt_le_e k x2); Intros.
(* case 1.1: k < k0 *)
      XPoseClear H '(aplus_reg_r ? ? ? ? ? H (minus x2 k)).
      Rewrite <- le_plus_minus_sym in H; XDEAuto 3.
(* case 1.2: k >= k0 *)
      XPoseClear H1 '(aplus_reg_r ? ? ? ? ? H1 (minus k x2)).
      Rewrite <- le_plus_minus_sym in H1; XDEAuto 3.
(* case 2: leq_head *)
      XDEAuto 4.
      Qed.

      Lemma leq_ahead_false_1: (g:?; a1,a2:?)
                               (leq g (AHead a1 a2) a1) -> (P:Prop) P.
      Proof.
      XElim a1; Simpl; Intros.
(* case 1; ASort *)
      NewInduction n; LEqGenBase.
(* case 2; AHead *)
      LEqGenBase; EApply H; XDEAuto 2.
      Qed.

      Lemma leq_ahead_false_2: (g:?; a2,a1:?)
                               (leq g (AHead a1 a2) a2) -> (P:Prop) P.
      Proof.
      XElim a2; Simpl; Intros.
(* case 1; ASort *)
      NewInduction n; LEqGenBase.
(* case 2; AHead *)
      LEqGenBase; EApply H0; XDEAuto 2.
      Qed.

      Lemma leq_ahead_asucc_false: (g:?; a1,a2:?)
                                   (leq g (AHead a1 a2) (asucc g a1)) ->
                                   (P:Prop) P.
      Proof.
      XElim a1; Simpl; Intros.
(* case 1; ASort *)
      NewInduction n; LEqGenBase.
(* case 2; AHead *)
      LEqGenBase; EApply leq_ahead_false_1; XDEAuto 2.
      Qed.

      Lemma leq_asucc_false: (g:?; a:?) (leq g (asucc g a) a) -> (P:Prop) P.
      Proof.
      XElim a; Simpl; Intros.
(* case 1: ASort *)
      NewInduction n; LEqGenBase.
(* case 1.1: n = 0 *)
      Rewrite <- aplus_sort_O_S_simpl in H0.
      XPoseClear H0 '(aplus_inj ? ? ? ? H0).
      Apply (le_Sx_x x2); Rewrite H0; XAuto.
(* case 1.2: n > 0 *)
      Rewrite <- aplus_sort_S_S_simpl in H0.
      XPoseClear H0 '(aplus_inj ? ? ? ? H0).
      Apply (le_Sx_x x2); Rewrite H0; XAuto.
(* case 2: AHead *)
      LEqGenBase; EApply H0; XDEAuto 2.
      Qed.

   End leq_props.

      Hints Resolve leq_refl leq_eq : ld.