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

(* NOTE: monomorphic lists of terms without implicit arguments *)

      Inductive TList: Set :=
         | TNil : TList
         | TCons: T -> TList -> TList.

      Fixpoint THeads [k:K; us:TList] : T -> T := [t:?] Cases us of
         | TNil         => t
         | (TCons u ul) => (THead k u (THeads k ul t))
      end.

      Fixpoint TApp [ts:TList] : T -> TList := [v:?] Cases ts of
         | TNil         => (TCons v TNil)
         | (TCons t ts) => (TCons t (TApp ts v))
      end.

      Fixpoint tslen [ts:TList] : nat := Cases ts of
         | TNil         => (0)
         | (TCons _ ts) => (S (tslen ts))
      end.

      Definition tslt: TList -> TList -> Prop :=
                 [ts1,ts2:?] (lt (tslen ts1) (tslen ts2)).

      Hint f2TTs : ld := Resolve (f_equal2 T TList).

   Section tslt_wf. (********************************************************)

      Local Q: (TList -> Prop) -> nat -> Prop :=
         [P,n:?] (ts:?) (tslen ts) = n -> (P ts).

      Remark q_ind: (P:TList->Prop)((n:?) (Q P n)) -> (ts:?) (P ts).
      Proof.
      Unfold Q; Intros.
      Apply (H (tslen ts) ts); XAuto.
      Qed.

      Lemma tslt_wf_ind: (P:TList->Prop)
                         ((ts2:?)((ts1:?)(tslt ts1 ts2) -> (P ts1)) -> (P ts2)) ->
                         (ts:?)(P ts).
      Proof.
      Unfold tslt; Intros.
      XElimUsing q_ind ts; 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 tslt_wf.

   Section tlist_props. (****************************************************)

      Lemma theads_tapp: (k:?; v,t:?; vs:?)
                         (THeads k (TApp vs v) t) = (THeads k vs (THead k v t)).
      Proof.
      XElim vs; Simpl; Intros; Try Rewrite <- H; XAuto.
      Qed.

      Lemma tcons_tapp_ex: (ts1:?; t1:?)
                           (EX ts2 t2 | (TCons t1 ts1) = (TApp ts2 t2) &
                                        (tslen ts1) = (tslen ts2)
                           ).
      Proof.
      XElim ts1; Simpl; Intros.
(* case 1: TNil *)
      Apply ex2_2_intro with x0:=TNil x1:=t1; XAuto.
(* case 2: TCons *)
      XDecomPoseClear H '(H t).
      Rewrite H0; Rewrite H1; Clear H0 H1.
      Apply ex2_2_intro with x0:=(TCons t1 x0) x1:=x1; XAuto.
      Qed.

      Lemma tlist_ind_rev: (P:TList->Prop) (P TNil) ->
                           ((ts:?; t:?)(P ts)->(P (TApp ts t))) ->
                           (ts:?) (P ts).
      Proof.
      XElimUsing tslt_wf_ind ts; XElim ts2; Intros.
(* case 1: TNil *)
      XAuto.
(* case 2: TCons *)
      XDecomPose '(tcons_tapp_ex t0 t); Rewrite H3; Clear H3.
      Apply H0; Apply H2.
      Unfold tslt; Rewrite <- H4; XAuto.
      Qed.

   End tlist_props.