(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require getl_props. Require subst1_gen. Require subst1_subst1. Require subst1_confluence. Require csubst1_defs. Require pr0_gen. Require pr0_subst1. Require pr2_defs. Require pr2_gen. Require pr2_subst1. Section pr2_gen_context. (************************************************) Hints Resolve le_S_n sym_not_equal lt_neq subst1_trans : ld. Lemma pr2_gen_cabbr: (c:?; t1,t2:?) (pr2 c t1 t2) -> (e:?; u:?; d:?) (getl d c (CHead e (Bind Abbr) u)) -> (a0:?) (csubst1 d u c a0) -> (a:?) (drop (1) d a0 a) -> (x1:?) (subst1 d u t1 (lift (1) d x1)) -> (EX x2 | (subst1 d u t2 (lift (1) d x2)) & (pr2 a x1 x2) ). Proof. Intros until 1; XElim H; Clear c t1 t2; Intros; Pr0Subst1; Pr0Gen; Subst. (* case 1: pr2_free *) XDEAuto 3. (* case 2: pr2_delta *) Apply (lt_eq_gt_e i d0); Intros; Subst. (* case 2.1: i < d0 *) Subst1Confluence; CSubst1GetL. Rewrite minus_x_Sy in H; [ Idtac | XAuto ]. CSubst1GenBase; Subst. Rewrite (lt_plus_minus i d0) in H4; [ Idtac | XAuto ]. GetLDis; Subst. Subst1Subst1; Pattern 2 d0 in H; Rewrite (lt_plus_minus i d0) in H; [ Idtac | XAuto ]. Subst1Gen; Subst. Rewrite <- lt_plus_minus in H8; [ Idtac | XAuto ]. Rewrite <- lt_plus_minus_r in H8; XDEAuto 4. (* case 2.2: i = d0 *) GetLDis; XInv; Subst. Subst1Confluence; Subst1Gen; Subst; XDEAuto 3. (* case 2.3: i > d0 *) Subst1Confluence; Subst1Gen; Subst; Clear H2. CSubst1GetL; GetLDis; XDEAuto 3. Qed. End pr2_gen_context. Tactic Definition Pr2GenContext := ( Match Context With | [ H0: (pr2 ?1 ?2 ?3); H1: (getl ?4 ?1 (CHead ?5 (Bind Abbr) ?6)); H2: (csubst1 ?4 ?6 ?1 ?7); H3: (drop (1) ?4 ?7 ?8); H4: (subst1 ?4 ?6 ?2 (lift (1) ?4 ?9)) |- ? ] -> LApply (pr2_gen_cabbr ?1 ?2 ?3); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?5 ?6 ?4); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?8); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?9); [ Clear H0 H4; Intros H0 | XAuto ]; XElim H0; Intros ).