(****************************************************************************) (* *) (* 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 getl_defs. Require Export pr0_defs. Inductive pr2: C -> T -> T -> Prop := | pr2_free : (c:?; t1,t2:?) (pr0 t1 t2) -> (pr2 c t1 t2) | pr2_delta: (c,d:?; u:?; i:?) (getl i c (CHead d (Bind Abbr) u)) -> (t1,t2:?) (pr0 t1 t2) -> (t:?) (subst0 i u t2 t) -> (pr2 c t1 t). Hint pr2 : ld := Constructors pr2. Section pr2_gen_base. (***************************************************) Lemma pr2_gen_sort: (c:?; x:?; n:?) (pr2 c (TSort n) x) -> x = (TSort n). Proof. Intros; InsertEq H '(TSort n); XElim H; Clear c y x; Intros; Subst; Pr0GenBase; Subst; [ XAuto | Subst0GenBase ]. Qed. Lemma pr2_gen_lref: (c:?; x:?; n:?) (pr2 c (TLRef n) x) -> x = (TLRef n) \/ (EX d u | (getl n c (CHead d (Bind Abbr) u)) & x = (lift (S n) (0) u) ). Proof. Intros; InsertEq H '(TLRef n); XElim H; Clear c y x; Intros; Subst; Pr0GenBase; Subst; [ XAuto | Subst0GenBase; Subst; XDEAuto 3 ]. Qed. Hint discr : ld := Extern 4 (getl ? ? ?) Simpl. Lemma pr2_gen_abst: (c:?; u1,t1,x:?) (pr2 c (THead (Bind Abst) u1 t1) x) -> (EX u2 t2 | x = (THead (Bind Abst) u2 t2) & (pr2 c u1 u2) & (b:?; u:?) (pr2 (CHead c (Bind b) u) t1 t2) ). Proof. Intros; InsertEq H '(THead (Bind Abst) u1 t1); XElim H; Clear c y x; Intros; Subst; Pr0GenBase; Subst; [ XDEAuto 4 | Subst0GenBase; Subst; XDEAuto 6 ]. Qed. Lemma pr2_gen_cast: (c:?; u1,t1,x:?) (pr2 c (THead (Flat Cast) u1 t1) x) -> (EX u2 t2 | x = (THead (Flat Cast) u2 t2) & (pr2 c u1 u2) & (pr2 c t1 t2) ) \/ (pr2 c t1 x). Proof. Intros; InsertEq H '(THead (Flat Cast) u1 t1); XElim H; Clear c y x; Intros; Subst; Pr0GenBase; Subst; Try Subst0GenBase; XDEAuto 5. Qed. Lemma pr2_gen_csort: (t1,t2:?; n:?) (pr2 (CSort n) t1 t2) -> (pr0 t1 t2). Proof. Intros; InsertEq H '(CSort n); XElim H; Clear y t1 t2; Intros; Subst; [ XAuto | GetLGenBase ]. Qed. Lemma pr2_gen_ctail: (k:?; c:?; u,t1,t2:?) (pr2 (CTail k u c) t1 t2) -> (pr2 c t1 t2) \/ (EX t | k = (Bind Abbr) & (pr0 t1 t) & (subst0 (clen c) u t t2) ). Proof. Intros; InsertEq H '(CTail k u c); XElim H; Clear y t1 t2; Intros; Subst; Try GetLXGenBase; XDEAuto 3. Qed. End pr2_gen_base. Tactic Definition Pr2GenBase := ( Match Context With | [ H: (pr2 ?1 (TSort ?2) ?3) |- ? ] -> LApply (pr2_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ] | [ H: (pr2 ?1 (TLRef ?2) ?3) |- ? ] -> LApply (pr2_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (pr2 ?1 (THead (Bind Abst) ?2 ?3) ?4) |- ? ] -> LApply (pr2_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (pr2 ?1 (THead (Flat Cast) ?2 ?3) ?4) |- ? ] -> LApply (pr2_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (pr2 (CSort ?) ? ?) |- ? ] -> XPoseClear H '(pr2_gen_csort ? ? ? H) | [ H: (pr2 (CTail ? ? ?) ? ?) |- ? ] -> XDecomPoseClear H '(pr2_gen_ctail ? ? ? ? ? H) ). Section pr2_props. (******************************************************) Lemma pr2_thin_dx: (c:?; t1,t2:?) (pr2 c t1 t2) -> (u:?; f:?) (pr2 c (THead (Flat f) u t1) (THead (Flat f) u t2)). Proof. Intros; XElim H; XDEAuto 4. Qed. Lemma pr2_head_1: (c:?; u1,u2:?) (pr2 c u1 u2) -> (k:?; t:?) (pr2 c (THead k u1 t) (THead k u2 t)). Proof. Intros; XElim H; XDEAuto 4. Qed. Lemma pr2_head_2: (c:?; u,t1,t2:?; k:?) (pr2 (CHead c k u) t1 t2) -> (pr2 c (THead k u t1) (THead k u t2)). Proof. Intros; InsertEq H '(CHead c k u); XElim H; Clear y t1 t2. (* case 1: pr2_free *) XAuto. (* case 2: pr2_delta *) XElim k; XElim i; Intros; Subst; GetLGenBase; Try ClearGenBase; XInv; Subst; XDEAuto 4. (* case 2.3: Flat, i = 0 *) EApply pr2_delta with d:=d; [ Idtac | Idtac | EApply subst0_snd; Simpl; XDEAuto 2 ]; XDEAuto 2. Qed. Hints Resolve clear_getl_trans : ld. Lemma clear_pr2_trans: (c2:?; t1,t2:?) (pr2 c2 t1 t2) -> (c1:?) (clear c1 c2) -> (pr2 c1 t1 t2). Proof. Intros until 1; XElim H; Clear c2 t1 t2; [ XAuto | XDEAuto 3 ]. Qed. Lemma pr2_cflat: (c:?; t1,t2:?) (pr2 c t1 t2) -> (f:?; v:?) (pr2 (CHead c (Flat f) v) t1 t2). Proof. Intros; XElim H; Clear c t1 t2; XDEAuto 3. Qed. Lemma pr2_ctail: (c:?; t1,t2:?) (pr2 c t1 t2) -> (k:?; u:?) (pr2 (CTail k u c) t1 t2). Proof. Intros; XElim H; Clear c t1 t2; XDEAuto 3. Qed. Lemma pr2_change: (b:?) ~b=Abbr -> (c:?; v1,t1,t2:?) (pr2 (CHead c (Bind b) v1) t1 t2) -> (v2:?) (pr2 (CHead c (Bind b) v2) t1 t2). Proof. Intros; InsertEq H0 '(CHead c (Bind b) v1). XElim H0; Clear y t1 t2; Intros; Subst. (* case 1: pr2_free *) XAuto. (* case 2: pr2_delta *) NewInduction i; [ Idtac | Clear IHi ]. (* case 2.1: i = 0 *) GetLGenBase; ClearGenBase; XInv; Subst; EqFalse. (* case 2.1: i > 0 *) GetLGenBase; XDEAuto 3. Qed. End pr2_props. Hints Resolve pr2_thin_dx pr2_head_1 pr2_head_2 pr2_cflat pr2_ctail : ld. Section more_pr2_gen_base. (**********************************************) Lemma pr2_gen_cbind: (b:?; c:?; v,t1,t2:?) (pr2 (CHead c (Bind b) v) t1 t2) -> (pr2 c (THead (Bind b) v t1) (THead (Bind b) v t2)). Proof. Intros; InsertEq H '(CHead c (Bind b) v); XElim H; Clear y t1 t2. (* case 1: pr2_free *) XAuto. (* case 2: pr2_delta *) Intros; Subst; GetLXGenBase; XInv; Subst; XDEAuto 4. Qed. Lemma pr2_gen_cflat: (f:?; c:?; v,t1,t2:?) (pr2 (CHead c (Flat f) v) t1 t2) -> (pr2 c t1 t2). Proof. Intros; InsertEq H '(CHead c (Flat f) v); XElim H; Clear y t1 t2. (* case 1: pr2_free *) XAuto. (* case 2: pr2_delta *) Intros; Subst; GetLXGenBase; XDEAuto 3. Qed. End more_pr2_gen_base. Tactic Definition Pr2XGenBase := ( Match Context With | [ H: (pr2 (CHead ? (Bind ?) ?) ? ?) |- ? ] -> XPoseClear H '(pr2_gen_cbind ? ? ? ? ? H) | [ H: (pr2 (CHead ? (Flat ?) ?) ? ?) |- ? ] -> XPoseClear H '(pr2_gen_cflat ? ? ? ? ? H) | [ |- ? ] -> Pr2GenBase ).