(****************************************************************************)
(*                                                                          *)
(*                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 bg_tactics.
Require Export bg_subst.
Require Export bg_types.

   Section bg_hints. (* missing in the standard library *********************)

      Lemma nat_dec: (n1,n2:nat) n1 = n2 \/ (n1 = n2 -> (P:Prop) P).
      Proof.
      XElim n1; XElim n2; Intros;
      Try Solve [ DecFalse ].
(* case 1: O *)
      XAuto.
(* case 2: S *)
      Elim (H n0); Clear H; Intros; Subst;
      [ XAuto | DecFalse; EApply H; XDEAuto 1 ].
      Qed.

      Lemma simpl_plus_r: (n,m,p:?) (plus m n) = (plus p n) -> m = p.
      Proof.
      Intros.
      Apply (simpl_plus_l n).
      Rewrite plus_sym.
      Rewrite H; XAuto.
      Qed.

      Lemma minus_Sx_Sy: (x,y:?) (minus (S x) (S y)) = (minus x y).
      Proof.
      XAuto.
      Qed.

      Lemma minus_plus_r: (m,n:?) (minus (plus m n) n) = m.
      Proof.
      Intros.
      Rewrite plus_sym.
      Apply minus_plus.
      Qed.

      Lemma plus_permute_2_in_3: (x,y,z:?) (plus (plus x y) z) = (plus (plus x z) y).
      Proof.
      Intros.
      Rewrite plus_assoc_r.
      Rewrite (plus_sym y z).
      Rewrite <- plus_assoc_r; XAuto.
      Qed.

      Lemma plus_permute_2_in_3_assoc: (n,h,k:?) (plus (plus n h) k) = (plus n (plus k h)).
      Proof.
      Intros.
      Rewrite plus_permute_2_in_3; Rewrite plus_assoc_l; XAuto.
      Qed.

      Lemma plus_O: (x,y:?) (plus x y) = (0) -> x = (O) /\ y = (O).
      Proof.
      XElim x; [ XAuto | Intros; Inversion H0 ].
      Qed.

      Lemma minus_Sx_SO: (x:?) (minus (S x) (1)) = x.
      Proof.
      Intros; Simpl; Rewrite <- minus_n_O; XAuto.
      Qed.

      Hints Resolve sym_not_eq : ld.

      Lemma nat_dec_neg: (i,j:nat) ~i=j \/ i=j.
      Proof.
      XElim i; XElim j; Intros; XAuto.
      Elim (H n0); Clear H; XAuto.
      Qed.

      Lemma neq_eq_e: (i,j:nat; P:Prop) (~i=j -> P) -> (i=j -> P) -> P.
      Proof.
      Intros.
      Pose (nat_dec_neg i j).
      XElim o; XAuto.
      Qed.

      Hints Resolve le_S_n : ld.

      Lemma le_false: (m,n:?; P:Prop) (le m n) -> (le (S n) m) -> P.
      Proof.
      XElim m.
(* case 1 : m = 0 *)
      Intros; Inversion H0.
(* case 2 : m > 0 *)
      XElim n0; Intros.
(* case 2.1 : n = 0 *)
      Inversion H0.
(* case 2.2 : n > 0 *)
      Simpl in H1.
      Apply (H n0); XAuto.
      Qed.

      Lemma le_Sx_x: (x:?) (le (S x) x) -> (P:Prop) P.
      Proof.
      Intros; XPose H0 'le_Sn_n; Unfold not in H0.
      Apply False_ind; XDEAuto 2.
      Qed.

      Hints Resolve le_trans : ld.

      Lemma le_n_pred: (n,m:?) (le n m) -> (le (pred n) (pred m)).
      Proof.
      Intros; XElim H; Clear m; Intros; Simpl; XDEAuto 2.
      Qed.

      Lemma minus_le: (x,y:?) (le (minus x y) x).
      Proof.
      XElim x; [ XAuto | XElim y; Simpl; XDEAuto 2 ].
      Qed.

      Lemma le_plus_minus_sym: (n,m:?) (le n m) -> m = (plus (minus m n) n).
      Proof.
      Intros.
      Rewrite plus_sym; Apply le_plus_minus; XAuto.
      Qed.

      Lemma le_minus_minus: (x,y:?) (le x y) -> (z:?) (le y z) ->
                            (le (minus y x) (minus z x)).
      Proof.
      Intros.
      EApply simpl_le_plus_l.
      Rewrite le_plus_minus_r; [ Idtac | XAuto ].
      Rewrite le_plus_minus_r; XDEAuto 2.
      Qed.

      Hints Resolve sym_eq : ld.

      Lemma le_minus_plus: (z,x:?) (le z x) -> (y:?)
                           (minus (plus x y) z) = (plus (minus x z) y).
      Proof.
      XElim z.
(* case 1 : z = 0 *)
      Intros x H; Inversion H; XAuto.
(* case 2 : z > 0 *)
      Intros z; XElim x; Intros.
(* case 2.1 : x = 0 *)
      Inversion H0.
(* case 2.2 : x > 0 *)
      Simpl; XAuto.
      Qed.

      Lemma le_minus: (x,z,y:?) (le (plus x y) z) -> (le x (minus z y)).
      Proof.
      Intros.
      Rewrite <- (minus_plus_r x y); XAuto.
      Apply le_minus_minus; XAuto.
      Qed.

      Lemma le_trans_plus_r: (x,y,z:?) (le (plus x y) z) -> (le y z).
      Proof.
      Intros.
      EApply le_trans; [ EApply le_plus_r | Idtac ]; XDEAuto 2.
      Qed.

      Lemma lt_x_O: (x:?) (lt x O) -> (P:Prop) P.
      Proof.
      Unfold lt; Intros.
      XPoseClear H '(le_n_O_eq ? H); Subst; XInv.
      Qed.

      Lemma le_gen_S: (m,x:?) (le (S m) x) ->
                      (EX n | x = (S n) & (le m n)).
      Proof.
      Intros; Inversion H; XDEAuto 4.
      Qed.

      Lemma lt_x_plus_x_Sy: (x,y:?) (lt x (plus x (S y))).
      Proof.
      Intros; Rewrite plus_sym; Simpl; XAuto.
      Qed.

      Lemma simpl_lt_plus_r: (p,n,m:?) (lt (plus n p) (plus m p)) -> (lt n m).
      Proof.
      Intros.
      EApply simpl_lt_plus_l.
      Rewrite plus_sym in H; Rewrite (plus_sym m p) in H; Apply H.
      Qed.

      Lemma minus_x_Sy: (x,y:?) (lt y x) ->
                        (minus x y) = (S (minus x (S y))).
      Proof.
      XElim x.
(* case 1 : x = 0 *)
      Intros; Inversion H.
(* case 2 : x > 0 *)
      XElim y; Intros; Simpl.
(* case 2.1 : y = 0 *)
      Rewrite <- minus_n_O; XAuto.
(* case 2.2 : y > 0 *)
      Cut (lt n0 n); XAuto.
      Qed.

      Lemma lt_plus_minus: (x,y:?) (lt x y) ->
                           y = (S (plus x (minus y (S x)))).
      Proof.
      Intros.
      Apply (le_plus_minus (S x) y); XAuto.
      Qed.

      Lemma lt_plus_minus_r: (x,y:?) (lt x y) ->
                             y = (S (plus (minus y (S x)) x)).
      Proof.
      Intros.
      Rewrite plus_sym; Apply lt_plus_minus; XAuto.
      Qed.

      Lemma minus_x_SO: (x:?) (lt (0) x) -> x = (S (minus x (1))).
      Proof.
      Intros.
      Rewrite <- minus_x_Sy; [ Rewrite <- minus_n_O; XDEAuto 2 | XDEAuto 2 ].
      Qed.

      Lemma le_x_pred_y: (y,x:?) (lt x y) -> (le x (pred y)).
      Proof.
      XElim y; Intros; Simpl.
(* case 1: y = 0 *)
      Inversion H.
(* case 1: y > 0 *)
      XAuto.
      Qed.

      Lemma lt_le_minus: (x,y:?) (lt x y) -> (le x (minus y (1))).
      Proof.
      Intros; Apply le_minus; Rewrite plus_sym; Simpl; XAuto.
      Qed.

      Lemma lt_le_e: (n,d:?; P:Prop)
                     ((lt n d) -> P) -> ((le d n) -> P) -> P.
      Proof.
      Intros.
      Cut (le d n) \/ (lt n d); [ Intros H1; XElim H1; XAuto | Apply le_or_lt ].
      Qed.

      Lemma lt_eq_e: (x,y:?; P:Prop) ((lt x y) -> P) ->
                     (x = y -> P) -> (le x y) -> P.
      Proof.
      Intros.
      LApply (le_lt_or_eq x y); [ Clear H1; Intros H1 | XAuto ].
      XElim H1; XAuto.
      Qed.

      Lemma lt_eq_gt_e: (x,y:?; P:Prop) ((lt x y) -> P) ->
                        (x = y -> P) -> ((lt y x) -> P) -> P.
      Proof.
      Intros.
      Apply (lt_le_e x y); [ XAuto | Intros ].
      Apply (lt_eq_e y x); XAuto.
      Qed.

      Lemma lt_gen_xS: (x,n:?) (lt x (S n)) ->
                       x = (0) \/ (EX m | x = (S m) & (lt m n)).
      Proof.
      XElim x; XDEAuto 5.
      Qed.

      Lemma le_lt_false: (x,y:?) (le x y) -> (lt y x) -> (P:Prop) P.
      Proof.
      Intros.
      LApply (le_not_lt x y); [ Clear H; Intros H | XAuto ].
      Unfold not in H; Elim (H H0).
      Qed.

      Lemma lt_neq: (x,y:?) (lt x y) -> ~x=y.
      Proof.
      Unfold not; Intros; Rewrite H0 in H; Clear H0 x.
      LApply (lt_n_n y); XAuto.
      Qed.

      Lemma arith0: (h2,d2,n:?) (le (plus d2 h2) n) ->
                    (h1:?) (le (plus d2 h1) (minus (plus n h1) h2)).
      Proof.
      Intros.
      Rewrite <- (minus_plus h2 (plus d2 h1)).
      Apply le_minus_minus; [ XAuto | Idtac ].
      Rewrite plus_assoc_l; Rewrite (plus_sym h2 d2); XAuto.
      Qed.

   End bg_hints.

      Hints Resolve minus_plus_r
                    plus_permute_2_in_3 plus_permute_2_in_3_assoc : ld.

      Hints Resolve le_minus_minus minus_le le_n_pred arith0 : ld.

      Hints Resolve lt_x_plus_x_Sy : ld.

      Tactic Definition EqFalse := (
         Match Context With
            | [ H: ~?1=?1 |- ? ] ->
               LApply H; [ Clear H; Intros H; Inversion H | XAuto ]
      ).

      Tactic Definition PlusO := (
         Match Context With
            | [ H: (plus ?0 ?1) = (0) |- ? ] ->
               LApply (plus_O ?0 ?1); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (0) = (plus ?0 ?1) |- ? ] ->
               LApply (plus_O ?0 ?1); [ Clear H; Intros H | Apply sym_equal; XAuto ];
               XElim H; Intros
      ).

      Tactic Definition SymEqual := (
         Match Context With
            | [ H: ?1 = ?2 |- ? ] ->
               Cut ?2 = ?1; [ Clear H; Intros H | Apply sym_equal; XAuto ]
      ).

      Tactic Definition LeLtGen := (
         Match Context With
            | [ H: (le (0) ?) |-? ] -> Clear H
            | [ H: (lt (0) (S ?)) |-? ] -> Clear H
            | [ H0: (le ?1 ?2); H1: (lt ?2 ?1) |- ? ] ->
               EApply le_lt_false; [ Apply H0 | Apply H1 ]
            | [ H: (le (S ?) (S ?)) |- ? ] -> XPoseClear H '(le_S_n ? ? H)
            | [ H: (le (S ?1) ?2) |- ? ] ->
               LApply (le_gen_S ?1 ?2); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (lt (S ?1) (S ?2)) |- ? ] ->
               LApply (lt_S_n ?1 ?2); [ Clear H; Intros H | XAuto ]
            | [ H: (lt ?1 (S ?2)) |- ? ] ->
               LApply (lt_gen_xS ?1 ?2); [ Clear H; Intros H | XAuto ];
               XElim H; [ Intros | Intros H; XElim H; Intros ]
            | [ H: (le ? (0)) |- ? ] ->
               XPoseClear H '(le_n_O_eq ? H); Subst
            | [ H: (lt ? (0)) |- ? ] ->
               Apply (lt_x_O ? H)
      ).

   Section more_bg_hints. (**************************************************)

      Hints Resolve le_S_n : ld.

      Lemma O_minus: (x,y:?) (le x y) -> (minus x y) = (0).
      Proof.
      XElim x; Simpl.
(* case 1: x = 0 *)
      XAuto.
(* case 2: x > 0 *)
      Intros x; XElim y; Simpl; Intros.
(* case 2.1: y = 0 *)
      LeLtGen; XInv.
(* case 2.2: y > 0 *)
      XAuto.
      Qed.

      Lemma minus_minus: (z,x,y:?) (le z x) -> (le z y) ->
                         (minus x z) = (minus y z) -> x = y.
      Proof.
      XElim z.
(* case 1: z = 0 *)
      Intros; Repeat Rewrite <- minus_n_O in H1; XAuto.
(* case 2: z > 0 *)
      Intros z IH; XElim x.
(* case 2.1: x = 0 *)
      Intros; Clear H0 H1; LeLtGen; XInv.
(* case 2.2: x > 0 *)
      Intros x; Intros IHx; Clear IHx; XElim y.
(* case 2.2.1: y = 0 *)
      Intros; LeLtGen; LeLtGen;  XInv.
(* case 2.2.2: y > 0 *)
      Intros y; Intros IHy; Clear IHy; Intros.
      Simpl in H1; XAuto.
      Qed.

      Hints Resolve eq_add_S : ld.

      Lemma plus_plus: (z,x1,x2,y1,y2:?) (le x1 z) -> (le x2 z) ->
                       (plus (minus z x1) y1) = (plus (minus z x2) y2) ->
                       (plus x1 y2) = (plus x2 y1).
      Proof.
      XElim z.
(* case 1: z = 0 *)
      Simpl; Intros; Subst; Repeat LeLtGen; XAuto.
(* case 2: z > 0 *)
      Intros z IH; XElim x1.
(* case 2.1: x1 = 0 *)
      XElim x2; Simpl.
(* case 2.1.1: x2 = 0 *)
      Intros; Clear H H0; XPoseClear IH '(IH (0) (0)).
      Simpl in IH; Repeat Rewrite <- minus_n_O in IH; XAuto.
(* case 2.1.2: x2 > 0 *)
      Intros x2; Intros IHx2; Clear IHx2; Intros; Clear H.
      XPoseClear IH '(IH (0) x2 (S y1)).
      Simpl in IH; Rewrite <- minus_n_O in IH.
      Repeat Rewrite <- plus_n_Sm in IH; XAuto.
(* case 2.2: x1 > 0 *)
      Intros x1; Intros IHx1; Clear IHx1; XElim x2; Simpl.
(* case 2.2.1: x2 = 0 *)
      Intros; Clear H0; XPoseClear IH '(IH x1 (0) y1 (S y2)).
      Simpl in IH; Rewrite <- minus_n_O in IH.
      Repeat Rewrite <- plus_n_Sm in IH; XAuto.
(* case 2.2.2: x2 > 0 *)
      Intros x2; Intros IHx2; Clear IHx2; XAuto.
      Qed.

      Hints Resolve le_trans le_minus : ld.

      Lemma le_S_minus: (d,h,n:?) (le (plus d h) n) ->
                        (le d (S (minus n h))).
      Proof.
      Intros; Cut (le d n); Intros; [ Idtac | XDEAuto 2 ].
      Rewrite (le_plus_minus_sym h n) in H0; XDEAuto 3.
      Qed.

      Lemma lt_x_pred_y: (x,y:?) (lt x (pred y)) -> (lt (S x) y).
      Proof.
      XElim y; Simpl; Intros; [ LeLtGen | XAuto ].
      Qed.

   End more_bg_hints.