(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require pr2_gen. Require pr3_defs. Require pr3_props. Section pr3_gen_lift. (***************************************************) Hints Resolve pr3_sing : ld. (* NOTE: consider the generalization coming from nf2_lift *) Lemma pr3_gen_lift: (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) -> (e:?) (drop h d c e) -> (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)). Proof. Intros until 1; InsertEq H '(lift h d t1); UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4. (* case 1 : pr3_refl *) XDEAuto 2. (* case 2 : pr3_sing *) Rewrite H2 in H; Pr2Gen. LApply (H1 x); [ Clear H1; Intros H1 | XAuto ]. LApply (H1 e); [ Clear H1; Intros H1 | XAuto ]. XElim H1; XDEAuto 3. Qed. End pr3_gen_lift. Section pr3_gen_lref. (***************************************************) Hints Resolve getl_drop : ld. Lemma pr3_gen_lref: (c:?; x:?; n:?) (pr3 c (TLRef n) x) -> x = (TLRef n) \/ (EX d u v | (getl n c (CHead d (Bind Abbr) u)) & (pr3 d u v) & x = (lift (S n) (0) v) ). Proof. Intros; InsertEq H '(TLRef n); XElim H; Clear y x; Intros. (* case 1: pr3_refl *) XAuto. (* case 2: pr3_sing *) Subst; Pr2GenBase; Subst. (* case 2.1: pr2_free *) XAuto. (* case 2.2: pr2_delta *) Clear H1. LApply (pr3_gen_lift c x1 t3 (S n) (0)); [ Clear H0; Intros | XAuto ]. LApply (H x0); [ Clear H; Intros | XDEAuto 2 ]. XDecompose H; XDEAuto 3. Qed. End pr3_gen_lref. Section pr3_gen_bind. (***************************************************) Tactic Definition IH := ( Match Context With | [ H: (u,t:T) (THead (Bind Void) ?1 ?2) = (THead (Bind Void) u t) -> ? |- ? ] -> LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (u,t:T) (THead (Bind Abbr) ?1 ?2) = (THead (Bind Abbr) u t) -> ? |- ? ] -> LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (u,t:T) (THead (Flat Appl) ?1 ?2) = (THead (Flat Appl) u t) -> ? |- ? ] -> LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; XDecompose H; Subst ). Hints Resolve pr3_sing : ld. Lemma pr3_gen_void: (c:?; u1,t1,x:?) (pr3 c (THead (Bind Void) u1 t1) x) -> (EX u2 t2 | x = (THead (Bind Void) u2 t2) & (pr3 c u1 u2) & (b:?; u:?) (pr3 (CHead c (Bind b) u) t1 t2) ) \/ (pr3 (CHead c (Bind Void) u1) t1 (lift (1) (0) x)). Proof. Intros until 1; InsertEq H '(THead (Bind Void) u1 t1); UnIntro t1 H; UnIntro u1 H; XElim H; Intros. (* case 1 : pr3_refl *) Rewrite H; XDEAuto 3. (* case 2 : pr3_sing *) Rewrite H2 in H; Clear H2 t0; Pr2Gen. (* case 2.1 : short step: compatibility *) Rewrite H3 in H1; Clear H0 H3 t2. IH; Try Pr3Context; Try Rewrite H2; XDEAuto 5. (* case 2.2 : short step: zeta *) XDEAuto 5. Qed. Hints Resolve pr3_t : ld. Lemma pr3_gen_abbr: (c:?; u1,t1,x:?) (pr3 c (THead (Bind Abbr) u1 t1) x) -> (EX u2 t2 | x = (THead (Bind Abbr) u2 t2) & (pr3 c u1 u2) & (pr3 (CHead c (Bind Abbr) u1) t1 t2) ) \/ (pr3 (CHead c (Bind Abbr) u1) t1 (lift (1) (0) x)). Proof. Intros until 1; InsertEq H '(THead (Bind Abbr) u1 t1); UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; Rename x into u1; Rename x0 into t4. (* case 1: pr3_refl *) Rewrite H; XDEAuto 3. (* case 2: pr3_sing *) Rewrite H2 in H; Clear H2 t1; Pr2Gen. (* case 2.1: short step: compatibility *) Rewrite H3 in H1; Clear H0 H3 t2. IH; Repeat Pr3Context; Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); XDEAuto 3. (* case 2.2: short step: beta *) Rewrite H3 in H1; Clear H0 H3 t1. IH; Repeat Pr3Context; Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); XDEAuto 3. (* case 2.3: short step: delta *) Rewrite H3 in H1; Clear H0 H3 t2. IH; Repeat Pr3Context; Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); XDEAuto 7. (* case 2.4: short step: zeta *) XDEAuto 5. Qed. Lemma pr3_gen_appl: (c:?; u1,t1,x:?) (pr3 c (THead (Flat Appl) u1 t1) x) -> (OR (EX u2 t2 | x = (THead (Flat Appl) u2 t2) & (pr3 c u1 u2) & (pr3 c t1 t2) ) | (EX y1 z1 u2 t2 | (pr3 c (THead (Bind Abbr) u2 t2) x) & (pr3 c u1 u2) & (pr3 c t1 (THead (Bind Abst) y1 z1)) & (b:?; u:?) (pr3 (CHead c (Bind b) u) z1 t2) ) | (EX b y1 z1 z2 u2 y2 | ~b=Abst & (pr3 c t1 (THead (Bind b) y1 z1)) & (pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (1) (0) u2) z2)) x) & (pr3 c u1 u2) & (pr3 c y1 y2) & (pr3 (CHead c (Bind b) y2) z1 z2)) ). Proof. Intros; InsertEq H '(THead (Flat Appl) u1 t1). UnIntro t1 H; UnIntro u1 H. XElim H; Clear y x; Intros; Subst. Rename x into u0; Rename x0 into t0. (* case 1: pr3_refl *) XDEAuto 3. (* case 2: pr3_sing *) Pr2Gen; Subst. (* case 2.1: short step: compatibility *) Clear H0; IH. (* case 2.1.1: long step: compatibility *) Apply or3_intro0; EApply ex3_2_intro; XDEAuto 2. (* case 2.1.2: long step: beta *) Apply or3_intro1; EApply ex4_4_intro; XDEAuto 2. (* case 2.1.3: long step: upsilon *) Apply or3_intro2; EApply ex6_6_intro; XDEAuto 2. (* case 2.2: short step: beta *) Clear H1; Apply or3_intro1; EApply ex4_4_intro; XDEAuto 2. (* case 2.3: short step: upsilon *) Clear H1; Apply or3_intro2; EApply ex6_6_intro; XDEAuto 2. Qed. Tactic Definition XPr3Gen := ( Match Context With | [ H: (pr3 ?1 (THead (Bind Void) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (pr3 ?1 (THead (Bind Abbr) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H | [ |- ? ] -> Pr3GenBase ). Lemma pr3_gen_bind: (b:?) ~b=Abst -> (c:?; u1,t1,x:?) (pr3 c (THead (Bind b) u1 t1) x) -> (EX u2 t2 | x = (THead (Bind b) u2 t2) & (pr3 c u1 u2) & (pr3 (CHead c (Bind b) u1) t1 t2) ) \/ (pr3 (CHead c (Bind b) u1) t1 (lift (1) (0) x)). Proof. XElim b; Intros; Try EqFalse; XPr3Gen; XDEAuto 3. Qed. End pr3_gen_bind. Tactic Definition Pr3Gen := ( Match Context With | [ H: (pr3 ?1 (TLRef ?2) ?3) |- ? ] -> LApply (pr3_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (pr3 ?1 (THead (Bind Void) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (pr3 ?1 (THead (Bind Abbr) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (pr3 ?1 (THead (Flat Appl) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H0: (pr3 ?1 (lift ?2 ?3 ?4) ?5); H1: (drop ?2 ?3 ?1 ?6) |- ? ] -> LApply (pr3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ]; XDecompose H0 | [ H: (pr3 (CHead ?1 (Bind ?2) ?3) (lift (1) (0) ?4) ?5) |- ? ] -> LApply (pr3_gen_lift (CHead ?1 (Bind ?2) ?3) ?4 ?5 (1) (0)); [ Clear H; Intros H | XAuto ]; LApply (H ?1); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H0: ~?0=Abst; H1: (pr3 ? (THead (Bind ?0) ? ?) ?) |- ? ] -> XDecomPoseClear H1 '(pr3_gen_bind ? H0 ? ? ? ? H1) | [ H0: ~?0=Abst; H1: (pr2 ?1 (THead (Bind ?0) ?2 ?3) ?4) |- ? ] -> XPose H_x '(pr3_gen_bind ? H0 ?1 ?2 ?3 ?4); LApply H_x; [ Clear H1 H_x; Intros H1; XDecompose H1 | XAuto ] | [ |- ? ] -> Pr3GenBase ).