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

      Definition wadd: (nat -> nat) -> nat -> (nat -> nat) :=
         [f,w,n:?] Cases n of | (0) => w | (S m) => (f m) end.

      Fixpoint weight_map [f:nat->nat; t:T] : nat := Cases t of
         | (TSort n)               => (0)
         | (TLRef n)               => (f n)
         | (THead (Bind Abbr) u t) =>
            (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f u))) t)))
         | (THead (Bind _) u t)    =>
            (S (plus (weight_map f u) (weight_map (wadd f (0)) t)))
         | (THead _ u t)           => (S (plus (weight_map f u) (weight_map f t)))
      end.

      Definition weight: T -> nat := (weight_map [_:?](0)).

      Definition tlt: T -> T -> Prop := [t1,t2:?](lt (weight t1) (weight t2)).

   Section wadd_props. (*****************************************************)

      Lemma wadd_le: (f,g:?) ((n:?) (le (f n) (g n))) -> (v,w:?) (le v w) ->
                     (n:?) (le (wadd f v n) (wadd g w n)).
      Proof.
      XElim n; Simpl; XAuto.
      Qed.

      Hints Resolve le_S_n : ld.

      Lemma wadd_lt: (f,g:?) ((n:?) (le (f n) (g n))) -> (v,w:?) (lt v w) ->
                     (n:?) (le (wadd f v n) (wadd g w n)).
      Proof.
      XElim n; Simpl; XAuto.
      Qed.

      Lemma wadd_O: (n:?) (wadd [_:?](0) (0) n) = (0).
      Proof.
      XElim n; XAuto.
      Qed.

   End wadd_props.

      Hints Resolve wadd_le wadd_lt : ld.

   Section weight_props. (***************************************************)

      Lemma weight_le : (t:?; f,g:?) ((n:?) (le (f n) (g n))) ->
                        (le (weight_map f t) (weight_map g t)).
      Proof.
      XElim t; [ XAuto | Simpl; XAuto | Idtac ].
      XElim k; Simpl; [ Idtac | XAuto ].
      XElim b; Auto 7 with ld. (**)
      Qed.

      Lemma weight_eq : (t:?; f,g:?) ((n:?) (f n) = (g n)) ->
                        (weight_map f t) = (weight_map g t).
      Proof.
      Intros; Apply le_antisym; Apply weight_le;
      Intros; Rewrite (H n); XAuto.
      Qed.

      Hints Resolve wadd_O weight_le weight_eq : ld.

      Lemma weight_add_O : (t:?) (weight_map (wadd [_:?](0) (0)) t) =
                                 (weight_map [_:?](0) t).
      Proof.
      XAuto.
      Qed.

      Lemma weight_add_S : (t:?; m:?) (le (weight_map (wadd [_:?](0) (0)) t)
                                          (weight_map (wadd [_:?](0) (S m)) t)
                                      ).
      Proof.
      XAuto.
      Qed.

   End weight_props.

      Hints Resolve weight_le weight_add_S : ld.

   Section tlt_props. (******************************************************)

      Hints Resolve lt_trans : ld.

      Theorem tlt_trans: (v,u,t:?) (tlt u v) -> (tlt v t) -> (tlt u t).
      Proof.
      Unfold tlt; XDEAuto 2.
      Qed.

      Lemma tlt_head_sx: (k:?; u,t:?) (tlt u (THead k u t)).
      Proof.
      Unfold tlt weight.
      XElim k; Simpl; [ XElim b | Idtac ]; XAuto.
      Qed.

      Lemma tlt_head_dx: (k:?; u,t:?) (tlt t (THead k u t)).
      Proof.
      Unfold tlt weight.
      XElim k; Simpl; [ Idtac | XAuto ].
      XElim b; Intros; Try Rewrite weight_add_O; [ Idtac | XAuto | XAuto ].
      EApply lt_le_trans; [ Apply lt_n_Sn | Apply le_n_S ].
      EApply le_trans; [ Rewrite <- (weight_add_O t); Apply weight_add_S | XAuto ].
      Qed.

   End tlt_props.

      Hints Resolve tlt_head_sx tlt_head_dx : ld.

   Section tlt_wf. (*********************************************************)

      Local Q: (T -> Prop) -> nat -> Prop :=
         [P,n:?] (t:?) (weight t) = n -> (P t).

      Remark q_ind: (P:T->Prop)((n:?) (Q P n)) -> (t:?) (P t).
      Proof.
      Unfold Q; Intros.
      Apply (H (weight t) t); XAuto.
      Qed.

      Lemma tlt_wf_ind: (P:T->Prop)
                        ((t:?)((v:?)(tlt v t) -> (P v)) -> (P t)) ->
                        (t:?)(P t).
      Proof.
      Unfold tlt; Intros.
      XElimUsing q_ind t; Intros.
      Apply lt_wf_ind; Clear n; Intros.
      Unfold Q in H0; Unfold Q; Intros.
      Rewrite <- H1 in H0; Clear H1.
      Apply H; XDEAuto 2.
      Qed.

   End tlt_wf.