(****************************************************************************) (* *) (* 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 contexts_defs. Fixpoint tweight [t:T]: nat := Cases t of | (THead _ u t) => (S (plus (tweight u) (tweight t))) | _ => (1) end. Fixpoint cweight [c:C]: nat := Cases c of | (CSort _) => (0) | (CHead c _ t) => (plus (cweight c) (tweight t)) end. Definition tle: T -> T -> Prop := [t1,t2:?] (le (tweight t1) (tweight t2)). Definition clt: C -> C -> Prop := [c1,c2:?] (lt (cweight c1) (cweight c2)). Definition cle: C -> C -> Prop := [c1,c2:?] (le (cweight c1) (cweight c2)). Section tweight_props. (**************************************************) Lemma tweight_lt: (t:?) (lt (0) (tweight t)). Proof. XElim t; Simpl; XAuto. Qed. End tweight_props. Hints Resolve tweight_lt : ld. Section tle_props. (******************************************************) Lemma tle_r: (t:?) (tle t t). Proof. Unfold tle; XElim t; Simpl; XAuto. Qed. End tle_props. Hints Resolve tle_r : ld. Section cle_props. (******************************************************) Lemma cle_r: (c:?) (cle c c). Proof. Unfold cle; XElim c; Simpl; XAuto. Qed. Lemma cle_head: (c1,c2:?) (cle c1 c2) -> (u1,u2:?) (tle u1 u2) -> (k:?) (cle (CHead c1 k u1) (CHead c2 k u2)). Proof. Unfold cle tle; Simpl; XAuto. Qed. Lemma cle_trans_head: (c1,c2:?) (cle c1 c2) -> (k:?; u:?) (cle c1 (CHead c2 k u)). Proof. Unfold cle; Simpl; XAuto. Qed. End cle_props. Hints Resolve cle_r cle_head cle_trans_head : ld. Section clt_props. (******************************************************) Lemma clt_cong: (c,d:?) (clt c d) -> (k:?; t:?) (clt (CHead c k t) (CHead d k t)). Proof. Unfold clt; Simpl; XAuto. Qed. Lemma clt_head: (k:?; c:?; u:?) (clt c (CHead c k u)). Proof. Unfold clt; Intros; Simpl. Pattern 1 (cweight c); Rewrite (plus_n_O (cweight c)); XAuto. Qed. End clt_props. Hints Resolve clt_cong clt_head : ld. Section clt_wf. (*********************************************************) Local Q: (C -> Prop) -> nat -> Prop := [P,n:?] (c:?) (cweight c) = n -> (P c). Remark q_ind: (P:C->Prop)((n:?) (Q P n)) -> (c:?) (P c). Proof. Unfold Q; Intros. Apply (H (cweight c) c); XAuto. Qed. Lemma clt_wf_ind: (P:C->Prop) ((c:?)((d:?)(clt d c) -> (P d)) -> (P c)) -> (c:?)(P c). Proof. Unfold clt; Intros. XElimUsing q_ind c; 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 clt_wf.