(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require pr3_gen. Require nf2_defs. Require nf2_gen. Require pc3_props. Require pc3_gen. Require ty3_defs. Require ty3_gen. Require ty3_props. Require ty3_arity_props. Require ty3_gen_nf2. Definition ty3_nf2_inv_abst_premise := [c,w,u:?] (d:C; wi:T; i:nat) (getl i c (CHead d (Bind Abst) wi)) -> (vs:TList) (pc3 c (THeads (Flat Appl) vs (lift (S i) O wi)) (THead (Bind Abst) w u) ) -> False. Section ty3_nf2_inv_abst_premise_props. (*********************************) Lemma ty3_nf2_inv_abst_premise_csort: (w,u:?; m:?) (ty3_nf2_inv_abst_premise (CSort m) w u). Proof. Unfold ty3_nf2_inv_abst_premise; Intros; GetLGenBase. Qed. End ty3_nf2_inv_abst_premise_props. Hints Resolve ty3_nf2_inv_abst_premise_csort : ld. Section ty3_nf2_gen. (****************************************************) Hints Resolve arity_nf2_inv_all : ld. Lemma ty3_nf2_inv_all: (g:?; c:?; t:?; u:?) (ty3 g c t u) -> (nf2 c t) -> (OR (EX w u | t = (THead (Bind Abst) w u) & (nf2 c w) & (nf2 (CHead c (Bind Abst) w) u) ) | (EX n | t = (TSort n)) | (EX ws i | t = (THeads (Flat Appl) ws (TLRef i)) & (nfs2 c ws) & (nf2 c (TLRef i)) )). Proof. Intros; XDecomPose '(ty3_arity ? ? ? ? H); Clear H H2; XDEAuto 2. Qed. Lemma ty3_nf2_inv_sort: (g:?; c:?; t:?; m:?) (ty3 g c t (TSort m)) -> (nf2 c t) -> (or (EX n | t = (TSort n) & m = (next g n)) (EX ws i | t = (THeads (Flat Appl) ws (TLRef i)) & (nfs2 c ws) & (nf2 c (TLRef i)) )). Proof. Intros; XDecomPose '(ty3_nf2_inv_all ? ? ? ? H H0); Clear H0; Subst. (* case 1: Abst *) Clear H3 H4; Ty3GenBase; Clear H0 H1 H2; Pc3Gen. (* case 2: Sort *) Ty3GenBase; Pc3Gen; Subst; XDEAuto 3. (* case 3: Appls *) XDEAuto 3. Qed. Hints Resolve pc3_t : ld. Remark ty3_nf2_inv_abst_aux: (c:?; w1,u1:?) (ty3_nf2_inv_abst_premise c w1 u1) -> (t,w2,u2:?) (pc3 c (THead (Flat Appl) t (THead (Bind Abst) w2 u2)) (THead (Bind Abst) w1 u1)) -> (ty3_nf2_inv_abst_premise c w2 u2). Proof. Unfold ty3_nf2_inv_abst_premise; Intros. EApply H with vs:=(TCons t vs); Simpl; XDEAuto 3. Qed. Hints Resolve ty3_conv : ld. Lemma ty3_nf2_inv_abst: (g:?; c:?; t,w,u:?) (ty3 g c t (THead (Bind Abst) w u)) -> (nf2 c t) -> (nf2 c w) -> (ty3_nf2_inv_abst_premise c w u) -> (EX v w0 | t = (THead (Bind Abst) w v) & (ty3 g c w w0) & (ty3 g (CHead c (Bind Abst) w) v u) & (nf2 (CHead c (Bind Abst) w) v) ). Proof. Intros; XDecomPoseClear H0 '(ty3_nf2_inv_all ? ? ? ? H H0); Subst. (* case 1: Abst *) Ty3Correct; Repeat Ty3GenBase; Pc3Gen; Clear H0 H2 H7 x x5. XPoseClear H '(pc3_nf2 ? ? ? H H5 H1); Clear H5 H1; Subst. XDEAuto 3. (* case 2: Sort *) Clear H1; Ty3GenBase; Pc3Gen. (* case 3: Appls *) Clear H1 H5; Impl H H2; ImplLast; UnIntro H6 u; UnIntro H6 w. XElim x0; Simpl; Intros. (* case 3.1: TNil *) Ty3GenBase; [ NF2GenBase | XDecomPose '(H0 ? ? ? H1 TNil H) ]. (* case 3.2: TCons *) Clear H6; Ty3GenBase; Clear H3. XPoseClear H1 '(ty3_nf2_inv_abst_aux ? ? ? H1 ? ? ? H0); Clear H0. XDecomPoseClear H '(H ? ? H2 H1); Clear H1 H2 H3 H4 H5. NewInduction t0; Simpl in H0; XInv. Qed. Lemma ty3_inv_lref_nf2_pc3: (g:?; c:?; u1:?; i:?) (ty3 g c (TLRef i) u1) -> (nf2 c (TLRef i)) -> (u2:?) (nf2 c u2) -> (pc3 c u1 u2) -> (EX u | u2 = (lift (S i) (0) u)). Proof. Intros until 1; InsertEq H '(TLRef i); XElim H; Clear c y u1; Intros; Subst; XInv; Subst. (* case 1: ty3_conv *) Clear H H0 H1 g t. XPoseClear H2 '(H2 (refl_equal ? ?) H5 ? H6); Clear H5 H6. LApply H2; [ Clear H2 H3 H7 c t1 t2; Intros H2 | XDEAuto 2 ]. XAuto. (* case 2: ty3_abbr *) NF2GenBase. (* case 3: ty3_abst *) Clear H0 H1 H3 g t; GetLDrop; Clear H. XPoseClear H4 '(pc3_nf2_unfold ? ? ? H5 H4); Clear H5. Pr3Gen; Subst; XDEAuto 2. Qed. Hints Resolve ty3_inv_lref_nf2_pc3 : ld. Lemma ty3_inv_lref_nf2: (g:?; c:?; u:?; i:?) (ty3 g c (TLRef i) u) -> (nf2 c (TLRef i)) -> (nf2 c u) -> (EX u0 | u = (lift (S i) (0) u0)). Proof. Intros; XDEAuto 2. Qed. Lemma ty3_inv_appls_lref_nf2: (g:?; c:?; vs:?; u1:?; i:?) (ty3 g c (THeads (Flat Appl) vs (TLRef i)) u1) -> (nf2 c (TLRef i)) -> (nf2 c u1) -> (EX u | (nf2 c (lift (S i) (0) u)) & (pc3 c (THeads (Flat Appl) vs (lift (S i) (0) u)) u1) ). Proof. XElim vs; Simpl; Intros. (* case 1: TNil *) XDecomPose '(ty3_inv_lref_nf2 ? ? ? ? H H0 H1); Clear H H0; Subst. XDEAuto 2. (* case 2: TCons *) Ty3GenNF2. XPoseClear H '(H ? ? H4 H1); Clear H4 H1. LApply H; [ Clear H; Intros H; Clear H0 H7 | XAuto ]. XDecompose H; XDEAuto 4. Qed. Lemma ty3_inv_lref_lref_nf2: (g:?; c:?; i,j:?) (ty3 g c (TLRef i) (TLRef j)) -> (nf2 c (TLRef i)) -> (nf2 c (TLRef j)) -> (lt i j). Proof. Intros. XDecomPose '(ty3_inv_lref_nf2 ? ? ? ? H H0 H1); Clear H H0 H1 g c. LiftGenBase; [ LeLtGen | XAuto ]. Qed. End ty3_nf2_gen. Tactic Definition Ty3NF2Gen := ( Match Context With | [ H0: (ty3 ? ?1 ?2 (TSort ?)); H1: (nf2 ?1 ?2) |- ? ] -> XDecomPose '(ty3_nf2_inv_sort ? ? ? ? H0 H1); Subst; Clear H0 H1 | [ H0: (ty3 ? ?0 ?1 (THead (Bind Abst) ?2 ?3)); H1: (nf2 ?0 ?1) |- ? ] -> XPoseClear H0 '(ty3_nf2_inv_abst ? ? ? ? ? H0 H1); Clear H1 | [ H0: (ty3 ? ?1 ?2 ?); H1: (nf2 ?1 ?2) |- ? ] -> XDecomPose '(ty3_nf2_inv_all ? ? ? ? H0 H1); Subst; Clear H1 ).