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

      Inductive C: Set :=
         | CSort: nat -> C
         |  CHead: C -> K -> T -> C.

      Hint f3CKT : ld := Resolve (f_equal3 C K T).

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

      Fixpoint clen [c:C] : nat := Cases c of
         | (CSort _)     => (0)
         | (CHead c k _) => (s k (clen c))
      end.

   Section r_props. (********************************************************)

      Lemma r_S: (k:?; i:?) (r k (S i)) = (S (r k i)).
      Proof.
      XElim k; XAuto.
      Qed.

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

      Lemma r_plus_sym: (k:?; i,j:?) (r k (plus i j)) = (plus i (r k j)).
      Proof.
      XElim k; Intros; Simpl; XAuto.
      Qed.

      Hints Resolve minus_x_Sy : ld.

      Lemma r_minus: (i,n:?) (lt n i) ->
                     (k:?) (minus (r k i) (S n)) = (r k (minus i (S n))).
      Proof.
      XElim k; Intros; Simpl; XDEAuto 2.
      Qed.

      Lemma r_dis: (k:?; P:Prop)
                   (((i:?) (r k i) = i) -> P) ->
                   (((i:?) (r k i) = (S i)) -> P) -> P.
      Proof.
      XElim k; XAuto.
      Qed.

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

   End r_props.

      Tactic Definition RRw :=
         Repeat (Rewrite r_S Orelse Rewrite r_plus_sym).

      Tactic Definition RRwIn H :=
         Repeat (Rewrite r_S in H Orelse Rewrite r_plus in H).

      Tactic Definition RRwBackIn H :=
         Repeat (Rewrite <- r_S in H Orelse Rewrite <- r_plus in H).

   Section r_arith. (********************************************************)

      Lemma r_arith0: (k:?; i:?) (minus (r k (S i)) (1)) = (r k i).
      Proof.
      Intros; RRw; Rewrite minus_Sx_SO; XAuto.
      Qed.

      Lemma r_arith1: (k:?; i,j:?) (minus (r k (S i)) (S j)) = (minus (r k i) j).
      Proof.
      Intros; RRw; XAuto.
      Qed.

      Lemma r_arith2: (k:?; i,j:?) (le (S i) (s k j)) -> (le (r k i) j).
      Proof.
      XElim k; Simpl; Intros; [ LeLtGen | Idtac ]; XAuto.
      Qed.

      Lemma r_arith3: (k:?; i,j:?) (le (s k j) (S i)) -> (le j (r k i)).
      Proof.
      XElim k; Simpl; Intros; [ LeLtGen | Idtac ]; XAuto.
      Qed.

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

      Lemma r_arith5: (k:?; i,j:?) (lt (s k j) (S i)) -> (lt j (r k i)).
      Proof.
      XElim k; Simpl; Intros; [ LeLtGen | Idtac ]; XAuto.
      Qed.

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

      Hints Resolve eq_add_S : ld.

      Lemma r_arith7: (k:?; i,j:?) (S i) = (s k j) -> (r k i) = j.
      Proof.
      XElim k; Simpl; XAuto.
      Qed.

   End r_arith.

      Tactic Definition RArithGen := (
         Match Context With
            | [ H: (le (S ?) (s ? ?)) |- ? ] ->
               XPoseClear H '(r_arith2 ? ? ? H)
            | [ H: (le (s ? ?) (S ?)) |- ? ] ->
               XPoseClear H '(r_arith3 ? ? ? H)
            | [ H: (lt (s ? ?) (S ?)) |- ? ] ->
               XPoseClear H '(r_arith5 ? ? ? H)
            | [ H: (S ?) = (s ? ?) |- ? ] ->
               XPoseClear H '(r_arith7 ? ? ? H); Subst
         ).