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

      Definition fweight: C -> T -> nat :=
         [c,t:?] (plus (cweight c) (tweight t)).

      Definition flt: C -> T -> C -> T -> Prop :=
         [c1,t1,c2,t2:?] (lt (fweight c1 t1) (fweight c2 t2)).

   Section flt_props_base. (*************************************************)

      Lemma flt_thead_sx: (k:?; c:?; u,t:?) (flt c u c (THead k u t)).
      Proof.
      Unfold flt fweight; Simpl; XAuto.
      Qed.

      Lemma flt_thead_dx: (k:?; c:?; u,t:?) (flt c t c (THead k u t)).
      Proof.
      Unfold flt fweight; Simpl; XAuto.
      Qed.

      Lemma flt_shift: (k:?; c:?; u,t:?)
                       (flt (CHead c k u) t c (THead k u t)).
      Proof.
      Unfold flt fweight; Simpl; Intros.
      Rewrite <- plus_n_Sm; Rewrite plus_assoc_l; XAuto.
      Qed.

      Lemma flt_arith0: (k:?; c:?; t:?; i:?)
                        (flt c t (CHead c k t) (TLRef i)).
      Proof.
      Unfold flt fweight; Simpl; XAuto.
      Qed.

      Lemma flt_arith1: (k1:?; c1,c2:?; t1:?) (cle (CHead c1 k1 t1) c2) ->
                        (k2:?; t2:?; i:?)
                        (flt c1 t1 (CHead c2 k2 t2) (TLRef i)).
      Proof.
      Unfold cle flt fweight; Simpl; Intros.
      EApply le_lt_trans; [ Apply H | Idtac ].
      Rewrite plus_sym; Simpl; Apply le_lt_n_Sm; XAuto.
      Qed.

      Lemma flt_arith2: (c1,c2:?; t1:?; i:?) (flt c1 t1 c2 (TLRef i)) ->
                        (k2:?; t2:?; j:?)
                        (flt c1 t1 (CHead c2 k2 t2) (TLRef j)).
      Proof.
      Unfold flt fweight; Simpl; Intros.
      EApply lt_le_trans; [ Apply H | Idtac ].
      XAuto.
      Qed.

      Hints Resolve le_lt_trans : ld.

      Lemma cle_flt_trans: (c1,c2:?) (cle c1 c2) ->
                           (c3:?; u2,u3:?) (flt c2 u2 c3 u3) ->
                           (flt c1 u2 c3 u3).
      Proof.
      Unfold cle flt fweight; XDEAuto 3.
      Qed.

      Hints Resolve lt_trans : ld.

      Theorem flt_trans: (c1,c2:?; t1,t2:?) (flt c1 t1 c2 t2) ->
                         (c3:?; t3:?) (flt c2 t2 c3 t3) -> (flt c1 t1 c3 t3).
      Proof.
      Unfold flt; XDEAuto 2.
      Qed.

   End flt_props_base.

      Hints Resolve flt_thead_sx flt_thead_dx flt_shift
                    flt_arith0 flt_arith1 flt_arith2 : ld.

   Section flt_wf. (*********************************************************)

      Local Q: (C -> T -> Prop) -> nat -> Prop :=
         [P,n:?] (c:?; t:?) (fweight c t) = n -> (P c t).

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

      Lemma flt_wf_ind: (P:C->T->Prop)
                        ((c2:?; t2:?)((c1:?; t1:?)(flt c1 t1 c2 t2) -> (P c1 t1)) -> (P c2 t2)) ->
                        (c:?; t:?)(P c t).
      Proof.
      Unfold clt; Intros.
      Apply q_ind; Clear c t; Intros.
      Apply lt_wf_ind; Clear n; Intros.
      Unfold Q in H0; Unfold Q; Intros; Subst.
      Apply H; Intros; Unfold flt in H1; XDEAuto 2.
      Qed.

   End flt_wf.