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

      Fixpoint lweight [a:A] : nat :=
         Cases a of
            | (ASort _ _)   => (0)
            | (AHead a1 a2) => (S (plus (lweight a1) (lweight a2)))
         end.

      Definition llt : A -> A -> Prop :=
         [a1,a2:?](lt (lweight a1) (lweight a2)).

   Section lweight_props. (**************************************************)

      Lemma lweight_repl: (g:?; a1,a2:?) (leq g a1 a2) ->
                          (lweight a1) = (lweight a2).
      Proof.
      Intros; XElim H; Simpl; XAuto.
      Qed.

   End lweight_props.

   Section llt_props. (******************************************************)

      Lemma llt_repl: (g:?; a1,a2:?) (leq g a1 a2) ->
                      (a3:?) (llt a1 a3) -> (llt a2 a3).
      Proof.
      Unfold llt; Intros.
      Rewrite (lweight_repl ? ? ? H) in H0; XAuto.
      Qed.

      Hints Resolve lt_trans : ld.

      Theorem llt_trans: (a1,a2,a3:?) (llt a1 a2) -> (llt a2 a3) -> (llt a1 a3).
      Proof.
      Unfold llt; XDEAuto 2.
      Qed.

      Lemma llt_head_sx: (a1,a2:?) (llt a1 (AHead a1 a2)).
      Proof.
      Unfold llt; Simpl; XAuto.
      Qed.

      Lemma llt_head_dx: (a1,a2:?) (llt a2 (AHead a1 a2)).
      Proof.
      Unfold llt; Simpl; XAuto.
      Qed.

   End llt_props.

      Hints Resolve llt_head_sx llt_head_dx : ld.

   Section llt_wf. (*********************************************************)

      Local Q: (A -> Prop) -> nat -> Prop :=
         [P,n:?] (a:?) (lweight a) = n -> (P a).

      Remark q_ind: (P:A->Prop)((n:?) (Q P n)) -> (a:?) (P a).
      Proof.
      Unfold Q; Intros.
      Apply (H (lweight a) a); XAuto.
      Qed.

      Lemma llt_wf_ind: (P:A->Prop)
                        ((a2:?)((a1:?)(llt a1 a2) -> (P a1)) -> (P a2)) ->
                        (a:?)(P a).
      Proof.
      Unfold llt; Intros.
      XElimUsing q_ind a; 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 llt_wf.