From: Ferruccio Guidi Date: Sun, 15 Jun 2014 14:19:10 +0000 (+0000) Subject: - we introduce stratified term equivalence to remove the parameter g from cpx X-Git-Tag: make_still_working~901 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d669f492522b055f76c627eb89da97d0be05c2a;p=helm.git - we introduce stratified term equivalence to remove the parameter g from cpx - unused files removed from etc - minor updates --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma index b11b709a9..c3e0444d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma @@ -138,7 +138,7 @@ lemma cpds_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. #h #g #G #L1 #T1 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 -elim (lstas_cpr_lpr … g … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12 +elim (lstas_cpr_lpr … Hl1 … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12 lapply (da_cpr_lpr … Hl1 … HT12 … HL12) // -T1 lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_conj.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_conj.etc deleted file mode 100644 index 6ffdb54db..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_conj.etc +++ /dev/null @@ -1,88 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) -(* -include "basic_2/reduction/lpr_ldrop.ma". - -include "basic_2/unfold/fsups.ma". -include "basic_2/reducibility/lpr_ldrop.ma". - -lamma pippo: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀V1,i. ⇧[i, 1] V1 ≡ T1 → T2 = #i → ⊥. -#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 -[ #I #L1 #V #W1 #j #H1 #H2 - elim (lift_inv_lref2 … H1) -H1 * #H1 #H3 - - HVT2 : () - HV2 : (K2⊢V➡V2) - - -thaorem cpr_trans_lpr: ∀L1,T1,T. L1 ⊢ T1 ➡ T → ∀L2. L1 ⊢ ➡ L2 → - ∀T2. L2 ⊢ T ➡ T2 → - (⦃L2, T2⦄ ⊃* ⦃L1, T1⦄ → ⊥) ∨ T1 = T. -#L1 #T1 @(fsupp_wf_ind … L1 T1) -L1 -T1 #n #IH #L1 * [|*] -[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct -IH - elim (cpr_inv_atom1 … H1) -H1 - [ #H destruct - elim (cpr_inv_atom1 … HT2) -HT2 - [ #H destruct // - | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct // - ] - | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 - elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 - elim (lpr_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) -V0 #HLK2 - elim (cpr_inv_lift1 … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT #V2 #HVT2 #HV2 - @or_introl #H - - - - - - - elim (lift_inv_lref2 … HVT2) -HVT2 * #H #_ - [ elim (lt_zero_false … H) - | >commutative_plus in H; >plus_plus_comm_23 #H - elim (le_plus_xySz_x_false … H) - ] - ] -| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 - elim (cpr_inv_bind1 … H1) -H1 * - [ #V #T #HV1 #HT1 #H destruct - elim (cpr_inv_bind1 … H2) -H2 * - [ #V2 #T2 #HV2 #HT2 #H destruct - elim (IH … HV1 … HV2) // #HV12 destruct - [ @or_introl #H destruct /2 width=1/ - | elim (IH … HT1 … HT2) // /2 width=1/ -L1 -L2 #HT12 destruct - @or_introl #H destruct /2 width=1/ - ] - | #T2 #HT2 #HXT2 #H1 #H2 destruct - elim (IH … HT1 … HT2) // /2 width=1/ -L1 -L2 #HT12 destruct - | elim (term_eq_dec V1 V) #HV1 destruct - - ] - | #Y1 #HTY1 #HXY1 #H11 #H12 destruct - elim (lift_total (+ⓓV1.T1) 0 1) #Y2 #HXY2 - lapply (cpr_lift … H2 (L2.ⓓV1) … HXY1 … HXY2) /2 width=1/ -X1 /4 width=5/ - ] -| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 - elim (cpr_inv_flat1 … H1) -H1 * - [ #V #T #HV1 #HT1 #H destruct - elim (cpr_inv_flat1 … H2) -H2 * - [ #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ - | #HX2 #H destruct /3 width=5/ - ] - | #HX1 #H destruct /3 width=5/ -] -qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/etc/cpr_conj.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/etc/cpr_conj.etc new file mode 100644 index 000000000..6ffdb54db --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/etc/cpr_conj.etc @@ -0,0 +1,88 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) +(* +include "basic_2/reduction/lpr_ldrop.ma". + +include "basic_2/unfold/fsups.ma". +include "basic_2/reducibility/lpr_ldrop.ma". + +lamma pippo: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀V1,i. ⇧[i, 1] V1 ≡ T1 → T2 = #i → ⊥. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 +[ #I #L1 #V #W1 #j #H1 #H2 + elim (lift_inv_lref2 … H1) -H1 * #H1 #H3 + + HVT2 : () + HV2 : (K2⊢V➡V2) + + +thaorem cpr_trans_lpr: ∀L1,T1,T. L1 ⊢ T1 ➡ T → ∀L2. L1 ⊢ ➡ L2 → + ∀T2. L2 ⊢ T ➡ T2 → + (⦃L2, T2⦄ ⊃* ⦃L1, T1⦄ → ⊥) ∨ T1 = T. +#L1 #T1 @(fsupp_wf_ind … L1 T1) -L1 -T1 #n #IH #L1 * [|*] +[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct -IH + elim (cpr_inv_atom1 … H1) -H1 + [ #H destruct + elim (cpr_inv_atom1 … HT2) -HT2 + [ #H destruct // + | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct // + ] + | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -V0 #HLK2 + elim (cpr_inv_lift1 … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT #V2 #HVT2 #HV2 + @or_introl #H + + + + + + + elim (lift_inv_lref2 … HVT2) -HVT2 * #H #_ + [ elim (lt_zero_false … H) + | >commutative_plus in H; >plus_plus_comm_23 #H + elim (le_plus_xySz_x_false … H) + ] + ] +| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 + elim (cpr_inv_bind1 … H1) -H1 * + [ #V #T #HV1 #HT1 #H destruct + elim (cpr_inv_bind1 … H2) -H2 * + [ #V2 #T2 #HV2 #HT2 #H destruct + elim (IH … HV1 … HV2) // #HV12 destruct + [ @or_introl #H destruct /2 width=1/ + | elim (IH … HT1 … HT2) // /2 width=1/ -L1 -L2 #HT12 destruct + @or_introl #H destruct /2 width=1/ + ] + | #T2 #HT2 #HXT2 #H1 #H2 destruct + elim (IH … HT1 … HT2) // /2 width=1/ -L1 -L2 #HT12 destruct + | elim (term_eq_dec V1 V) #HV1 destruct + + ] + | #Y1 #HTY1 #HXY1 #H11 #H12 destruct + elim (lift_total (+ⓓV1.T1) 0 1) #Y2 #HXY2 + lapply (cpr_lift … H2 (L2.ⓓV1) … HXY1 … HXY2) /2 width=1/ -X1 /4 width=5/ + ] +| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 + elim (cpr_inv_flat1 … H1) -H1 * + [ #V #T #HV1 #HT1 #H destruct + elim (cpr_inv_flat1 … H2) -H2 * + [ #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ + | #HX2 #H destruct /3 width=5/ + ] + | #HX1 #H destruct /3 width=5/ +] +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/etc/ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/etc/ldrop.etc new file mode 100644 index 000000000..e4caef0c8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/etc/ldrop.etc @@ -0,0 +1,11 @@ +lemma ldrop_bor1: ∀L1,L2,s1,s2,d,e. ⇩[s1, d, e] L1 ≡ L2 → ⇩[s1 ∨ s2, d, e] L1 ≡ L2. +#L1 #L2 * /2 width=1 by ldrop_gen/ +qed. + +lemma ldrop_bor2: ∀L1,L2,s1,s2,d,e. ⇩[s2, d, e] L1 ≡ L2 → ⇩[s1 ∨ s2, d, e] L1 ≡ L2. +#L1 #L2 #s1 #s2 >commutative_orb /2 width=1 by ldrop_bor1/ +qed. + +(* Basic_1: was: drop_conf_rev *) +axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L → + ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss.etc deleted file mode 100644 index 8ca46b68a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss.etc +++ /dev/null @@ -1,115 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -notation "hvbox( h ⊢ break term 46 L1 • ⊑ break [ term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'CrSubEqS $h $g $L1 $L2 }. - -include "basic_2/static/ssta.ma". -include "basic_2/computation/cprs.ma". -include "basic_2/equivalence/cpcs.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) - -(* Note: this is not transitive *) -inductive lsubss (h:sh) (g:sd h): relation lenv ≝ -| lsubss_atom: lsubss h g (⋆) (⋆) -| lsubss_pair: ∀I,L1,L2,V. lsubss h g L1 L2 → - lsubss h g (L1. ⓑ{I} V) (L2. ⓑ{I} V) -| lsubss_abbr: ∀L1,L2,V1,V2,W1,W2,l. L1 ⊢ W1 ⬌* W2 → - ⦃h, L1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ → ⦃h, L2⦄ ⊢ W2 •[g] ⦃l, V2⦄ → - lsubss h g L1 L2 → lsubss h g (L1. ⓓV1) (L2. ⓛW2) -. - -interpretation - "local environment refinement (stratified static type assigment)" - 'CrSubEqS h g L1 L2 = (lsubss h g L1 L2). - -(* Basic inversion lemmas ***************************************************) - -fact lsubss_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 = ⋆ → L2 = ⋆. -#h #g #L1 #L2 * -L1 -L2 -[ // -| #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #H destruct -] -qed-. - -lemma lsubss_inv_atom1: ∀h,g,L2. h ⊢ ⋆ •⊑[g] L2 → L2 = ⋆. -/2 width=5 by lsubss_inv_atom1_aux/ qed-. - -fact lsubss_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ - ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & - K1 ⊢ W1 ⬌* W2 & h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. -#h #g #L1 #L2 * -L1 -L2 -[ #J #K1 #U1 #H destruct -| #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/ -| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=10/ -] -qed-. - -lemma lsubss_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 •⊑[g] L2 → - (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ - ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & - K1 ⊢ W1 ⬌* W2 & h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. -/2 width=3 by lsubss_inv_pair1_aux/ qed-. - -fact lsubss_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L2 = ⋆ → L1 = ⋆. -#h #g #L1 #L2 * -L1 -L2 -[ // -| #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #H destruct -] -qed-. - -lemma lsubss_inv_atom2: ∀h,g,L1. h ⊢ L1 •⊑[g] ⋆ → L1 = ⋆. -/2 width=5 by lsubss_inv_atom2_aux/ qed-. - -fact lsubss_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀I,K2,W2. L2 = K2. ⓑ{I} W2 → - (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ - ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & - K1 ⊢ W1 ⬌* W2 & h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. -#h #g #L1 #L2 * -L1 -L2 -[ #J #K2 #U2 #H destruct -| #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/ -| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=10/ -] -qed-. - -lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 •⊑[g] K2. ⓑ{I} W2 → - (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ - ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & - K1 ⊢ W1 ⬌* W2 & h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. -/2 width=3 by lsubss_inv_pair2_aux/ qed-. - -(* Basic_forward lemmas *****************************************************) - -axiom lsubss_fwd_lsubx: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⓝ⊑ L2. -(* -#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ -qed-. -*) -(* Basic properties *********************************************************) - -lemma lsubss_refl: ∀h,g,L. h ⊢ L •⊑[g] L. -#h #g #L elim L -L // /2 width=1/ -qed. - -lemma lsubss_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -/3 width=5 by lsubss_fwd_lsubx, lsubx_cprs_trans/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_cpcs.etc deleted file mode 100644 index 797a1b272..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_cpcs.etc +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/lsubss.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) - -(* Properties on context-sensitive parallel equivalence for terms ***********) - -lemma lsubss_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2. -/3 width=5 by lsubss_fwd_lsubx, lsubx_cpcs_trans/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_etc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_etc.etc deleted file mode 100644 index a30f3558c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_etc.etc +++ /dev/null @@ -1,3 +0,0 @@ -lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → h ⊢ L1 •⊑[g] L2. -#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_ldrop.etc deleted file mode 100644 index 8876f8593..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_ldrop.etc +++ /dev/null @@ -1,65 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/equivalence/lsubss.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) - -(* Properties concerning basic local environment slicing ********************) - -(* Note: the constant 0 cannot be generalized *) -lemma lsubss_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀K1,e. ⇩[0, e] L1 ≡ K1 → - ∃∃K2. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L2 ≡ K2. -#h #g #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3/ -| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H - elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 - [ destruct - elim (IHL12 L1 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=3/ - | elim (IHL12 … HLK1) -L1 /3 width=3/ - ] -| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #_ #IHL12 #K1 #e #H - elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 - [ destruct - elim (IHL12 L1 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=6/ - | elim (IHL12 … HLK1) -L1 /3 width=3/ - ] -] -qed-. - -(* Note: the constant 0 cannot be generalized *) -lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L1 ≡ K1. -#h #g #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3/ -| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H - elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 - [ destruct - elim (IHL12 L2 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=3/ - | elim (IHL12 … HLK2) -L2 /3 width=3/ - ] -| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #_ #IHL12 #K2 #e #H - elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 - [ destruct - elim (IHL12 L2 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=6/ - | elim (IHL12 … HLK2) -L2 /3 width=3/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_ssta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_ssta.etc deleted file mode 100644 index 0fe035dbb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss2/lsubss_ssta.etc +++ /dev/null @@ -1,54 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/ssta_ssta.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/lsubss_ldrop.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) - -(* Properties on stratified native type assignment **************************) - -lemma lsubss_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ → - ∀L1. h ⊢ L1 •⊑[g] L2 → - ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2. -#h #g #L2 #T #U #l #H elim H -L2 -T -U -l -[ /3 width=3/ -| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12 - elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ] - [ #HK12 #H destruct - elim (IHVW2 … HK12) -K2 #T2 #HVT2 #HTW2 - lapply (ldrop_fwd_ldrop2 … HLK1) #H - elim (lift_total T2 0 (i+1)) /3 width=11/ - | #W1 #V1 #W2 #l0 #_ #_ #_ #_ #_ #H destruct - ] -| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12 - elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ] - [ #HK12 #H destruct - elim (IHWV2 … HK12) -K2 /3 width=6/ - | #W1 #V1 #T2 #l0 #HVW1 #HWT2 #HW12 #_ #H #_ destruct - elim (ssta_mono … HWV2 … HWT2) -HWV2 -HWT2 #H1 #H2 destruct - lapply (ldrop_fwd_ldrop2 … HLK1) #H - elim (lift_total W1 0 (i+1)) /3 width=11/ - ] -| #a #I #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 - elim (IHTU2 (L1.ⓑ{I}V2) …) [2: /2 width=1/ ] -L2 /3 width=3/ -| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 - elim (IHTU2 … HL12) -L2 /3 width=5/ -| #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 - elim (IHTU2 … HL12) -L2 /3 width=3/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/aaa_ssta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/aaa_ssta.etc deleted file mode 100644 index 5cccd8fe1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/aaa_ssta.etc +++ /dev/null @@ -1,47 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/ssta.ma". -include "basic_2/static/aaa_lift.ma". -include "basic_2/static/aaa_da.ma". - -(* ATONIC ARITY ASSIGNMENT FOR TERMS ****************************************) - -(* Properties on stratified static type assignment for terms ****************) - -lemma aaa_ssta_conf: ∀h,g,G,L. Conf3 … (aaa G L) (ssta h g G L). -#h #g #G #L #T #A #H elim H -G -L -T -A -[ #G #L #k #U #H - lapply (ssta_inv_sort1 … H) -H #H destruct // -| #I #G #L #K #V #B #i #HLK #HV #IHV #U #H - elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HU - lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H0 destruct - lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK - @(aaa_lift … HLK … HU) -HU -L // -HV /2 width=2/ -| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #H - elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/ -| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #H - elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/ -| #G #L #V #T #B #A #HV #_ #_ #IHT #X #H - elim (ssta_inv_appl1 … H) -H #U #HTU #H destruct /3 width=3/ -| #G #L #V #T #A #_ #_ #IHV #IHT #X #H - lapply (ssta_inv_cast1 … H) -H /2 width=2/ -] -qed-. - -(* Forward lemmas on stratified static type assignment for terms ************) - -lemma aaa_fwd_ssta: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∃U. ⦃G, L⦄ ⊢ T •[h, g] U. -#h #g #G #L #T #A #H elim (aaa_fwd_da … H) -H /2 width=3 by da_ssta/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds.etc deleted file mode 100644 index 692f1fb0a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds.etc +++ /dev/null @@ -1,46 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/dpredstar_6.ma". -include "basic_2/unfold/lsstas.ma". -include "basic_2/computation/cprs.ma". - -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) - -definition cpds: ∀h. sd h → relation4 genv lenv term term ≝ - λh,g,G,L,T1,T2. - ∃∃T,l1,l2. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T & ⦃G, L⦄ ⊢ T ➡* T2. - -interpretation "decomposed extended parallel computation (term)" - 'DPRedStar h g G L T1 T2 = (cpds h g G L T1 T2). - -(* Basic properties *********************************************************) - -lemma ssta_cprs_cpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h, g] T → - ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/3 width=7/ qed. - -lemma lsstas_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/2 width=7/ qed. - -lemma cprs_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/2 width=7/ qed. - -lemma cpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g] T. -/2 width=2/ qed. - -lemma cpds_strap1: ∀h,g,G,L,T1,T,T2. - ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -#h #g #G #L #T1 #T #T2 * /3 width=9/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_aaa.etc deleted file mode 100644 index 1eba7e837..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_aaa.etc +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/unfold/lsstas_aaa.ma". -include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/cpds.ma". - -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) - -(* Properties on atomic arity assignment for terms **************************) - -lemma cpds_aaa_conf: ∀h,g,G,L. Conf3 … (aaa G L) (cpds h g G L). -#h #g #G #L #A #T #HT #U * /3 width=6 by lsstas_aaa_conf, cprs_aaa_conf/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_cpds.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_cpds.etc deleted file mode 100644 index ef1e56d90..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_cpds.etc +++ /dev/null @@ -1,75 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/unfold/lsstas_lsstas.ma". -include "basic_2/computation/lprs_cprs.ma". -include "basic_2/computation/cpxs_cpxs.ma". -include "basic_2/computation/cpds.ma". - -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) - -(* Advanced properties ******************************************************) - -lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •[h, g] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -#h #g #G #L #T1 #T #T2 #l #Hl #HT1 * -#T0 #l0 #l1 #Hl10 #HT #HT0 #HT02 -lapply (ssta_da_conf … HT1 … Hl) (lift_mono … H1 … H2) -H1 -H2 // -| #G #K #k #l #Hkl #L #s #d #e #_ #U1 #H1 #U2 #H2 - >(lift_inv_sort1 … H1) -U1 - >(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_st/ -| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #d #e #HLK #U1 #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 - lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta, ldrop_inv_gen/ - ] -| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2 - elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct - elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpx_bind, ldrop_skip/ -| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2 - elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct - elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpx_flat/ -| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #H #U2 #HTU2 - elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct - elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpx_zeta, ldrop_skip/ -| #G #K #V #T1 #T2 #_ #IHT12 #L #s #d #e #HLK #U1 #H #U2 #HTU2 - elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_eps/ -| #G #K #V1 #V2 #T #_ #IHV12 #L #s #d #e #HLK #U1 #H #U2 #HVU2 - elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_ct/ -| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct - elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct - elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpx_beta, ldrop_skip/ -| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct - elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct - elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct - elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpx_theta, ldrop_skip/ -] -qed. - -lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G). -#h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2 -[ * #i #G #L #K #s #d #e #_ #T1 #H - [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_sort, ex2_intro/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ - | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_gref, ex2_intro/ - ] -| #G #L #k #l #Hkl #K #s #d #e #_ #T1 #H - lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by cpx_st, lift_sort, ex2_intro/ -| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #d #e #HLK #T1 #H - elim (lift_inv_lref2 … H) -H * #Hid #H destruct - [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV - elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 - elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus plus_minus // (plus_minus_m_m (l2-l1) 1 ?) -[ /4 width=5 by cpxs_strap1, ssta_cpx, lt_to_le/ -| /2 width=1 by monotonic_le_minus_r/ -] -qed. - -lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i. - ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 → - ∀W2. ⇧[0, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2. -#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2 -[ /3 width=9 by cpx_cpxs, cpx_delta/ -| #V1 lapply (ldrop_fwd_drop2 … HLK) -HLK - elim (lift_total V1 0 (i+1)) /4 width=12 by cpx_lift, cpxs_strap1/ -] -qed. - -(* Advanced inversion lemmas ************************************************) - -lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 → - T2 = #i ∨ - ∃∃I,K,V1,T1. ⇩[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 & - ⇧[0, i+1] T1 ≡ T2. -#h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ -#T #T2 #_ #HT2 * -[ #H destruct - elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ - * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ -| * #I #K #V1 #T1 #HLK #HVT1 #HT1 - lapply (ldrop_fwd_drop2 … HLK) #H0LK - elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T - /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ -] -qed-. - -(* Relocation properties ****************************************************) - -lemma cpxs_lift: ∀h,g,G. l_liftable (cpxs h g G). -/3 width=10 by cpx_lift, cpxs_strap1, l_liftable_LTC/ qed. - -lemma cpxs_inv_lift1: ∀h,g,G. l_deliftable_sn (cpxs h g G). -/3 width=6 by l_deliftable_sn_LTC, cpx_inv_lift1/ -qed-. - -(* Properties on supclosure *************************************************) - -lemma fqu_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ -#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqu_cpx_trans … HT1 … HT2) -T -#T #HT1 #HT2 elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ -qed-. - -lemma fquq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_cpxs_trans … HTU2 … HT12) /3 width=3 by fqu_fquq, ex2_intro/ -| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma fquq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → - ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -/3 width=5 by fquq_cpxs_trans, lsstas_cpxs/ qed-. - -lemma fqup_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ -#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqup_cpx_trans … HT1 … HT2) -T -#U1 #HTU1 #H2 elim (IHTU2 … H2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ -qed-. - -lemma fqus_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fqus_inv_gen … H) -H -[ #HT12 elim (fqup_cpxs_trans … HTU2 … HT12) /3 width=3 by fqup_fqus, ex2_intro/ -| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma fqus_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → - ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -/3 width=7 by fqus_cpxs_trans, lsstas_cpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpb_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpb_lift.etc deleted file mode 100644 index 8011dd753..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpb_lift.etc +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reduction/cpx_lift.ma". -include "basic_2/reduction/fpb.ma". - -(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) - -(* Advanced properties ******************************************************) - -lemma ssta_fpb: ∀h,g,G,L,T1,T2,l. - ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h, g] T2 → - ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄. -/3 width=5 by fpb_cpx, ssta_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbg_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbg_lift.etc deleted file mode 100644 index c67134ee3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbg_lift.etc +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/fpbu_lift.ma". -include "basic_2/computation/fpbg.ma". - -(* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************) - -(* Advanced properties ******************************************************) - -lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. -/5 width=5 by fpbc_fpbg, fpbu_fpbc, lsstas_fpbu/ qed. - -lemma ssta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. -/4 width=2 by fpbc_fpbg, fpbu_fpbc, ssta_fpbu/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbs_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbs_lift.etc deleted file mode 100644 index ab8f6608d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbs_lift.etc +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reduction/fpb_lift.ma". -include "basic_2/computation/cpxs_lift.ma". -include "basic_2/computation/fpbs.ma". - -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) - -(* Advanced properties ******************************************************) - -lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. -/3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed. - -lemma ssta_fpbs: ∀h,g,G,L,T,U,l. - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → - ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. -/4 width=2 by fpb_fpbs, ssta_fpb/ qed. - -(* Note: this is used in the closure proof *) -lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. - ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → - ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. -/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, ssta_cpx, fpb_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbu_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbu_lift.etc deleted file mode 100644 index d7b48650e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbu_lift.etc +++ /dev/null @@ -1,32 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/ssta_ssta.ma". -include "basic_2/computation/cpxs_lift.ma". -include "basic_2/computation/fpbu.ma". - -(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) - -(* Advanced properties ******************************************************) - -lemma lsstas_fpbu: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -/4 width=5 by fpbu_cpxs, lsstas_cpxs/ qed. - -lemma ssta_fpbu: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) -/3 width=5 by ssta_lsstas, lsstas_fpbu/ #H destruct -elim (ssta_inv_refl_pos … HT1 … HT12) -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas.etc deleted file mode 100644 index efad65abc..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas.etc +++ /dev/null @@ -1,133 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/statictypestar_7.ma". -include "basic_2/static/ssta.ma". - -(* NAT-ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *****************) - -definition lsstas: ∀h. sd h → genv → lenv → nat → relation term ≝ - λh,g,G,L. lstar … (ssta h g G L). - -interpretation "nat-iterated stratified static type assignment (term)" - 'StaticTypeStar h g G L l T U = (lsstas h g G L l T U). - -(* Basic eliminators ********************************************************) - -lemma lsstas_ind_sn: ∀h,g,G,L,U2. ∀R:relation2 nat term. - R 0 U2 → ( - ∀l,T,U1. ⦃G, L⦄ ⊢ T •[h, g] U1 → ⦃G, L⦄ ⊢ U1 •* [h, g, l] U2 → - R l U1 → R (l+1) T - ) → - ∀l,T. ⦃G, L⦄ ⊢ T •*[h, g, l] U2 → R l T. -/3 width=5 by lstar_ind_l/ qed-. - -lemma lsstas_ind_dx: ∀h,g,G,L,T. ∀R:relation2 nat term. - R 0 T → ( - ∀l,U1,U2. ⦃G, L⦄ ⊢ T •* [h, g, l] U1 → ⦃G, L⦄ ⊢ U1 •[h, g] U2 → - R l U1 → R (l+1) U2 - ) → - ∀l,U. ⦃G, L⦄ ⊢ T •*[h, g, l] U → R l U. -/3 width=5 by lstar_ind_r/ qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma lsstas_inv_O: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g, 0] U → T = U. -/2 width=4 by lstar_inv_O/ qed-. - -lemma lsstas_inv_SO: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g, 1] U → ⦃G, L⦄ ⊢ T •[h, g] U. -/2 width=1 by lstar_inv_step/ qed-. - -lemma lsstas_inv_step_sn: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, g, l+1] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 •[h, g] T & ⦃G, L⦄ ⊢ T •*[h, g, l] T2. -/2 width=3 by lstar_inv_S/ qed-. - -lemma lsstas_inv_step_dx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, g, l+1] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 •*[h, g, l] T & ⦃G, L⦄ ⊢ T •[h, g] T2. -/2 width=3 by lstar_inv_S_dx/ qed-. - -lemma lsstas_inv_sort1: ∀h,g,G,L,X,k,l. ⦃G, L⦄ ⊢ ⋆k •*[h, g, l] X → X = ⋆((next h)^l k). -#h #g #G #L #X #k #l #H @(lsstas_ind_dx … H) -X -l // -#l #X #X0 #_ #H #IHX destruct -lapply (ssta_inv_sort1 … H) -H #H destruct ->iter_SO // -qed-. - -lemma lsstas_inv_gref1: ∀h,g,G,L,X,p,l. ⦃G, L⦄ ⊢ §p •*[h, g, l+1] X → ⊥. -#h #g #G #L #X #p #l #H elim (lsstas_inv_step_sn … H) -H -#U #H #HUX elim (ssta_inv_gref1 … H) -qed-. - -lemma lsstas_inv_bind1: ∀h,g,a,I,G,L,V,T,X,l. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T •*[h, g, l] X → - ∃∃U. ⦃G, L.ⓑ{I}V⦄ ⊢ T •*[h, g, l] U & X = ⓑ{a,I}V.U. -#h #g #a #I #G #L #V #T #X #l #H @(lsstas_ind_dx … H) -X -l [ /2 width=3/ ] -#l #X #X0 #_ #HX0 * #U #HTU #H destruct -elim (ssta_inv_bind1 … HX0) -HX0 #U0 #HU0 #H destruct /3 width=3/ -qed-. - -lemma lsstas_inv_appl1: ∀h,g,G,L,V,T,X,l. ⦃G, L⦄ ⊢ ⓐV.T •*[h, g, l] X → - ∃∃U. ⦃G, L⦄ ⊢ T •*[h, g, l] U & X = ⓐV.U. -#h #g #G #L #V #T #X #l #H @(lsstas_ind_dx … H) -X -l [ /2 width=3/ ] -#l #X #X0 #_ #HX0 * #U #HTU #H destruct -elim (ssta_inv_appl1 … HX0) -HX0 #U0 #HU0 #H destruct /3 width=3/ -qed-. - -lemma lsstas_inv_cast1: ∀h,g,G,L,W,T,U,l. ⦃G, L⦄ ⊢ ⓝW.T •*[h, g, l+1] U → ⦃G, L⦄ ⊢ T •*[h, g, l+1] U. -#h #g #G #L #W #T #X #l #H elim (lsstas_inv_step_sn … H) -H -#U #H #HUX lapply (ssta_inv_cast1 … H) -H /2 width=3/ -qed-. - -(* Basic properties *********************************************************) - -lemma lsstas_refl: ∀h,g,G,L. reflexive … (lsstas h g G L 0). -// qed. - -lemma ssta_lsstas: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ T •*[h, g, 1] U. -/2 width=1/ qed. - -lemma lsstas_step_sn: ∀h,g,G,L,T1,U1,U2,l. ⦃G, L⦄ ⊢ T1 •[h, g] U1 → ⦃G, L⦄ ⊢ U1 •*[h, g, l] U2 → - ⦃G, L⦄ ⊢ T1 •*[h, g, l+1] U2. -/2 width=3/ qed. - -lemma lsstas_step_dx: ∀h,g,G,L,T1,T2,U2,l. ⦃G, L⦄ ⊢ T1 •*[h, g, l] T2 → ⦃G, L⦄ ⊢ T2 •[h, g] U2 → - ⦃G, L⦄ ⊢ T1 •*[h, g, l+1] U2. -/2 width=3/ qed. - -lemma lsstas_split: ∀h,g,G,L. inv_ltransitive … (lsstas h g G L). -/2 width=1 by lstar_inv_ltransitive/ qed-. - -lemma lsstas_sort: ∀h,g,G,L,l,k. ⦃G, L⦄ ⊢ ⋆k •*[h, g, l] ⋆((next h)^l k). -#h #g #G #L #l @(nat_ind_plus … l) -l // -#l #IHl #k >iter_SO /2 width=3/ -qed. - -lemma lsstas_bind: ∀h,g,I,G,L,V,T,U,l. ⦃G, L.ⓑ{I}V⦄ ⊢ T •*[h, g, l] U → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T •*[h, g, l] ⓑ{a,I}V.U. -#h #g #I #G #L #V #T #U #l #H @(lsstas_ind_dx … H) -U -l // /3 width=3/ -qed. - -lemma lsstas_appl: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •*[h, g, l] U → - ∀V.⦃G, L⦄ ⊢ ⓐV.T •*[h, g, l] ⓐV.U. -#h #g #G #L #T #U #l #H @(lsstas_ind_dx … H) -U -l // /3 width=3/ -qed. - -lemma lsstas_cast: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •*[h, g, l+1] U → - ∀W. ⦃G, L⦄ ⊢ ⓝW.T •*[h, g, l+1] U. -#h #g #G #L #T #U #l #H elim (lsstas_inv_step_sn … H) -H /3 width=3/ -qed. - -(* Basic_1: removed theorems 7: - sty1_abbr sty1_appl sty1_bind sty1_cast2 - sty1_correct sty1_lift sty1_trans -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_aaa.etc deleted file mode 100644 index e8d7fb837..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_aaa.etc +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/aaa_ssta.ma". -include "basic_2/unfold/lsstas.ma". - -(* NAT-ITERATED STATIC TYPE ASSIGNMENT FOR TERMS ****************************) - -(* Properties on atomic arity assignment for terms **************************) - -lemma aaa_lsstas_conf: ∀h,g,G,L,l. Conf3 … (aaa G L) (lsstas h g G L l). -/3 width=6 by aaa_ssta_conf, lstar_Conf3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_alt.etc deleted file mode 100644 index 849579fa8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_alt.etc +++ /dev/null @@ -1,102 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/statictypestaralt_7.ma". -include "basic_2/unfold/lsstas_lift.ma". - -(* NAT-ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *****************) - -(* alternative definition of lsstas *) -inductive lsstasa (h) (g): genv → relation4 lenv nat term term ≝ -| lsstasa_O : ∀G,L,T. lsstasa h g G L 0 T T -| lsstasa_sort: ∀G,L,l,k. lsstasa h g G L l (⋆k) (⋆((next h)^l k)) -| lsstasa_ldef: ∀G,L,K,V,W,U,i,l. ⇩[i] L ≡ K.ⓓV → lsstasa h g G K (l+1) V W → - ⇧[0, i+1] W ≡ U → lsstasa h g G L (l+1) (#i) U -| lsstasa_ldec: ∀G,L,K,W,V,U,i,l,l0. ⇩[i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W ▪[h, g] l0 → - lsstasa h g G K l W V → ⇧[0, i+1] V ≡ U → lsstasa h g G L (l+1) (#i) U -| lsstasa_bind: ∀a,I,G,L,V,T,U,l. lsstasa h g G (L.ⓑ{I}V) l T U → - lsstasa h g G L l (ⓑ{a,I}V.T) (ⓑ{a,I}V.U) -| lsstasa_appl: ∀G,L,V,T,U,l. lsstasa h g G L l T U → lsstasa h g G L l (ⓐV.T) (ⓐV.U) -| lsstasa_cast: ∀G,L,W,T,U,l. lsstasa h g G L (l+1) T U → lsstasa h g G L (l+1) (ⓝW.T) U -. - -interpretation "nat-iterated stratified static type assignment (term) alternative" - 'StaticTypeStarAlt h g G L l T U = (lsstasa h g G L l T U). - -(* Base properties **********************************************************) - -lemma ssta_lsstasa: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ T ••*[h, g, 1] U. -#h #g #G #L #T #U #H elim H -G -L -T -U -/2 width=8 by lsstasa_O, lsstasa_sort, lsstasa_ldef, lsstasa_ldec, lsstasa_bind, lsstasa_appl, lsstasa_cast/ -qed. - -lemma lsstasa_step_dx: ∀h,g,G,L,T1,T,l. ⦃G, L⦄ ⊢ T1 ••*[h, g, l] T → - ∀T2. ⦃G, L⦄ ⊢ T •[h, g] T2 → ⦃G, L⦄ ⊢ T1 ••*[h, g, l+1] T2. -#h #g #G #L #T1 #T #l #H elim H -G -L -T1 -T -l -[ /2 width=1/ -| #G #L #l #k #X #H >(ssta_inv_sort1 … H) -X >commutative_plus // -| #G #L #K #V #W #U #i #l #HLK #_ #HWU #IHVW #U2 #HU2 - lapply (ldrop_fwd_drop2 … HLK) #H - elim (ssta_inv_lift1 … HU2 … H … HWU) -H -U /3 width=6 by lsstasa_ldef/ -| #G #L #K #W #V #U #i #l #l0 #HLK #HWl0 #_ #HVU #IHWV #U2 #HU2 - lapply (ldrop_fwd_drop2 … HLK) #H - elim (ssta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8 by lsstasa_ldec/ -| #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H - elim (ssta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1 by lsstasa_bind/ -| #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H - elim (ssta_inv_appl1 … H) -H #U #HU1 #H destruct /3 width=1 by lsstasa_appl/ -| /3 width=1 by lsstasa_cast/ -] -qed. - -(* Main properties **********************************************************) - -theorem lsstas_lsstasa: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •*[h, g, l] U → ⦃G, L⦄ ⊢ T ••*[h, g, l] U. -#h #g #G #L #T #U #l #H @(lsstas_ind_dx … H) -U -l /2 width=3 by lsstasa_step_dx, lsstasa_O/ -qed. - -(* Main inversion lemmas ****************************************************) - -theorem lsstasa_inv_lsstas: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T ••*[h, g, l] U → ⦃G, L⦄ ⊢ T •*[h, g, l] U. -#h #g #G #L #T #U #l #H elim H -G -L -T -U -l -/2 width=8 by lsstas_inv_SO, lsstas_ldec, lsstas_ldef, lsstas_cast, lsstas_appl, lsstas_bind/ -qed-. - -(* Advanced eliminators *****************************************************) - -lemma lsstas_ind_alt: ∀h,g. ∀R:genv→relation4 lenv nat term term. - (∀G,L,T. R G L O T T) → - (∀G,L,l,k. R G L l (⋆k) (⋆((next h)^l k))) → ( - ∀G,L,K,V,W,U,i,l. - ⇩[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V •*[h, g, l+1] W → ⇧[O, i+1] W ≡ U → - R G K (l+1) V W → R G L (l+1) (#i) U - ) → ( - ∀G,L,K,W,V,U,i,l,l0. - ⇩[i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W ▪[h, g] l0 → - ⦃G, K⦄ ⊢ W •*[h, g, l]V → ⇧[O, i+1] V ≡ U → - R G K l W V → R G L (l+1) (#i) U - ) → ( - ∀a,I,G,L,V,T,U,l. ⦃G, L.ⓑ{I}V⦄ ⊢ T •*[h, g, l] U → - R G (L.ⓑ{I}V) l T U → R G L l (ⓑ{a,I}V.T) (ⓑ{a,I}V.U) - ) → ( - ∀G,L,V,T,U,l. ⦃G, L⦄ ⊢ T •*[h, g, l] U → - R G L l T U → R G L l (ⓐV.T) (ⓐV.U) - ) → ( - ∀G,L,W,T,U,l. ⦃G, L⦄⊢ T •*[h, g, l+1] U → - R G L (l+1) T U → R G L (l+1) (ⓝW.T) U - ) → - ∀G,L,l,T,U. ⦃G, L⦄ ⊢ T •*[h, g, l] U → R G L l T U. -#h #g #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #G #L #l #T #U #H -elim (lsstas_lsstasa … H) /3 width=10 by lsstasa_inv_lsstas/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_lift.etc deleted file mode 100644 index 2a7cc800e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_lift.etc +++ /dev/null @@ -1,90 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/ssta_lift.ma". -include "basic_2/unfold/lsstas.ma". - -(* NAT-ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *****************) - -(* Properties on relocation *************************************************) - -lemma lsstas_lift: ∀h,g,G,l. l_liftable (llstar … (ssta h g G) l). -/3 width=10 by l_liftable_llstar, ssta_lift/ qed. - -(* Inversion lemmas on relocation *******************************************) - -lemma lsstas_inv_lift1: ∀h,g,G,l. l_deliftable_sn (llstar … (ssta h g G) l). -/3 width=6 by l_deliftable_sn_llstar, ssta_inv_lift1/ qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma lsstas_inv_lref1: ∀h,g,G,L,U,i,l. ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U → - (∃∃K,V,W. ⇩[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V •*[h, g, l+1] W & - ⇧[0, i + 1] W ≡ U - ) ∨ - (∃∃K,W,V,l0. ⇩[i] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & - ⦃G, K⦄ ⊢ W •*[h, g, l] V & ⇧[0, i + 1] V ≡ U - ). -#h #g #G #L #U #i #l #H elim (lsstas_inv_step_sn … H) -H -#X #H #HXU elim (ssta_inv_lref1 … H) -H -* #K [ #V #W | #W #l0 ] #HLK [ #HVW | #HWl0 ] #HWX -lapply (ldrop_fwd_drop2 … HLK) #H0LK -elim (lsstas_inv_lift1 … HXU … H0LK … HWX) -H0LK -X -/4 width=8 by lsstas_step_sn, ex4_4_intro, ex3_3_intro, or_introl, or_intror/ -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma lsstas_fwd_correct: ∀h,g,G,L,T1,U1. ⦃G, L⦄ ⊢ T1 •[h, g] U1 → - ∀T2,l. ⦃G, L⦄ ⊢ T1 •*[h, g, l] T2 → - ∃U2. ⦃G, L⦄ ⊢ T2 •[h, g] U2. -#h #g #G #L #T1 #U1 #HTU1 #T2 #l #H @(lsstas_ind_dx … H) -l -T2 [ /2 width=3 by ex_intro/ ] -HTU1 -#l #T #T2 #_ #HT2 #_ -T1 -U1 -l -elim (ssta_fwd_correct … HT2) -T /2 width=2 by ex_intro/ -qed-. - -(* Advanced properties ******************************************************) - -lemma lsstas_total: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → - ∀l. ∃U0. ⦃G, L⦄ ⊢ T •*[h, g, l] U0. -#h #g #G #L #T #U #HTU #l @(nat_ind_plus … l) -l [ /2 width=2 by lstar_O, ex_intro/ ] -#l * #U0 #HTU0 -elim (lsstas_fwd_correct … HTU … HTU0) -U /3 width=4 by lsstas_step_dx, ex_intro/ -qed-. - -lemma lsstas_ldef: ∀h,g,G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → - ∀W,l. ⦃G, K⦄ ⊢ V •*[h, g, l+1] W → - ∀U. ⇧[0, i+1] W ≡ U → ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U. -#h #g #G #L #K #V #i #HLK #W #l #HVW #U #HWU -lapply (ldrop_fwd_drop2 … HLK) -elim (lsstas_inv_step_sn … HVW) -HVW #W0 -elim (lift_total W0 0 (i+1)) /3 width=12 by lsstas_step_sn, ssta_ldef, lsstas_lift/ -qed. - -lemma lsstas_ldec: ∀h,g,G,L,K,W,i. ⇩[i] L ≡ K.ⓛW → ∀l0. ⦃G, K⦄ ⊢ W ▪[h, g] l0 → - ∀V,l. ⦃G, K⦄ ⊢ W •*[h, g, l] V → - ∀U. ⇧[0, i+1] V ≡ U → ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U. -#h #g #G #L #K #W #i #HLK #T #HWT #V #l #HWV #U #HVU -lapply (ldrop_fwd_drop2 … HLK) #H -elim (lift_total W 0 (i+1)) /3 width=12 by lsstas_step_sn, ssta_ldec, lsstas_lift/ -qed. - -(* Properties on degree assignment for terms ********************************) - -lemma lsstas_da_conf: ∀h,g,G,L,T,U,l1. ⦃G, L⦄ ⊢ T •*[h, g, l1] U → - ∀l2. ⦃G, L⦄ ⊢ T ▪[h, g] l2 → ⦃G, L⦄ ⊢ U ▪[h, g] l2-l1. -#h #g #G #L #T #U #l1 #H @(lsstas_ind_dx … H) -U -l1 // -#l1 #U #U0 #_ #HU0 #IHTU #l2 #HT -(plus_minus_m_m … Hl12) in ⊢ (%→?); -Hl12 >commutative_plus #H -elim (lsstas_split … H) -H #U #HTU ->(lsstas_mono … HTU … HTU1) -T // -qed-. - -(* Advanced properties ******************************************************) - -lemma lsstas_ssta_conf_pos: ∀h,g,G,L,T,U1. ⦃G, L⦄ ⊢ T •[h, g] U1 → - ∀U2,l. ⦃G, L⦄ ⊢ T •*[h, g, l+1] U2 → ⦃G, L⦄ ⊢ U1 •*[h, g, l] U2. -#h #g #G #L #T #U1 #HTU1 #U2 #l #HTU2 -lapply (lsstas_conf_le … T U1 1 … HTU2) -HTU2 // /2 width=1/ -qed-. - -lemma lsstas_strip_pos: ∀h,g,G,L,T1,U1. ⦃G, L⦄ ⊢ T1 •[h, g] U1 → - ∀T2,l. ⦃G, L⦄ ⊢ T1 •*[h, g, l+1] T2 → - ∃∃U2. ⦃G, L⦄ ⊢ T2 •[h, g] U2 & ⦃G, L⦄ ⊢ U1 •*[h, g, l+1] U2. -#h #g #G #L #T1 #U1 #HTU1 #T2 #l #HT12 -elim (lsstas_fwd_correct … HTU1 … HT12) -lapply (lsstas_ssta_conf_pos … HTU1 … HT12) -T1 /3 width=5/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_cpds.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_cpds.etc deleted file mode 100644 index a4d4cff8d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_cpds.etc +++ /dev/null @@ -1,31 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/dynamic/lsubsv_lsstas.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) - -(* Properties on decomposed extended parallel computation on terms **********) - -lemma lsubsv_cpds_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g] T2 → - ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] T & ⦃G, L1⦄ ⊢ T2 ➡* T. -#h #g #G #L2 #T1 #T2 * #T #l1 #l2 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12 -lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2 -elim (lsubsv_lsstas_trans … HT1 … Hl1 … HL12) // #T0 #HT10 #HT0 -lapply (lsubsv_fwd_lsubd … HL12) -HL12 #HL12 -lapply (lsubd_da_trans … Hl1 … HL12) -L2 #Hl1 -lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02 -elim (cpcs_inv_cprs … HT02) -HT02 /3 width=7/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_lsstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_lsstas.etc deleted file mode 100644 index ec2ae57bc..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_lsstas.etc +++ /dev/null @@ -1,89 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lsubd_da.ma". -include "basic_2/unfold/lsstas_alt.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/dynamic/lsubsv_ldrop.ma". -include "basic_2/dynamic/lsubsv_lsubd.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) - -(* Properties on nat-iterated stratified static type assignment *************) - -lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1] U2 → - ∀l2. l1 ≤ l2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l2 → - ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → - ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, g, l1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2. -#h #g #G #L2 #T #U #l1 #H @(lsstas_ind_alt … H) -G -L2 -T -U -l1 -[1,2: /2 width=3 by lstar_O, ex2_intro/ -| #G #L2 #K2 #X #Y #U #i #l1 #HLK2 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12 - elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0 - lapply (ldrop_mono … HK0 … HLK2) -HK0 #H destruct - elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HYU -IHXY -HLK1 ] - [ #HK12 #H destruct - elim (IHXY … Hl12 HV0 … HK12) -K2 -l2 #T #HXT #HTY - lapply (ldrop_fwd_drop2 … HLK1) #H - elim (lift_total T 0 (i+1)) - /3 width=12 by lsstas_ldef, cpcs_lift, ex2_intro/ - | #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct - ] -| #G #L2 #K2 #X #Y #U #i #l1 #l #HLK2 #_ #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12 -l - elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0 [| #H1 ] - lapply (ldrop_mono … HK0 … HLK2) -HK0 #H2 destruct - lapply (le_plus_to_le_r … Hl12) -Hl12 #Hl12 - elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubsv_inv_pair2 … H) -H * #K1 [| ] - [ #HK12 #H destruct - lapply (lsubsv_fwd_lsubd … HK12) #H - lapply (lsubd_da_trans … HV0 … H) -H - elim (IHXY … Hl12 HV0 … HK12) -K2 -Hl12 #Y0 - lapply (ldrop_fwd_drop2 … HLK1) - elim (lift_total Y0 0 (i+1)) - /3 width=12 by lsstas_ldec, cpcs_lift, ex2_intro/ - | #V #l #_ #_ #HVX #_ #HV #HX #HK12 #_ #H destruct - lapply (da_mono … HX … HV0) -HX #H destruct - elim (IHXY … Hl12 HV0 … HK12) -K2 #Y0 #HXY0 #HY0 - elim (da_ssta … HV) -HV #W #HVW - elim (lsstas_total … HVW (l1+1)) -W #W #HVW - lapply (HVX … Hl12 HVW HXY0) -HVX -Hl12 -HXY0 #HWY0 - lapply (cpcs_trans … HWY0 … HY0) -Y0 - lapply (ldrop_fwd_drop2 … HLK1) - elim (lift_total W 0 (i+1)) - /4 width=12 by lsstas_ldef, lsstas_cast, cpcs_lift, ex2_intro/ - ] -| #a #I #G #L2 #V2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12 - lapply (da_inv_bind … Hl2) -Hl2 #Hl2 - elim (IHTU2 … Hl2 (L1.ⓑ{I}V2) …) // [2: /2 width=1/ ] -L2 - /3 width=3 by lsstas_bind, cpcs_bind_dx, ex2_intro/ -| #G #L2 #V2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12 - lapply (da_inv_flat … Hl2) -Hl2 #Hl2 - elim (IHTU2 … Hl2 … HL12) -L2 // - /3 width=5 by lsstas_appl, cpcs_flat, ex2_intro/ -| #G #L2 #W2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12 - lapply (da_inv_flat … Hl2) -Hl2 #Hl2 - elim (IHTU2 … Hl2 … HL12) -L2 // - /3 width=3 by lsstas_cast, ex2_intro/ -] -qed-. - -lemma lsubsv_ssta_trans: ∀h,g,G,L2,T,U2. ⦃G, L2⦄ ⊢ T •[h, g] U2 → - ∀l. ⦃G, L2⦄ ⊢ T ▪[h, g] l+1 → - ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → - ∃∃U1. ⦃G, L1⦄ ⊢ T •[h, g] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2. -#h #g #G #L2 #T #U2 #H #l #HTl #L1 #HL12 -elim ( lsubsv_lsstas_trans … U2 1 … HTl … HL12) -/3 width=3 by lsstas_inv_SO, ssta_lsstas, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_snv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_snv.etc deleted file mode 100644 index e4596e7d4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_snv.etc +++ /dev/null @@ -1,52 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/cpds_cpds.ma". -include "basic_2/dynamic/snv_aaa.ma". -include "basic_2/dynamic/lsubsv_cpds.ma". -include "basic_2/dynamic/lsubsv_cpcs.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) - -(* Properties concerning stratified native validity *************************) - -lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] → - ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g]. -#h #g #G #L2 #T #H elim H -G -L2 -T // -[ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12 - elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubsv_inv_pair2 … H) -H * #K1 - [ #HK12 #H destruct /3 width=5 by snv_lref/ - | #W #l #H1V #H1W #HWV #_ #HWl #_ #_ #H1 #H2 destruct -IHV - /3 width=10 by snv_scast, snv_lref/ - ] -| #a #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 destruct - /4 width=1 by snv_bind, lsubsv_pair/ -| #a #G #L2 #V #W #W0 #T #U #l #_ #_ #HVl #HVW #HW0 #HTU #IHV #IHT #L1 #HL12 - lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0 - elim (lsubsv_ssta_trans … HVW … HVl … HL12) -HVW #W1 #HVW1 #HW1 - lapply (cpcs_cprs_strap1 … HW1 … HW0) -W #HW10 - lapply (lsubd_da_trans … HVl L1 ?) -HVl /2 width=1 by lsubsv_fwd_lsubd/ #HVl - elim (lsubsv_cpds_trans … HTU … HL12) -HTU #X #HTU #H - elim (cprs_inv_abst1 … H) -H #W #U2 #HW0 #_ #H destruct - lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H - elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0 - /4 width=11 by snv_appl, cpds_cprs_trans, cprs_bind/ -| #G #L2 #W #T #U #l #_ #_ #HTl #HTU #HUW #IHW #IHT #L1 #HL12 - lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW - elim (lsubsv_ssta_trans … HTU … HTl … HL12) -HTU #U0 #HTU0 #HU0 - lapply (lsubd_da_trans … HTl L1 ?) -HTl - /4 width=5 by lsubsv_fwd_lsubd, snv_cast, cpcs_trans/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv.etc deleted file mode 100644 index 7bdef30fa..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv.etc +++ /dev/null @@ -1,119 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/nativevalid_5.ma". -include "basic_2/computation/cpds.ma". -include "basic_2/equivalence/cpcs.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -definition scast: ∀h. sd h → nat → relation4 genv lenv term term ≝ - λh,g,l,G,L,V,W. ∀V0,W0,l0. - l0 ≤ l → ⦃G, L⦄ ⊢ V •*[h, g, l0+1] V0 → ⦃G, L⦄ ⊢ W •*[h, g, l0] W0 → ⦃G, L⦄ ⊢ V0 ⬌* W0. - -(* activate genv *) -inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝ -| snv_sort: ∀G,L,k. snv h g G L (⋆k) -| snv_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i) -| snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T) -| snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T → - ⦃G, L⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ V •[h, g] W → ⦃G, L⦄ ⊢ W ➡* W0 → - ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g G L (ⓐV.T) -| snv_cast: ∀G,L,W,T,U,l. snv h g G L W → snv h g G L T → - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ U ⬌* W → snv h g G L (ⓝW.T) -. - -interpretation "stratified native validity (term)" - 'NativeValid h g G L T = (snv h g G L T). - -(* Basic inversion lemmas ***************************************************) - -fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i → - ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. -#h #g #G #L #X * -G -L -X -[ #G #L #k #i #H destruct -| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5 by ex2_3_intro/ -| #a #I #G #L #V #T #_ #_ #i #H destruct -| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #i #H destruct -| #G #L #W #T #U #l #_ #_ #_ #_ #_ #i #H destruct -] -qed-. - -lemma snv_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] → - ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. -/2 width=3 by snv_inv_lref_aux/ qed-. - -fact snv_inv_gref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥. -#h #g #G #L #X * -G -L -X -[ #G #L #k #p #H destruct -| #I #G #L #K #V #i #_ #_ #p #H destruct -| #a #I #G #L #V #T #_ #_ #p #H destruct -| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #p #H destruct -| #G #L #W #T #U #l #_ #_ #_ #_ #_ #p #H destruct -] -qed-. - -lemma snv_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ §p ¡[h, g] → ⊥. -/2 width=8 by snv_inv_gref_aux/ qed-. - -fact snv_inv_bind_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → - ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. -#h #g #G #L #X * -G -L -X -[ #G #L #k #a #I #V #T #H destruct -| #I0 #G #L #K #V0 #i #_ #_ #a #I #V #T #H destruct -| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1 by conj/ -| #b #G #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_#_ #_ #a #I #V #T #H destruct -| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct -] -qed-. - -lemma snv_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] → - ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. -/2 width=4 by snv_inv_bind_aux/ qed-. - -fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T → - ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & - ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. -#h #g #G #L #X * -L -X -[ #G #L #k #V #T #H destruct -| #I #G #L #K #V0 #i #_ #_ #V #T #H destruct -| #a #I #G #L #V0 #T0 #_ #_ #V #T #H destruct -| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #Hl #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8 by ex6_5_intro/ -| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #V #T #H destruct -] -qed-. - -lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] → - ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & - ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. -/2 width=3 by snv_inv_appl_aux/ qed-. - -fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T → - ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h, g] U & ⦃G, L⦄ ⊢ U ⬌* W. -#h #g #G #L #X * -G -L -X -[ #G #L #k #W #T #H destruct -| #I #G #L #K #V #i #_ #_ #W #T #H destruct -| #a #I #G #L #V #T0 #_ #_ #W #T #H destruct -| #a #G #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #_ #W #T #H destruct -| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #Hl #HTU0 #HUW0 #W #T #H destruct /2 width=4 by ex5_2_intro/ -] -qed-. - -lemma snv_inv_cast: ∀h,g,G,L,W,T. ⦃G, L⦄ ⊢ ⓝW.T ¡[h, g] → - ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h, g] U & ⦃G, L⦄ ⊢ U ⬌* W. -/2 width=3 by snv_inv_cast_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_aaa.etc deleted file mode 100644 index 20d72ef3e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_aaa.etc +++ /dev/null @@ -1,66 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/csx_aaa.ma". -include "basic_2/computation/cpds_aaa.ma". -include "basic_2/equivalence/cpcs_aaa.ma". -include "basic_2/dynamic/snv.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Forward lemmas on atomic arity assignment for terms **********************) - -lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A. -#h #g #G #L #T #H elim H -G -L -T -[ /2 width=2/ -| #I #G #L #K #V #i #HLK #_ * /3 width=6/ -| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/ -| #a #G #L #V #W #W0 #T #U #l #_ #_ #Hl #HVW #HW0 #HTU * #B #HV * #X #HT - lapply (aaa_cpds_conf h g … HV W0 ?) [ -HTU /3 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *) - lapply (aaa_cpds_conf … HT … HTU) -HTU #H - elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct - lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/ -| #G #L #W #T #U #l #_ #_ #_ #HTU #HUW * #B #HW * #A #HT - lapply (aaa_ssta_conf … HT … HTU) -HTU #H - lapply (aaa_cpcs_mono … HUW … H … HW) -HUW -H #H destruct /3 width=3/ -] -qed-. - -lemma snv_fwd_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/ -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma snv_fwd_da: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l. -#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fwd_da/ -qed-. - -lemma snv_fwd_ssta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃U. ⦃G, L⦄ ⊢ T •[h, g] U. -#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fwd_ssta/ -qed-. - -lemma snv_lsstas_fwd_correct: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, g, l] T2 → - ∃U2. ⦃G, L⦄ ⊢ T2 •[h, g] U2. -#h #g #G #L #T1 #T2 #l #HT1 #HT12 -elim (snv_fwd_ssta … HT1) -HT1 /2 width=5 by lsstas_fwd_correct/ -qed-. - -(* Advanced properties ******************************************************) - -lemma snv_scast: ∀h,g,G,L,V,W,l. ⦃G, L⦄ ⊢ V ¡[h, g] → ⦃G, L⦄ ⊢ W ¡[h, g] → - scast h g l G L V W → ⦃G, L⦄ ⊢V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ ⓝW.V ¡[h, g]. -#h #g #G #L #V #W #l #HV #HW #H #Hl -elim (snv_fwd_ssta … HV) /4 width=6 by snv_cast, ssta_lsstas/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_cpcs.etc deleted file mode 100644 index e73f809fc..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_cpcs.etc +++ /dev/null @@ -1,169 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/unfold/lsstas_lsstas.ma". -include "basic_2/computation/fpbs_lift.ma". -include "basic_2/computation/fpbg_fleq.ma". -include "basic_2/equivalence/cpes_cpds.ma". -include "basic_2/dynamic/snv.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Inductive premises for the preservation results **************************) - -definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ - λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. - -definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ - λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. - -definition IH_lsstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ - λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. - -definition IH_snv_lsstas: ∀h:sh. sd h → relation3 genv lenv term ≝ - λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 → - ∀U. ⦃G, L⦄ ⊢ T •*[h, g, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g]. - -(* Properties for the preservation results **********************************) - -fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. -#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H -@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/ -qed-. - -fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. -#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H -@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ -qed-. - -fact da_cpcs_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → - ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 → - ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2. -#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l1 #Hl1 #l2 #Hl2 #H -elim (cpcs_inv_cprs … H) -H /4 width=18 by da_cprs_lpr_aux, da_mono/ -qed-. - -fact ssta_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •[h, g] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #H01 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12 -elim (IH … H01 … 1 … Hl U1 … HT12 … HL12) -H01 -Hl -HT12 -HL12 -/3 width=3 by lsstas_inv_SO, ssta_lsstas, ex2_intro/ -qed-. - -fact lsstas_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=10 by/ ] -#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 -elim (IHT1 L1) // -IHT1 #U #HTU #HU1 -elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 -[2: /3 width=12 by da_cprs_lpr_aux/ -|3: /3 width=10 by snv_cprs_lpr_aux/ -|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/ -] -G0 -L0 -T0 -T1 -T -l1 -/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ -qed-. - -fact lsstas_cpcs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l] U1 → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → - ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, g, l] U2 → - ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #H02 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12 -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (lsstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1 -elim (lsstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0 -lapply (lsstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ -qed-. - -fact snv_ssta_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → - ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → - ∀U. ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ U ¡[h, g]. -/3 width=8 by lsstas_inv_SO, ssta_lsstas/ qed-. - -fact lsstas_cpds_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → - ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → - ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, g, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2. -#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2 -lapply (da_mono … H … Hl1) -H #H destruct -lapply (lsstas_da_conf … HTU1 … Hl1) #Hl12 -elim (le_or_ge l2 l) #Hl2 -[ lapply (lsstas_conf_le … HTU1 … HT1T) -HT1T - /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/ -| lapply (lsstas_da_conf … HT1T … Hl1) #Hl1l - lapply (lsstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 - elim (lsstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) -IH3 -IH2 -IH1 -Hl1l -HTU1 -HTT2 - /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l, ex3_2_intro/ -] -qed-. - -fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. -#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 -elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12 -lapply (IH2 … H01 … Hl1 … HT12 … HL12) -L0 -T0 // -T1 -lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 -lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H -elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_da_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_da_lpr.etc deleted file mode 100644 index dd56de7a2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_da_lpr.etc +++ /dev/null @@ -1,94 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lsubd_da.ma". -include "basic_2/computation/cpds_cpds.ma". -include "basic_2/dynamic/snv_aaa.ma". -include "basic_2/dynamic/snv_cpcs.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on degree assignment for terms ********************************) - -fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h g G1 L1 T1. -#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #k #_ #_ #_ #_ #l #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1 - lapply (da_inv_sort … H2) -H2 - lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1 by da_sort/ -| #i #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 - elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #H #HX0 - elim (da_inv_lref … H2) -H2 * #K1 [ #V1 | #W1 #l1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct - lapply (ldrop_mono … H … HLK1) -H #H destruct - elim (cpr_inv_lref1 … H3) -H3 - [1,3: #H destruct - lapply (fqup_lref … G1 … HLK1) - elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 - elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - /4 width=10 by da_ldef, da_ldec, fqup_fpbg/ - |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0 - lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (fqup_lref … G1 … HLK1) - elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 - elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct - lapply (ldrop_fwd_drop2 … HLK2) -V2 - /4 width=8 by da_lift, fqup_fpbg/ - ] -| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH2 - elim (snv_inv_bind … H1) -H1 #_ #HT1 - lapply (da_inv_bind … H2) -H2 - elim (cpr_inv_bind1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct - /4 width=9 by da_bind, fqup_fpbg, lpr_pair/ - | #T2 #HT12 #HT2 #H1 #H2 destruct - /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_drop/ - ] -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct - elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 - lapply (da_inv_flat … H2) -H2 #Hl - elim (cpr_inv_appl1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/ - | #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW #HU1 - lapply (da_inv_bind … Hl) -Hl #Hl - elim (cpds_inv_abst1 … HT10) -HT10 #W3 #U3 #HW3 #_ #H destruct -U3 - lapply (cprs_div … HW3 … HW10) -W3 #HWW1 - lapply (ssta_da_conf … HVW1 … Hl0) (lift_inv_sort1 … H) -X -K -d -e // -| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #d #e #HLK #X #H - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (ldrop_trans_le … HLK … HK0) -K /2 width=2 by lt_to_le/ #X #HL0 #H - elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #L0 #W #HLK0 #HVW #H destruct - /3 width=9 by snv_lref/ - | lapply (ldrop_trans_ge … HLK … HK0 ?) -K - /3 width=9 by snv_lref, ldrop_inv_gen/ - ] -| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #s #d #e #HLK #X #H - elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct - /4 width=5 by snv_bind, ldrop_skip/ -| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #Hl #HV0 #HV01 #HT1 #IHV #IHT #L #s #d #e #HLK #X #H - elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct - elim (lift_total V0 d e) #W0 #HVW0 - elim (lift_total V1 d e) #W1 #HVW1 - elim (lift_total T1 (d+1) e) #U1 #HTU1 - @(snv_appl … a … W0 … W1 … U1 l) - [1,2,3,4,5: /2 width=10 by cprs_lift, ssta_lift, da_lift/ ] - @(cpds_lift … HT1 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typecjhecker failure *) -| #G #K #V0 #T #V #l #_ #_ #Hl #HTV #HV0 #IHV0 #IHT #L #s #d #e #HLK #X #H - elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct - elim (lift_total V d e) - /3 width=12 by snv_cast, cpcs_lift, ssta_lift, da_lift/ -] -qed. - -lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g]. -#h #g #G #L #U #H elim H -G -L -U -[ #G #L #k #K #s #d #e #_ #X #H - >(lift_inv_sort2 … H) -X -L -d -e // -| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #s #d #e #HLK #X #H - elim (lift_inv_lref2 … H) * #Hid #H destruct - [ elim (ldrop_conf_le … HLK … HL0) -L /2 width=2 by lt_to_le/ #X #HK0 #H - elim (ldrop_inv_skip1 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K0 #V #HLK0 #HVW #H destruct - /3 width=12 by snv_lref/ - | lapply (ldrop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/ - ] -| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #s #d #e #HLK #X #H - elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct - /4 width=5 by snv_bind, ldrop_skip/ -| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #Hl #HW0 #HW01 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H - elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct - lapply (da_inv_lift … Hl … HLK … HVW) -Hl #Hl - elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0 - elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01 - elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU - elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct - lapply (lift_inj … HY … HVW1) -HY #H destruct - /3 width=8 by snv_appl/ -| #G #L #W0 #U #W #l #_ #_ #Hl #HUW #HW0 #IHW0 #IHU #K #s #d #e #HLK #X #H - elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct - lapply (da_inv_lift … Hl … HLK … HTU) -Hl #Hl - elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HVW #HTV - lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W - /3 width=8 by snv_cast/ -] -qed-. - -(* Advanced properties ******************************************************) - -lemma snv_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g]. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I1 #G1 #L1 #V1 #H - elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2 - lapply (ldrop_inv_O2 … H) -H #H destruct // -|2: * -|5,6: /3 width=8 by snv_inv_lift/ -] -[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // -|2,4: * #G1 #L1 #V1 #T1 #H - [1,3: elim (snv_inv_appl … H) -H // - |2,4: elim (snv_inv_cast … H) -H // - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lpr.etc deleted file mode 100644 index f73c20a5e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lpr.etc +++ /dev/null @@ -1,132 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/dynamic/snv_lift.ma". -include "basic_2/dynamic/snv_cpcs.ma". -include "basic_2/dynamic/lsubsv_snv.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on context-free parallel reduction for local environments *****) - -fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g G1 L1 T1. -#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #k #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1 - >(cpr_inv_sort1 … H2) -X // -| #i #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 - elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 - elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - lapply (fqup_lref … G1 … HLK1) #HKL - elim (cpr_inv_lref1 … H2) -H2 - [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/ - | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12 - lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct - lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=8 by fqup_fpbg, snv_lift/ - ] -| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #HV1 #HT1 - elim (cpr_inv_bind1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/ - | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 - /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_drop/ - ] -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct - elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1 - elim (cpr_inv_appl1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 - lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 - lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 - lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0 - elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12 - elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H - elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct - lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10 - lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 - lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20 - elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200 - lapply (cpds_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) - /2 width=7 by snv_appl, cprs_bind/ - | #b #V2 #W20 #W2 #T20 #T2 #HV12 #HW202 #HT202 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 - elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 - lapply (cprs_div … HW10 … HW230) -W30 #HW120 - lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10 - lapply (ssta_da_conf … HVW1 … Hl0) ≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lsstas h g G1 L1 T1. -#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #k #HG0 #HL0 #HT0 #_ #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 - >(lsstas_inv_sort1 … H2) -X // -| #i #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 - [ lapply (lsstas_inv_O … H2) -H2 #H destruct // ] - elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HLK0 #HX0 - elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l ] #HLK1 [ #Hl1 | #Hl #H ] - lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H0 destruct - elim (lsstas_inv_lref1 … H2) -H2 * #K0 #Y0 #X0 [2,4: #l0 ] #HLK0 [1,2: #HYl0 ] #HYX0 #HX0 - lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct - [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ] - lapply (fqup_lref … G1 … HLK1) #H - lapply (ldrop_fwd_drop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/ -| #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #HV1 #HT1 - lapply (da_inv_bind … Hl1) -Hl1 #Hl1 - elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/ -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 - lapply (da_inv_flat … Hl1) -Hl1 #Hl1 - elim (lsstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct - lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbg/ #HU1 - elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2 - elim (lsstas_inv_bind1 … H) -H #U0 #_ #H destruct -T0 -l - elim (cpes_inv_abst2 … HU10) -HU10 #W2 #U2 #HU12 #HU02 - elim (cprs_inv_abst … HU02) -HU02 #HW02 #_ - /3 width=7 by snv_appl, cprs_trans/ -| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 - [ lapply (lsstas_inv_O … H2) -H2 #H destruct // ] - elim (snv_inv_cast … H1) -H1 - lapply (da_inv_flat … Hl1) -Hl1 - lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lsstas_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lsstas_lpr.etc deleted file mode 100644 index 1ee5ba08e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lsstas_lpr.etc +++ /dev/null @@ -1,151 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/cpds_cpds.ma". -include "basic_2/dynamic/snv_aaa.ma". -include "basic_2/dynamic/snv_cpcs.ma". -include "basic_2/dynamic/lsubsv_lsstas.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on sn parallel reduction for local environments ***************) - -fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lsstas_cpr_lpr h g G1 L1 T1. -#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #k #_ #_ #_ #_ #l1 #l2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1 - >(lsstas_inv_sort1 … H2) -X2 - >(cpr_inv_sort1 … H3) -X3 /2 width=3 by cpr_atom, ex2_intro/ -| #i #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 - [ lapply (lsstas_inv_O … H2) -H2 #H destruct -IH1 -H1 -l1 /4 width=5 by lpr_cpcs_conf, cpr_cpcs_dx, ex2_intro/ ] - elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HK0 #HX0 - elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l0 ] #HLK1 [ #HVl1 | #HWl1 #H destruct ] - lapply (ldrop_mono … HK0 … HLK1) -HK0 #H destruct - elim (lsstas_inv_lref1 … H2) -H2 * #K0 #V0 #W0 [2,4: #l ] #HK0 [1,2: #Hl ] #HW0 #HX2 - lapply (ldrop_mono … HK0 … HLK1) -HK0 #H destruct - [ lapply (da_mono … Hl … HWl1) -Hl #H destruct - lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 - ] - lapply (fqup_lref … G1 … HLK1) #HKV1 - elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct - lapply (ldrop_fwd_drop2 … HLK2) #H2 - elim (cpr_inv_lref1 … H3) -H3 - [1,3: #H destruct -HLK1 - |2,4: * #K0 #V0 #X0 #H #HVX0 #HX0 - lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct - ] - [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2 - elim (lift_total V2 0 (i+1)) - /6 width=12 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/ - | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02 - elim (lift_total W2 0 (i+1)) - /4 width=12 by cpcs_lift, lsstas_ldef, ex2_intro/ - | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02 - elim (lift_total W2 0 (i+1)) - /3 width=12 by cpcs_lift, lsstas_lift, ex2_intro/ - ] -| #p #_ #_ #HT0 #H1 destruct -IH4 -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #_ #HT1 - lapply (da_inv_bind … Hl1) -Hl1 #Hl1 - elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct - elim (cpr_inv_bind1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct - elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 - /4 width=5 by cpcs_bind2, lpr_cpr_conf, lsstas_bind, ex2_intro/ - | #T3 #HT13 #HXT3 #H1 #H2 destruct - elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13 - elim (lsstas_inv_lift1 … HTU3 L2 … HXT3) -T3 - /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_drop, ex2_intro/ - ] -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10 - lapply (da_inv_flat … Hl1) -Hl1 #Hl1 - elim (lsstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct - elim (cpr_inv_appl1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH4 -IH3 -IH2 - elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 - /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/ - | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2 - lapply (da_inv_bind … Hl1) -Hl1 #Hl1 - elim (lsstas_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct - elim (cpds_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW20 #_ #H destruct - lapply (cprs_div … HW10 … HW20) -W0 #HW12 - lapply (ssta_da_conf … HVW1 … Hl0) (lift_inv_sort1 … H1) -X1 - >(lift_inv_sort1 … H2) -X2 // -| #G #L1 #K1 #V1 #U1 #W1 #i #HLK1 #_ #HWU1 #IHVW1 #L2 #s #d #e #HL21 #X #H #U2 #HU12 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HWU1 … HU12) -U1 // #W2 #HW12 #HWU2 - elim (ldrop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H - elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K2 #V2 #HK21 #HV12 #H destruct - /3 width=9 by ssta_ldef/ - | lapply (lift_trans_be … HWU1 … HU12 ? ?) -U1 /2 width=1 by le_S/ #HW1U2 - lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid - /3 width=9 by ssta_ldef, ldrop_inv_gen/ - ] -| #G #L1 #K1 #W1 #U1 #l #i #HLK1 #HW1l #HWU1 #L2 #s #d #e #HL21 #X #H #U2 #HU12 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HWU1 … HU12) -U1 // (lift_inv_sort2 … H) -X /2 width=3 by ssta_sort, lift_sort, ex2_intro/ -| #G #L2 #K2 #V2 #U2 #W2 #i #HLK2 #HVW2 #HWU2 #IHVW2 #L1 #s #d #e #HL21 #X #H - elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ] - [ elim (ldrop_conf_lt … HL21 … HLK2) -L2 // #K1 #V1 #HLK1 #HK21 #HV12 - elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HW12 #HVW1 - elim (lift_trans_le … HW12 … HWU2) -W2 // >minus_plus minus_minus_m_m - /3 width=8 by ssta_ldef, le_S, ex2_intro/ - | minus_plus minus_minus_m_m - /3 width=8 by ssta_ldec, le_S, ex2_intro/ - | (ssta_inv_sort1 … H) -X // -| #G #L #K #V #U1 #W #i #HLK #_ #HWU1 #IHVW #U2 #H - elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HW0U2 - lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct - lapply (IHVW … HVW0) -IHVW -HVW0 #H destruct - >(lift_mono … HWU1 … HW0U2) -W0 -U1 // -| #G #L #K #W #U1 #l #i #HLK #HWl #HWU1 #U2 #H - elim (ssta_inv_lref1 … H) -H * #K0 #W0 #l0 #HLK0 #HWl0 #HW0U2 - lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct - lapply (da_mono … HWl0 … HWl) -HWl0 #H destruct - >(lift_mono … HWU1 … HW0U2) -W -U1 // -| #a #I #G #L #V #T #U1 #_ #IHTU1 #X #H - elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ -| #G #L #V #T #U1 #_ #IHTU1 #X #H - elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ -| #G #L #W #T #U1 #_ #IHTU1 #U2 #H - lapply (ssta_inv_cast1 … H) -H /2 width=1/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictype_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictype_6.etc deleted file mode 100644 index 3861e34e1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictype_6.etc +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 h , break term 46 g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'StaticType $h $g $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictypestar_7.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictypestar_7.etc deleted file mode 100644 index a738fe57a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictypestar_7.etc +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 •* break [ term 46 h , break term 46 g , break term 46 l ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'StaticTypeStar $h $g $G $L $l $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictypestaralt_7.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictypestaralt_7.etc deleted file mode 100644 index f4b2828eb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/statictypestaralt_7.etc +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • • * break [ term 46 h , break term 46 g , break term 46 l ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'StaticTypeStarAlt $h $g $G $L $l $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta.etc deleted file mode 100644 index 6eba700b1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta.etc +++ /dev/null @@ -1,145 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/statictype_7.ma". -include "basic_2/grammar/genv.ma". -include "basic_2/relocation/ldrop.ma". -include "basic_2/static/sd.ma". - -(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) - -(* activate genv *) -inductive ssta (h:sh) (g:sd h): nat → relation4 genv lenv term term ≝ -| ssta_sort: ∀G,L,k,l. deg h g k l → ssta h g l G L (⋆k) (⋆(next h k)) -| ssta_ldef: ∀G,L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l G K V W → - ⇧[0, i + 1] W ≡ U → ssta h g l G L (#i) U -| ssta_ldec: ∀G,L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → ssta h g l G K W V → - ⇧[0, i + 1] W ≡ U → ssta h g (l+1) G L (#i) U -| ssta_bind: ∀a,I,G,L,V,T,U,l. ssta h g l G (L. ⓑ{I} V) T U → - ssta h g l G L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U) -| ssta_appl: ∀G,L,V,T,U,l. ssta h g l G L T U → - ssta h g l G L (ⓐV.T) (ⓐV.U) -| ssta_cast: ∀G,L,W,T,U,l. ssta h g l G L T U → ssta h g l G L (ⓝW.T) U -. - -interpretation "stratified static type assignment (term)" - 'StaticType h g G L T U l = (ssta h g l G L T U). - -definition ssta_step: ∀h. sd h → relation4 genv lenv term term ≝ - λh,g,G,L,T,U. ∃l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄. - -(* Basic inversion lemmas ************************************************) - -fact ssta_inv_sort1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀k0. T = ⋆k0 → - deg h g k0 l ∧ U = ⋆(next h k0). -#h #g #G #L #T #U #l * -G -L -T -U -l -[ #G #L #k #l #Hkl #k0 #H destruct /2 width=1/ -| #G #L #K #V #W #U #i #l #_ #_ #_ #k0 #H destruct -| #G #L #K #W #V #U #i #l #_ #_ #_ #k0 #H destruct -| #a #I #G #L #V #T #U #l #_ #k0 #H destruct -| #G #L #V #T #U #l #_ #k0 #H destruct -| #G #L #W #T #U #l #_ #k0 #H destruct -qed-. - -lemma ssta_inv_sort1: ∀h,g,G,L,U,k,l. ⦃G, L⦄ ⊢ ⋆k •[h, g] ⦃l, U⦄ → - deg h g k l ∧ U = ⋆(next h k). -/2 width=5 by ssta_inv_sort1_aux/ qed-. - -fact ssta_inv_lref1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀j. T = #j → - (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V •[h, g] ⦃l, W⦄ & - ⇧[0, j + 1] W ≡ U - ) ∨ - (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃G, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ & - ⇧[0, j + 1] W ≡ U & l = l0 + 1 - ). -#h #g #G #L #T #U #l * -G -L -T -U -l -[ #G #L #k #l #_ #j #H destruct -| #G #L #K #V #W #U #i #l #HLK #HVW #HWU #j #H destruct /3 width=6/ -| #G #L #K #W #V #U #i #l #HLK #HWV #HWU #j #H destruct /3 width=8/ -| #a #I #G #L #V #T #U #l #_ #j #H destruct -| #G #L #V #T #U #l #_ #j #H destruct -| #G #L #W #T #U #l #_ #j #H destruct -] -qed-. - -lemma ssta_inv_lref1: ∀h,g,G,L,U,i,l. ⦃G, L⦄ ⊢ #i •[h, g] ⦃l, U⦄ → - (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V •[h, g] ⦃l, W⦄ & - ⇧[0, i + 1] W ≡ U - ) ∨ - (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃G, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ & - ⇧[0, i + 1] W ≡ U & l = l0 + 1 - ). -/2 width=3 by ssta_inv_lref1_aux/ qed-. - -fact ssta_inv_gref1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀p0. T = §p0 → ⊥. -#h #g #G #L #T #U #l * -G -L -T -U -l -[ #G #L #k #l #_ #p0 #H destruct -| #G #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct -| #G #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct -| #a #I #G #L #V #T #U #l #_ #p0 #H destruct -| #G #L #V #T #U #l #_ #p0 #H destruct -| #G #L #W #T #U #l #_ #p0 #H destruct -qed-. - -lemma ssta_inv_gref1: ∀h,g,G,L,U,p,l. ⦃G, L⦄ ⊢ §p •[h, g] ⦃l, U⦄ → ⊥. -/2 width=10 by ssta_inv_gref1_aux/ qed-. - -fact ssta_inv_bind1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → - ∀a,I,X,Y. T = ⓑ{a,I}Y.X → - ∃∃Z. ⦃G, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z. -#h #g #G #L #T #U #l * -G -L -T -U -l -[ #G #L #k #l #_ #a #I #X #Y #H destruct -| #G #L #K #V #W #U #i #l #_ #_ #_ #a #I #X #Y #H destruct -| #G #L #K #W #V #U #i #l #_ #_ #_ #a #I #X #Y #H destruct -| #b #J #G #L #V #T #U #l #HTU #a #I #X #Y #H destruct /2 width=3/ -| #G #L #V #T #U #l #_ #a #I #X #Y #H destruct -| #G #L #W #T #U #l #_ #a #I #X #Y #H destruct -] -qed-. - -lemma ssta_inv_bind1: ∀h,g,a,I,G,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓑ{a,I}Y.X •[h, g] ⦃l, U⦄ → - ∃∃Z. ⦃G, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z. -/2 width=3 by ssta_inv_bind1_aux/ qed-. - -fact ssta_inv_appl1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀X,Y. T = ⓐY.X → - ∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓐY.Z. -#h #g #G #L #T #U #l * -G -L -T -U -l -[ #G #L #k #l #_ #X #Y #H destruct -| #G #L #K #V #W #U #i #l #_ #_ #_ #X #Y #H destruct -| #G #L #K #W #V #U #i #l #_ #_ #_ #X #Y #H destruct -| #a #I #G #L #V #T #U #l #_ #X #Y #H destruct -| #G #L #V #T #U #l #HTU #X #Y #H destruct /2 width=3/ -| #G #L #W #T #U #l #_ #X #Y #H destruct -] -qed-. - -lemma ssta_inv_appl1: ∀h,g,G,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓐY.X •[h, g] ⦃l, U⦄ → - ∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓐY.Z. -/2 width=3 by ssta_inv_appl1_aux/ qed-. - -fact ssta_inv_cast1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → - ∀X,Y. T = ⓝY.X → ⦃G, L⦄ ⊢ X •[h, g] ⦃l, U⦄. -#h #g #G #L #T #U #l * -G -L -T -U -l -[ #G #L #k #l #_ #X #Y #H destruct -| #G #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct -| #G #L #K #W #V #U #l #i #_ #_ #_ #X #Y #H destruct -| #a #I #G #L #V #T #U #l #_ #X #Y #H destruct -| #G #L #V #T #U #l #_ #X #Y #H destruct -| #G #L #W #T #U #l #HTU #X #Y #H destruct // -] -qed-. - -lemma ssta_inv_cast1: ∀h,g,G,L,X,Y,U,l. ⦃G, L⦄ ⊢ ⓝY.X •[h, g] ⦃l, U⦄ → - ⦃G, L⦄ ⊢ X •[h, g] ⦃l, U⦄. -/2 width=4 by ssta_inv_cast1_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta_aaa.etc deleted file mode 100644 index 27c12c465..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta_aaa.etc +++ /dev/null @@ -1,40 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/aaa_lift.ma". -include "basic_2/static/ssta.ma". - -(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) - -(* Properties on atomic arity assignment for terms **************************) - -lemma ssta_aaa: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ⦃G, L⦄ ⊢ U ⁝ A. -#h #g #G #L #T #A #H elim H -G -L -T -A -[ #G #L #k #U #l #H - elim (ssta_inv_sort1 … H) -H #_ #H destruct // -| #I #G #L #K #V #B #i #HLK #HV #IHV #U #l #H - elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 [2: #l0 ] #HLK0 #HVW0 #HU [ #H ] - lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H0 destruct - lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK - @(aaa_lift … HLK … HU) -HU -L // -HV /2 width=2/ -| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H - elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/ -| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H - elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/ -| #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H - elim (ssta_inv_appl1 … H) -H #U #HTU #H destruct /3 width=3/ -| #G #L #V #T #A #_ #_ #IHV #IHT #X #l #H - lapply (ssta_inv_cast1 … H) -H /2 width=2/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta_lift.etc deleted file mode 100644 index 5398364e0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta2/ssta_lift.etc +++ /dev/null @@ -1,119 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/ldrop_ldrop.ma". -include "basic_2/static/ssta.ma". - -(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) - -(* Properties on relocation *************************************************) - -lemma ssta_lift: ∀h,g,G,L1,T1,U1,l. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ → - ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 → - ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄. -#h #g #G #L1 #T1 #U1 #l #H elim H -G -L1 -T1 -U1 -l -[ #G #L1 #k #l #Hkl #L2 #d #e #HL21 #X1 #H1 #X2 #H2 - >(lift_inv_sort1 … H1) -X1 - >(lift_inv_sort1 … H2) -X2 /2 width=1/ -| #G #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 - elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H - elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct - /3 width=8/ - | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 - lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ - ] -| #G #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (lift_inv_sort2 … H) -X /3 width=3/ -| #G #L2 #K2 #V2 #W2 #W #i #l #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H - elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ] - [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12 - elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12 - elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus minus_minus_m_m /2 width=1/ /3 width=6/ - | minus_plus minus_minus_m_m /2 width=1/ /3 width=6/ - | (deg_mono … Hkl2 … Hkl) -g -L -l2 /2 width=1/ -| #G #L #K #V #W #U1 #i #l1 #HLK #_ #HWU1 #IHVW #U2 #l2 #H - elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 [2: #l0] #HLK0 #HVW0 #HW0U2 - lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct - lapply (IHVW … HVW0) -IHVW -HVW0 * #H1 #H2 destruct - >(lift_mono … HWU1 … HW0U2) -W0 -U1 /2 width=1/ -| #G #L #K #W #V #U1 #i #l1 #HLK #_ #HWU1 #IHWV #U2 #l2 #H - elim (ssta_inv_lref1 … H) -H * #K0 #W0 #V0 [2: #l0 ] #HLK0 #HWV0 #HV0U2 - lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct - lapply (IHWV … HWV0) -IHWV -HWV0 * #H1 #H2 destruct - >(lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/ -| #a #I #G #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H - elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct - elim (IHTU1 … HTU2) -T /3 width=1/ -| #G #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H - elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct - elim (IHTU1 … HTU2) -T /3 width=1/ -| #G #L #W1 #T #U1 #l1 #_ #IHTU1 #U2 #l2 #H - lapply (ssta_inv_cast1 … H) -H #HTU2 - elim (IHTU1 … HTU2) -T /2 width=1/ -] -qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma ssta_inv_refl_pos: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, T⦄ → ⊥. -#h #g #G #L #T #l #HTT -elim (ssta_fwd_correct … HTT) (lift_mono … HX … HU12) -X // -| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12 - elim (lift_total U0 d e) /3 width=10/ -] -qed. - -(* Inversion lemmas on relocation *******************************************) - -lemma sstas_inv_lift1: ∀h,g,G,L2,T2,U2. ⦃G, L2⦄ ⊢ T2 •*[h, g] U2 → - ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 → - ∃∃U1. ⦃G, L1⦄ ⊢ T1 •*[h, g] U1 & ⇧[d, e] U1 ≡ U2. -#h #g #G #L2 #T2 #U2 #H @(sstas_ind_dx … H) -T2 /2 width=3/ -#T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12 -elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0 -elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sstas2/sstas_sstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas2/sstas_sstas.etc deleted file mode 100644 index cc98d0ea0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/sstas2/sstas_sstas.etc +++ /dev/null @@ -1,54 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/ssta_ssta.ma". -include "basic_2/unfold/sstas.ma". - -(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) - -(* Advanced inversion lemmas ************************************************) - -lemma sstas_inv_O: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g] U → - ∀T0. ⦃G, L⦄ ⊢ T •[h, g] ⦃0, T0⦄ → U = T. -#h #g #G #L #T #U #H @(sstas_ind_dx … H) -T // -#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01 -elim (ssta_mono … HTU0 … HT01)