(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require levels_defs. Definition gz: G := (Build_G S lt_n_Sn). Inductive leqz : A -> A -> Prop := | leqz_sort: (h1,h2,n1,n2:?) (plus h1 n2) = (plus h2 n1) -> (leqz (ASort h1 n1) (ASort h2 n2)) | leqz_head: (a1,a2:?) (leqz a1 a2) -> (a3,a4:?) (leqz a3 a4) -> (leqz (AHead a1 a3) (AHead a2 a4)). Hint leqz : ld := Constructors leqz. Section gz_props. (*******************************************************) Lemma aplus_gz_le: (k,h,n:?) (le h k) -> (aplus gz (ASort h n) k) = (ASort (0) (plus (minus k h) n)). Proof. XElim k; Simpl. (* case 1: k = 0 *) Intros; LeLtGen; XAuto. (* case 2: k > 0 *) Intros k IH; XElim h; Simpl; Intros. (* case 2.1: h = 0 *) Clear H; Rewrite <- aplus_asucc; Simpl. Rewrite (IH (0) (S n)); [ Clear IH | XAuto ]. Rewrite <- minus_n_O; Rewrite <- plus_n_Sm; XAuto. (* case 2.1: h > 0 *) Clear H; LeLtGen; XInv; Subst. Rewrite <- IH; [ Clear IH H0 | XAuto ]. Rewrite <- aplus_asucc; Simpl; XAuto. Qed. Lemma aplus_gz_ge: (n,k,h:?) (le k h) -> (aplus gz (ASort h n) k) = (ASort (minus h k) n). Proof. XElim k; Simpl. (* case 1: k = 0 *) Intros; Rewrite <- minus_n_O; XAuto. (* case 2: k > 0 *) Intros k IH; XElim h; Simpl; Intros; LeLtGen; XInv; Subst. (* case 2.2: h > 0 *) Clear H; Rewrite <- IH; [ Clear IH H1 | XAuto ]. Rewrite <- aplus_asucc; Simpl; XAuto. Qed. Lemma next_plus_gz: (n,h:?) (next_plus gz n h) = (plus h n). Proof. XElim h; Simpl; XAuto. Qed. End gz_props. Section leqz_props. (*****************************************************) Hints Resolve sym_eq le_S_n : ld. Lemma leqz_leq: (a1,a2:?) (leq gz a1 a2) -> (leqz a1 a2). Proof. Intros; XElim H; Intros. (* case 1: leq_sort *) Apply (lt_le_e k h1); Intros; Apply (lt_le_e k h2); Intros. (* case 1.1 h1 > k, h2 > k *) Rewrite aplus_gz_ge in H; [ Idtac | XAuto ]. Rewrite aplus_gz_ge in H; [ Idtac | XAuto ]. XInv; Subst; Replace h2 with h1; [ XAuto | Idtac ]. EApply minus_minus; Try Apply H2; XAuto. (* case 1.2 h1 > k, h2 <= k *) Rewrite aplus_gz_ge in H; [ Idtac | XAuto ]. Rewrite aplus_gz_le in H; [ Idtac | XAuto ]. Rewrite minus_x_Sy in H; [ XInv | XAuto ]. (* case 1.3 h1 <= k, h2 > k *) Rewrite aplus_gz_le in H; [ Idtac | XAuto ]. Rewrite aplus_gz_ge in H; [ Idtac | XAuto ]. SymEqual; Rewrite minus_x_Sy in H; [ XInv | XAuto ]. (* case 1.4 h1 <= k, h2 <= k *) Rewrite aplus_gz_le in H; [ Idtac | XAuto ]. Rewrite aplus_gz_le in H; [ Idtac | XAuto ]. XInv; XPoseClear H '(plus_plus ? ? ? ? ? H0 H1 H); XAuto. (* case 2: leq_head *) XAuto. Qed. Lemma leq_leqz: (a1,a2:?) (leqz a1 a2) -> (leq gz a1 a2). Proof. Intros; XElim H; Intros. (* case 1: leq_sort *) Apply leq_sort with k:=(plus h1 h2). Repeat Rewrite aplus_asort_simpl. Rewrite minus_plus; Rewrite minus_plus_r. Repeat Rewrite O_minus; XAuto. Repeat Rewrite next_plus_gz; XAuto. (* case 2: leq_head *) XAuto. Qed. End leqz_props.