(****************************************************************************) (* *) (* 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. Inductive aprem: nat -> A -> A -> Prop := | aprem_zero: (a1,a2:?) (aprem (0) (AHead a1 a2) a1) | aprem_succ: (a2,a:?; i:?) (aprem i a2 a) -> (a1:?) (aprem (S i) (AHead a1 a2) a). Hint aprem : ld := Constructors aprem. Section aprem_gen_base. (*************************************************) Lemma aprem_gen_sort: (x:?; i,h,n:?) (aprem i (ASort h n) x) -> False. Proof. Intros; InsertEq H '(ASort h n); XElim H; Clear i y x; Intros; XInv. Qed. Lemma aprem_gen_head_O: (a1,a2,x:?) (aprem (0) (AHead a1 a2) x) -> x = a1. Proof. Intros; InsertEq H '(AHead a1 a2); InsertEq H '(0); XElim H; Clear y y0 x; Intros; XInv; Subst; XInv; XAuto. Qed. Lemma aprem_gen_head_S: (a1,a2,x:?; i:?) (aprem (S i) (AHead a1 a2) x) -> (aprem i a2 x). Proof. Intros; InsertEq H '(AHead a1 a2); InsertEq H '(S i); XElim H; Clear y y0 x; Intros; XInv; Subst; XInv; Subst; XAuto. Qed. End aprem_gen_base. Tactic Definition APremGenBase := ( Match Context With | [ H: (aprem ? (ASort ? ?) ?) |- ? ] -> XDecomPose '(aprem_gen_sort ? ? ? ? H) | [ H: (aprem (0) (AHead ? ?) ?) |- ? ] -> XPoseClear H '(aprem_gen_head_O ? ? ? H); Subst | [ H: (aprem (S ?) (AHead ? ?) ?) |- ? ] -> XPoseClear H '(aprem_gen_head_S ? ? ? ? H) ). Section aprem_props. (****************************************************) Lemma aprem_repl: (g:?; a1,a2:?) (leq g a1 a2) -> (i:?; b2:?) (aprem i a2 b2) -> (EX b1 | (leq g b1 b2) & (aprem i a1 b1)). Proof. Intros until 1; XElim H; Intros. (* case 1: leq_sort *) APremGenBase. (* case 2: leq_head *) NewInduction i; APremGenBase. (* case 2.1: i = 0 *) XDEAuto 2. (* case 2.2: i > 0 *) Clear IHi; XDecomPose '(H2 ? ? H3); Clear H1 H2 H3; XDEAuto 3. Qed. Lemma aprem_asucc: (g:?; a1,a2:?; i:?) (aprem i a1 a2) -> (aprem i (asucc g a1) a2). Proof. Intros; XElim H; Intros; Simpl; XAuto. Qed. End aprem_props. Hints Resolve aprem_asucc : ld.