From: Ferruccio Guidi Date: Wed, 18 Sep 2019 16:30:22 +0000 (+0200) Subject: update in static_2 and basic_2 X-Git-Tag: make_still_working~236 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ba7b8553850e4a33cf8607b07758392230d9ed40 update in static_2 and basic_2 + advances on ntas for the article + minor corrections + notation update for: ac, cnv, lsubv, nta, ntas + bold digits in predefined virtuals --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma index 9539ab942..17be9f2dd 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma @@ -17,10 +17,11 @@ include "basic_2/dynamic/cnv.ma". (* EXAMPLES *****************************************************************) -(* Extended validy (basic_2B) vs. restricted validity (basic_1A) ************) +(* Extended validy (λδ-2A) vs. restricted validity (λδ-1B) ******************) (* Note: extended validity of a closure, height of cnv_appl > 1 *) -lemma cnv_extended (h) (p): ∀G,L,s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 !*[h]. +lemma cnv_extended (h) (p) (G) (L): + ∀s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ![h,𝛚]. #h #p #G #L #s @(cnv_appl … 2 p … (⋆s) … (⋆s)) [ // @@ -32,7 +33,8 @@ lemma cnv_extended (h) (p): ∀G,L,s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ qed. (* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **) -lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h]. +lemma cnv_restricted (h) (p) (G) (L): + ∀s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h,𝟐]. #h #p #G #L #s @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2)) [ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma index 0bd1aa915..4b51fb944 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma @@ -14,40 +14,32 @@ include "static_2/syntax/ac.ma". include "basic_2/notation/relations/exclaim_5.ma". -include "basic_2/notation/relations/exclaim_4.ma". -include "basic_2/notation/relations/exclaimstar_4.ma". include "basic_2/rt_computation/cpms.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) (* activate genv *) (* Basic_2A1: uses: snv *) -inductive cnv (a) (h): relation3 genv lenv term ≝ -| cnv_sort: ∀G,L,s. cnv a h G L (⋆s) -| cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0) -| cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i) -| cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T) -| cnv_appl: ∀n,p,G,L,V,W0,T,U0. appl a n → cnv a h G L V → cnv a h G L T → - ⦃G,L⦄ ⊢ V ➡*[1,h] W0 → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0 → cnv a h G L (ⓐV.T) -| cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T → - ⦃G,L⦄ ⊢ U ➡*[h] U0 → ⦃G,L⦄ ⊢ T ➡*[1,h] U0 → cnv a h G L (ⓝU.T) +inductive cnv (h) (a): relation3 genv lenv term ≝ +| cnv_sort: ∀G,L,s. cnv h a G L (⋆s) +| cnv_zero: ∀I,G,K,V. cnv h a G K V → cnv h a G (K.ⓑ{I}V) (#0) +| cnv_lref: ∀I,G,K,i. cnv h a G K (#i) → cnv h a G (K.ⓘ{I}) (#↑i) +| cnv_bind: ∀p,I,G,L,V,T. cnv h a G L V → cnv h a G (L.ⓑ{I}V) T → cnv h a G L (ⓑ{p,I}V.T) +| cnv_appl: ∀n,p,G,L,V,W0,T,U0. ad a n → cnv h a G L V → cnv h a G L T → + ⦃G,L⦄ ⊢ V ➡*[1,h] W0 → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0 → cnv h a G L (ⓐV.T) +| cnv_cast: ∀G,L,U,T,U0. cnv h a G L U → cnv h a G L T → + ⦃G,L⦄ ⊢ U ➡*[h] U0 → ⦃G,L⦄ ⊢ T ➡*[1,h] U0 → cnv h a G L (ⓝU.T) . interpretation "context-sensitive native validity (term)" - 'Exclaim a h G L T = (cnv a h G L T). - -interpretation "context-sensitive restricted native validity (term)" - 'Exclaim h G L T = (cnv (ac_eq (S O)) h G L T). - -interpretation "context-sensitive extended native validity (term)" - 'ExclaimStar h G L T = (cnv ac_top h G L T). + 'Exclaim h a G L T = (cnv h a G L T). (* Basic inversion lemmas ***************************************************) -fact cnv_inv_zero_aux (a) (h): - ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → X = #0 → - ∃∃I,K,V. ⦃G,K⦄ ⊢ V ![a,h] & L = K.ⓑ{I}V. -#a #h #G #L #X * -G -L -X +fact cnv_inv_zero_aux (h) (a): + ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → X = #0 → + ∃∃I,K,V. ⦃G,K⦄ ⊢ V ![h,a] & L = K.ⓑ{I}V. +#h #a #G #L #X * -G -L -X [ #G #L #s #H destruct | #I #G #K #V #HV #_ /2 width=5 by ex2_3_intro/ | #I #G #K #i #_ #H destruct @@ -57,15 +49,15 @@ fact cnv_inv_zero_aux (a) (h): ] qed-. -lemma cnv_inv_zero (a) (h): - ∀G,L. ⦃G,L⦄ ⊢ #0 ![a,h] → - ∃∃I,K,V. ⦃G,K⦄ ⊢ V ![a,h] & L = K.ⓑ{I}V. +lemma cnv_inv_zero (h) (a): + ∀G,L. ⦃G,L⦄ ⊢ #0 ![h,a] → + ∃∃I,K,V. ⦃G,K⦄ ⊢ V ![h,a] & L = K.ⓑ{I}V. /2 width=3 by cnv_inv_zero_aux/ qed-. -fact cnv_inv_lref_aux (a) (h): - ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀i. X = #(↑i) → - ∃∃I,K. ⦃G,K⦄ ⊢ #i ![a,h] & L = K.ⓘ{I}. -#a #h #G #L #X * -G -L -X +fact cnv_inv_lref_aux (h) (a): + ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀i. X = #(↑i) → + ∃∃I,K. ⦃G,K⦄ ⊢ #i ![h,a] & L = K.ⓘ{I}. +#h #a #G #L #X * -G -L -X [ #G #L #s #j #H destruct | #I #G #K #V #_ #j #H destruct | #I #G #L #i #Hi #j #H destruct /2 width=4 by ex2_2_intro/ @@ -75,13 +67,13 @@ fact cnv_inv_lref_aux (a) (h): ] qed-. -lemma cnv_inv_lref (a) (h): - ∀G,L,i. ⦃G,L⦄ ⊢ #↑i ![a,h] → - ∃∃I,K. ⦃G,K⦄ ⊢ #i ![a,h] & L = K.ⓘ{I}. +lemma cnv_inv_lref (h) (a): + ∀G,L,i. ⦃G,L⦄ ⊢ #↑i ![h,a] → + ∃∃I,K. ⦃G,K⦄ ⊢ #i ![h,a] & L = K.ⓘ{I}. /2 width=3 by cnv_inv_lref_aux/ qed-. -fact cnv_inv_gref_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀l. X = §l → ⊥. -#a #h #G #L #X * -G -L -X +fact cnv_inv_gref_aux (h) (a): ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀l. X = §l → ⊥. +#h #a #G #L #X * -G -L -X [ #G #L #s #l #H destruct | #I #G #K #V #_ #l #H destruct | #I #G #K #i #_ #l #H destruct @@ -92,14 +84,14 @@ fact cnv_inv_gref_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀l. X = § qed-. (* Basic_2A1: uses: snv_inv_gref *) -lemma cnv_inv_gref (a) (h): ∀G,L,l. ⦃G,L⦄ ⊢ §l ![a,h] → ⊥. +lemma cnv_inv_gref (h) (a): ∀G,L,l. ⦃G,L⦄ ⊢ §l ![h,a] → ⊥. /2 width=8 by cnv_inv_gref_aux/ qed-. -fact cnv_inv_bind_aux (a) (h): - ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → +fact cnv_inv_bind_aux (h) (a): + ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀p,I,V,T. X = ⓑ{p,I}V.T → - ∧∧ ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L.ⓑ{I}V⦄ ⊢ T ![a,h]. -#a #h #G #L #X * -G -L -X + ∧∧ ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T ![h,a]. +#h #a #G #L #X * -G -L -X [ #G #L #s #q #Z #X1 #X2 #H destruct | #I #G #K #V #_ #q #Z #X1 #X2 #H destruct | #I #G #K #i #_ #q #Z #X1 #X2 #H destruct @@ -110,16 +102,16 @@ fact cnv_inv_bind_aux (a) (h): qed-. (* Basic_2A1: uses: snv_inv_bind *) -lemma cnv_inv_bind (a) (h): - ∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![a,h] → - ∧∧ ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L.ⓑ{I}V⦄ ⊢ T ![a,h]. +lemma cnv_inv_bind (h) (a): + ∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![h,a] → + ∧∧ ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T ![h,a]. /2 width=4 by cnv_inv_bind_aux/ qed-. -fact cnv_inv_appl_aux (a) (h): - ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀V,T. X = ⓐV.T → - ∃∃n,p,W0,U0. appl a n & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & +fact cnv_inv_appl_aux (h) (a): + ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀V,T. X = ⓐV.T → + ∃∃n,p,W0,U0. ad a n & ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] & ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0. -#a #h #G #L #X * -L -X +#h #a #G #L #X * -L -X [ #G #L #s #X1 #X2 #H destruct | #I #G #K #V #_ #X1 #X2 #H destruct | #I #G #K #i #_ #X1 #X2 #H destruct @@ -130,17 +122,17 @@ fact cnv_inv_appl_aux (a) (h): qed-. (* Basic_2A1: uses: snv_inv_appl *) -lemma cnv_inv_appl (a) (h): - ∀G,L,V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → - ∃∃n,p,W0,U0. appl a n & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & +lemma cnv_inv_appl (h) (a): + ∀G,L,V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h,a] → + ∃∃n,p,W0,U0. ad a n & ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] & ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0. /2 width=3 by cnv_inv_appl_aux/ qed-. -fact cnv_inv_cast_aux (a) (h): - ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀U,T. X = ⓝU.T → - ∃∃U0. ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & +fact cnv_inv_cast_aux (h) (a): + ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀U,T. X = ⓝU.T → + ∃∃U0. ⦃G,L⦄ ⊢ U ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] & ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[1,h] U0. -#a #h #G #L #X * -G -L -X +#h #a #G #L #X * -G -L -X [ #G #L #s #X1 #X2 #H destruct | #I #G #K #V #_ #X1 #X2 #H destruct | #I #G #K #i #_ #X1 #X2 #H destruct @@ -151,26 +143,26 @@ fact cnv_inv_cast_aux (a) (h): qed-. (* Basic_2A1: uses: snv_inv_cast *) -lemma cnv_inv_cast (a) (h): - ∀G,L,U,T. ⦃G,L⦄ ⊢ ⓝU.T ![a,h] → - ∃∃U0. ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & +lemma cnv_inv_cast (h) (a): + ∀G,L,U,T. ⦃G,L⦄ ⊢ ⓝU.T ![h,a] → + ∃∃U0. ⦃G,L⦄ ⊢ U ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] & ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[1,h] U0. /2 width=3 by cnv_inv_cast_aux/ qed-. (* Basic forward lemmas *****************************************************) -lemma cnv_fwd_flat (a) (h) (I) (G) (L): - ∀V,T. ⦃G,L⦄ ⊢ ⓕ{I}V.T ![a,h] → - ∧∧ ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h]. -#a #h * #G #L #V #T #H +lemma cnv_fwd_flat (h) (a) (I) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ⓕ{I}V.T ![h,a] → + ∧∧ ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L⦄ ⊢ T ![h,a]. +#h #a * #G #L #V #T #H [ elim (cnv_inv_appl … H) #n #p #W #U #_ #HV #HT #_ #_ | elim (cnv_inv_cast … H) #U #HV #HT #_ #_ ] -H /2 width=1 by conj/ qed-. -lemma cnv_fwd_pair_sn (a) (h) (I) (G) (L): - ∀V,T. ⦃G,L⦄ ⊢ ②{I}V.T ![a,h] → ⦃G,L⦄ ⊢ V ![a,h]. -#a #h * [ #p ] #I #G #L #V #T #H +lemma cnv_fwd_pair_sn (h) (a) (I) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ②{I}V.T ![h,a] → ⦃G,L⦄ ⊢ V ![h,a]. +#h #a * [ #p ] #I #G #L #V #T #H [ elim (cnv_inv_bind … H) -H #HV #_ | elim (cnv_fwd_flat … H) -H #HV #_ ] // diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma index 5667b7870..e96946f06 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma @@ -20,8 +20,8 @@ include "basic_2/dynamic/cnv.ma". (* Forward lemmas on atomic arity assignment for terms **********************) (* Basic_2A1: uses: snv_fwd_aaa *) -lemma cnv_fwd_aaa (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ∃A. ⦃G,L⦄ ⊢ T ⁝ A. -#a #h #G #L #T #H elim H -G -L -T +lemma cnv_fwd_aaa (h) (a): ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a] → ∃A. ⦃G,L⦄ ⊢ T ⁝ A. +#h #a #G #L #T #H elim H -G -L -T [ /2 width=2 by aaa_sort, ex_intro/ | #I #G #L #V #_ * /3 width=2 by aaa_zero, ex_intro/ | #I #G #L #K #_ * /3 width=2 by aaa_lref, ex_intro/ @@ -43,39 +43,39 @@ qed-. (* Forward lemmas with t_bound rt_transition for terms **********************) -lemma cnv_fwd_cpm_SO (a) (h) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U. -#a #h #G #L #T #H +lemma cnv_fwd_cpm_SO (h) (a) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U. +#h #a #G #L #T #H elim (cnv_fwd_aaa … H) -H #A #HA /2 width=2 by aaa_cpm_SO/ qed-. (* Forward lemmas with t_bound rt_computation for terms *********************) -lemma cnv_fwd_cpms_total (a) (h) (n) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U. -#a #h #n #G #L #T #H +lemma cnv_fwd_cpms_total (h) (a) (n) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U. +#h #a #n #G #L #T #H elim (cnv_fwd_aaa … H) -H #A #HA /2 width=2 by cpms_total_aaa/ qed-. -lemma cnv_fwd_cpms_abst_dx_le (a) (h) (G) (L) (W) (p): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → +lemma cnv_fwd_cpms_abst_dx_le (h) (a) (G) (L) (W) (p): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀n1,U1. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U1 → ∀n2. n1 ≤ n2 → ∃∃U2. ⦃G,L⦄ ⊢ T ➡*[n2,h] ⓛ{p}W.U2 & ⦃G,L.ⓛW⦄ ⊢ U1 ➡*[n2-n1,h] U2. -#a #h #G #L #W #p #T #H +#h #a #G #L #W #p #T #H elim (cnv_fwd_aaa … H) -H #A #HA /2 width=2 by cpms_abst_dx_le_aaa/ qed-. (* Advanced properties ******************************************************) -lemma cnv_appl_ge (a) (h) (n1) (p) (G) (L): - ∀n2. n1 ≤ n2 → appl a n2 → - ∀V. ⦃G,L⦄ ⊢ V ![a,h] → ∀T. ⦃G,L⦄ ⊢ T ![a,h] → +lemma cnv_appl_ge (h) (a) (n1) (p) (G) (L): + ∀n2. n1 ≤ n2 → ad a n2 → + ∀V. ⦃G,L⦄ ⊢ V ![h,a] → ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀X. ⦃G,L⦄ ⊢ V ➡*[1,h] X → ∀W. ⦃G,L⦄ ⊢ W ➡*[h] X → - ∀U. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![a,h]. -#a #h #n1 #p #G #L #n2 #Hn12 #Ha #V #HV #T #HT #X #HVX #W #HW #X #HTX + ∀U. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![h,a]. +#h #a #n1 #p #G #L #n2 #Hn12 #Ha #V #HV #T #HT #X #HVX #W #HW #X #HTX elim (cnv_fwd_cpms_abst_dx_le … HT … HTX … Hn12) #U #HTU #_ -n1 /4 width=11 by cnv_appl, cpms_bind, cpms_cprs_trans/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma index 792c48f05..a4b4078d8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma @@ -20,9 +20,9 @@ include "basic_2/dynamic/cnv_cpmuwe.ma". (* Properties with context-sensitive parallel eta-conversion for terms ******) -lemma cpce_total_cnv (a) (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2. -#a #h #G #L #T1 #HT1 +lemma cpce_total_cnv (h) (a) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2. +#h #a #G #L #T1 #HT1 lapply (cnv_fwd_csx … HT1) #H generalize in match HT1; -HT1 @(csx_ind_fpbg … H) -G -L -T1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma index ba65bce5b..5ed59b739 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma @@ -20,10 +20,10 @@ include "basic_2/dynamic/cnv_aaa.ma". (* Properties with r-equivalence ********************************************) -lemma cnv_cpcs_dec (a) (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∀T2. ⦃G,L⦄ ⊢ T2 ![a,h] → +lemma cnv_cpcs_dec (h) (a) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T2 ![h,a] → Decidable … (⦃G,L⦄ ⊢ T1 ⬌*[h] T2). -#a #h #G #L #T1 #HT1 #T2 #HT2 +#h #a #G #L #T1 #HT1 #T2 #HT2 elim (cnv_fwd_aaa … HT1) -HT1 #A1 #HA1 elim (cnv_fwd_aaa … HT2) -HT2 #A2 #HA2 /3 width=2 by csx_cpcs_dec, aaa_csx/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma index 125c9649f..fbf407f50 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma @@ -20,57 +20,57 @@ include "basic_2/dynamic/cnv.ma". (* Properties with t-bound rt-equivalence for terms *************************) -lemma cnv_appl_cpes (a) (h) (G) (L): - ∀n. appl a n → - ∀V. ⦃G,L⦄ ⊢ V ![a,h] → ∀T. ⦃G,L⦄ ⊢ T ![a,h] → +lemma cnv_appl_cpes (h) (a) (G) (L): + ∀n. ad a n → + ∀V. ⦃G,L⦄ ⊢ V ![h,a] → ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀W. ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W → - ∀p,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![a,h]. -#a #h #G #L #n #Hn #V #HV #T #HT #W * + ∀p,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![h,a]. +#h #a #G #L #n #Hn #V #HV #T #HT #W * /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/ qed. -lemma cnv_cast_cpes (a) (h) (G) (L): - ∀U. ⦃G,L⦄ ⊢ U ![a,h] → - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T → ⦃G,L⦄ ⊢ ⓝU.T ![a,h]. -#a #h #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/ +lemma cnv_cast_cpes (h) (a) (G) (L): + ∀U. ⦃G,L⦄ ⊢ U ![h,a] → + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T → ⦃G,L⦄ ⊢ ⓝU.T ![h,a]. +#h #a #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/ qed. (* Inversion lemmas with t-bound rt-equivalence for terms *******************) -lemma cnv_inv_appl_cpes (a) (h) (G) (L): - ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → - ∃∃n,p,W,U. appl a n & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & +lemma cnv_inv_appl_cpes (h) (a) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h,a] → + ∃∃n,p,W,U. ad a n & ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] & ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U. -#a #h #G #L #V #T #H +#h #a #G #L #V #T #H elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU /3 width=7 by cpms_div, ex5_4_intro/ qed-. -lemma cnv_inv_cast_cpes (a) (h) (G) (L): - ∀U,T. ⦃G,L⦄ ⊢ ⓝU.T ![a,h] → - ∧∧ ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T. -#a #h #G #L #U #T #H +lemma cnv_inv_cast_cpes (h) (a) (G) (L): + ∀U,T. ⦃G,L⦄ ⊢ ⓝU.T ![h,a] → + ∧∧ ⦃G,L⦄ ⊢ U ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] & ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T. +#h #a #G #L #U #T #H elim (cnv_inv_cast … H) -H /3 width=3 by cpms_div, and3_intro/ qed-. (* Eliminators with t-bound rt-equivalence for terms ************************) -lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term): +lemma cnv_ind_cpes (h) (a) (Q:relation3 genv lenv term): (∀G,L,s. Q G L (⋆s)) → - (∀I,G,K,V. ⦃G,K⦄ ⊢ V![a,h] → Q G K V → Q G (K.ⓑ{I}V) (#O)) → - (∀I,G,K,i. ⦃G,K⦄ ⊢ #i![a,h] → Q G K (#i) → Q G (K.ⓘ{I}) (#(↑i))) → - (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] → + (∀I,G,K,V. ⦃G,K⦄ ⊢ V![h,a] → Q G K V → Q G (K.ⓑ{I}V) (#O)) → + (∀I,G,K,i. ⦃G,K⦄ ⊢ #i![h,a] → Q G K (#i) → Q G (K.ⓘ{I}) (#(↑i))) → + (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![h,a] → ⦃G,L.ⓑ{I}V⦄⊢T![h,a] → Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T) ) → - (∀n,p,G,L,V,W,T,U. appl a n → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] → + (∀n,p,G,L,V,W,T,U. ad a n → ⦃G,L⦄ ⊢ V![h,a] → ⦃G,L⦄ ⊢ T![h,a] → ⦃G,L⦄ ⊢ V ⬌*[h,1,0]W → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → Q G L V → Q G L T → Q G L (ⓐV.T) ) → - (∀G,L,U,T. ⦃G,L⦄⊢ U![a,h] → ⦃G,L⦄ ⊢ T![a,h] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T → + (∀G,L,U,T. ⦃G,L⦄⊢ U![h,a] → ⦃G,L⦄ ⊢ T![h,a] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T → Q G L U → Q G L T → Q G L (ⓝU.T) ) → - ∀G,L,T. ⦃G,L⦄⊢ T![a,h] → Q G L T. -#a #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H + ∀G,L,T. ⦃G,L⦄⊢ T![h,a] → Q G L T. +#h #a #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H elim H -G -L -T [5,6: /3 width=7 by cpms_div/ |*: /2 width=1 by/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma index 56e5ffd9b..60f0a5e79 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma @@ -31,15 +31,15 @@ fact cnv_cpm_conf_lpr_atom_ess_aux (h) (G) (L1) (L2) (s): ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡*[1,h] T & ⦃G,L2⦄ ⊢ ⋆(⫯[h]s) ➡*[h] T. /3 width=3 by cpm_cpms, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (G) (L) (i): - (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄⊢#i![a,h] → +fact cnv_cpm_conf_lpr_atom_delta_aux (h) (a) (G) (L) (i): + (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄⊢#i![h,a] → ∀K,V. ⬇*[i]L ≘ K.ⓓV → ∀n,XV. ⦃G,K⦄ ⊢ V ➡[n,h] XV → ∀X. ⬆*[↑i]XV ≘ X → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T. -#a #h #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2 +#h #a #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2 lapply (cnv_inv_lref_pair … HT … HLK) -HT #HV elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #HV1 #H destruct @@ -53,15 +53,15 @@ elim (cpms_lifts_sn … HVX … HLK2 … HXV) -XV -HLK2 #XV #HVX #HXV /3 width=6 by cpms_delta_drops, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_atom_ell_aux (a) (h) (G) (L) (i): - (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄⊢#i![a,h] → +fact cnv_cpm_conf_lpr_atom_ell_aux (h) (a) (G) (L) (i): + (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄⊢#i![h,a] → ∀K,W. ⬇*[i]L ≘ K.ⓛW → ∀n,XW. ⦃G,K⦄ ⊢ W ➡[n,h] XW → ∀X. ⬆*[↑i]XW ≘ X → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T. -#a #h #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2 +#h #a #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2 lapply (cnv_inv_lref_pair … HT … HLK) -HT #HW elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1 elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK1 #HW1 #H destruct @@ -75,15 +75,15 @@ elim (cpms_lifts_sn … HWX … HLK2 … HXW) -XW -HLK2 #XW #HWX #HXW /3 width=6 by cpms_ell_drops, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_delta_delta_aux (a) (h) (I) (G) (L) (i): - (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄⊢#i![a,h] → +fact cnv_cpm_conf_lpr_delta_delta_aux (h) (a) (I) (G) (L) (i): + (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄⊢#i![h,a] → ∀K1,V1. ⬇*[i]L ≘ K1.ⓑ{I}V1 → ∀K2,V2. ⬇*[i]L ≘ K2.ⓑ{I}V2 → ∀n1,XV1. ⦃G,K1⦄ ⊢ V1 ➡[n1,h] XV1 → ∀n2,XV2. ⦃G,K2⦄ ⊢ V2 ➡[n2,h] XV2 → ∀X1. ⬆*[↑i]XV1 ≘ X1 → ∀X2. ⬆*[↑i]XV2 ≘ X2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ X1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ X2 ➡*[n1-n2,h] T. -#a #h #I #G #L #i #IH #HT +#h #a #I #G #L #i #IH #HT #K #V #HLK #Y #X #HLY #n1 #XV1 #HVX1 #n2 #XV2 #HVX2 #X1 #HXV1 #X2 #HXV2 #L1 #HL1 #L2 #HL2 lapply (drops_mono … HLY … HLK) -HLY #H destruct @@ -107,14 +107,14 @@ fact cnv_cpm_conf_lpr_delta_ell_aux (L) (K1) (K2) (V) (W) (i): lapply (drops_mono … HLK2 … HLK1) -L -i #H destruct qed-. -fact cnv_cpm_conf_lpr_bind_bind_aux (a) (h) (p) (I) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓑ{p,I}V.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![a,h] → +fact cnv_cpm_conf_lpr_bind_bind_aux (h) (a) (p) (I) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓑ{p,I}V.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![h,a] → ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀n1,T1. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n2,h] T2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡*[n1-n2,h] T. -#a #h #p #I #G0 #L0 #V0 #T0 #IH #H0 +#h #a #p #I #G0 #L0 #V0 #T0 #IH #H0 #V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #HV0 #HT0 @@ -124,14 +124,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I} /3 width=5 by cpms_bind_dx, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_bind_zeta_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] → +fact cnv_cpm_conf_lpr_bind_zeta_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ +ⓓV.T ![h,a] → ∀V1. ⦃G,L⦄ ⊢V ➡[h] V1 → ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → ∀T2. ⬆*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ +ⓓV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #V1 #HV01 #n1 #T1 #HT01 #T2 #HT20 #n2 #XT2 #HXT2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #_ #HT0 @@ -144,14 +144,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HXT12 … HXT2 … HL01 … HL02) /3 width=3 by cpms_zeta, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_zeta_zeta_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] → +fact cnv_cpm_conf_lpr_zeta_zeta_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ +ⓓV.T ![h,a] → ∀T1. ⬆*[1]T1 ≘ T → ∀T2. ⬆*[1]T2 ≘ T → ∀n1,XT1. ⦃G,L⦄ ⊢ T1 ➡[n1,h] XT1 → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ XT1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #T1 #HT10 #T2 #HT20 #n1 #XT1 #HXT1 #n2 #XT2 #HXT2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #_ #HT0 @@ -163,14 +163,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HXT1 … HXT2 … HL01 … HL02) /2 width=3 by ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_appl_appl_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → +fact cnv_cpm_conf_lpr_appl_appl_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓐV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓐV.T ![h,a] → ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓐV2.T2 ➡*[n1-n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02 @@ -180,15 +180,15 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w /3 width=5 by cpms_appl_dx, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_appl_beta_aux (a) (h) (p) (G) (L) (V) (W) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] → +fact cnv_cpm_conf_lpr_appl_beta_aux (h) (a) (p) (G) (L) (V) (W) (T): + (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![h,a] → ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 → ∀n1,T1. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡*[n1-n2,h] T. -#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0 #V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02 @@ -202,16 +202,16 @@ lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 [ /2 width=1 by lsubr_ /4 width=5 by cpms_beta_dx, cpms_bind_dx, cpm_cast, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_appl_theta_aux (a) (h) (p) (G) (L) (V) (W) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] → +fact cnv_cpm_conf_lpr_appl_theta_aux (h) (a) (p) (G) (L) (V) (W) (T): + (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![h,a] → ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 → ∀n1,T1. ⦃G,L⦄ ⊢ ⓓ{p}W.T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 → ∀U2. ⬆*[1]V2 ≘ U2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T. -#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0 #V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02 #U2 #HVU2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02 @@ -233,15 +233,15 @@ elim (cpm_inv_abbr1 … HX) -HX * ] qed-. -fact cnv_cpm_conf_lpr_beta_beta_aux (a) (h) (p) (G) (L) (V) (W) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] → +fact cnv_cpm_conf_lpr_beta_beta_aux (h) (a) (p) (G) (L) (V) (W) (T): + (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![h,a] → ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W1. ⦃G,L⦄ ⊢ W ➡[h] W1 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 → ∀n1,T1. ⦃G,L.ⓛW⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓓ{p}ⓝW1.V1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡*[n1-n2,h] T. -#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0 #V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02 @@ -255,16 +255,16 @@ lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_be /4 width=5 by cpms_bind_dx, cpm_eps, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_theta_theta_aux (a) (h) (p) (G) (L) (V) (W) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] → +fact cnv_cpm_conf_lpr_theta_theta_aux (h) (a) (p) (G) (L) (V) (W) (T): + (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![h,a] → ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W1. ⦃G,L⦄ ⊢ W ➡[h] W1 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 → ∀n1,T1. ⦃G,L.ⓓW⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 → ∀U1. ⬆*[1]V1 ≘ U1 → ∀U2. ⬆*[1]V2 ≘ U2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓓ{p}W1.ⓐU1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T. -#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0 #V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02 #U1 #HVU1 #U2 #HVU2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02 @@ -278,14 +278,14 @@ lapply (cpm_lifts_bi … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2 … HVU) -V2 -V [ /3 /4 width=7 by cpms_appl_dx, cpms_bind_dx, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_cast_cast_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → +fact cnv_cpm_conf_lpr_cast_cast_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![h,a] → ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 → ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓝV2.T2 ➡*[n1-n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0 @@ -295,14 +295,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w /3 width=5 by cpms_cast, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_cast_epsilon_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → +fact cnv_cpm_conf_lpr_cast_epsilon_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![h,a] → ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0 @@ -311,15 +311,15 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w /3 width=3 by cpms_eps, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_cast_ee_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → +fact cnv_cpm_conf_lpr_cast_ee_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) → + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![h,a] → ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 → ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-↑n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH2 #IH1 #H0 +#h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0 #n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01 #L1 #HL01 #L2 #HL02 -HV01 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0 @@ -334,13 +334,13 @@ lapply (cpms_trans … HT1 … HTU) -T [h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → +fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![h,a] → ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_cast … H0) -H0 #X0 #_ #HT0 #_ #_ -X0 @@ -349,14 +349,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w /2 width=3 by ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_epsilon_ee_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → +fact cnv_cpm_conf_lpr_epsilon_ee_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) → + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![h,a] → ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-↑n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH2 #IH1 #H0 +#h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0 #n1 #T1 #HT01 #n2 #V2 #HV02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0 @@ -371,13 +371,13 @@ lapply (cpms_trans … HT1 … HTU) -T [h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ ⓝV.T ![a,h] → +fact cnv_cpm_conf_lpr_ee_ee_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ⦃G,L⦄ ⊢ ⓝV.T ![h,a] → ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ V1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-n2,h] T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #n1 #V1 #HV01 #n2 #V2 #HV02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #_ #_ #_ -X0 @@ -386,12 +386,12 @@ elim (cnv_cpm_conf_lpr_sub … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 w /2 width=3 by ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_aux (a) (h): +fact cnv_cpm_conf_lpr_aux (h) (a): ∀G0,L0,T0. - (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → - (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr a h G1 L1 T1. -#a #h #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]] + (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) → + (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr h a G1 L1 T1. +#h #a #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]] [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct elim (cpm_inv_atom1_drops … HX1) -HX1 * elim (cpm_inv_atom1_drops … HX2) -HX2 * diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma index 8fac0d847..4ea9ff53f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma @@ -22,9 +22,9 @@ include "basic_2/dynamic/cnv_fsb.ma". (* Inversion lemmas with restricted rt-transition for terms *****************) -lemma cnv_cpr_tdeq_fwd_refl (a) (h) (G) (L): - ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[h] T2 → T1 ≛ T2 → ⦃G,L⦄ ⊢ T1 ![a,h] → T1 = T2. -#a #h #G #L #T1 #T2 #H @(cpr_ind … H) -G -L -T1 -T2 +lemma cnv_cpr_tdeq_fwd_refl (h) (a) (G) (L): + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[h] T2 → T1 ≛ T2 → ⦃G,L⦄ ⊢ T1 ![h,a] → T1 = T2. +#h #a #G #L #T1 #T2 #H @(cpr_ind … H) -G -L -T1 -T2 [ // | #G #K #V1 #V2 #X2 #_ #_ #_ #H1 #_ -a -G -K -V1 -V2 lapply (tdeq_inv_lref1 … H1) -H1 #H destruct // @@ -53,11 +53,11 @@ lemma cnv_cpr_tdeq_fwd_refl (a) (h) (G) (L): ] qed-. -lemma cpm_tdeq_inv_bind_sn (a) (h) (n) (p) (I) (G) (L): - ∀V,T1. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] → +lemma cpm_tdeq_inv_bind_sn (h) (a) (n) (p) (I) (G) (L): + ∀V,T1. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ![h,a] → ∀X. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ➡[n,h] X → ⓑ{p,I}V.T1 ≛ X → - ∃∃T2. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓑ{p,I}V.T2. -#a #h #n #p #I #G #L #V #T1 #H0 #X #H1 #H2 + ∃∃T2. ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓑ{p,I}V.T2. +#h #a #n #p #I #G #L #V #T1 #H0 #X #H1 #H2 elim (cpm_inv_bind1 … H1) -H1 * [ #XV #T2 #HXV #HT12 #H destruct elim (tdeq_inv_pair … H2) -H2 #_ #H2XV #H2T12 @@ -71,12 +71,12 @@ elim (cpm_inv_bind1 … H1) -H1 * ] qed-. -lemma cpm_tdeq_inv_appl_sn (a) (h) (n) (G) (L): - ∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![a,h] → +lemma cpm_tdeq_inv_appl_sn (h) (a) (n) (G) (L): + ∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![h,a] → ∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛ X → - ∃∃m,q,W,U1,T2. appl a m & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ V ➡*[1,h] W & ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1 - & ⦃G,L⦄⊢ T1 ![a,h] & ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓐV.T2. -#a #h #n #G #L #V #T1 #H0 #X #H1 #H2 + ∃∃m,q,W,U1,T2. ad a m & ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L⦄ ⊢ V ➡*[1,h] W & ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1 + & ⦃G,L⦄⊢ T1 ![h,a] & ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓐV.T2. +#h #a #n #G #L #V #T1 #H0 #X #H1 #H2 elim (cpm_inv_appl1 … H1) -H1 * [ #XV #T2 #HXV #HT12 #H destruct elim (tdeq_inv_pair … H2) -H2 #_ #H2XV #H2T12 @@ -90,13 +90,13 @@ elim (cpm_inv_appl1 … H1) -H1 * ] qed-. -lemma cpm_tdeq_inv_cast_sn (a) (h) (n) (G) (L): - ∀U1,T1. ⦃G,L⦄ ⊢ ⓝU1.T1 ![a,h] → +lemma cpm_tdeq_inv_cast_sn (h) (a) (n) (G) (L): + ∀U1,T1. ⦃G,L⦄ ⊢ ⓝU1.T1 ![h,a] → ∀X. ⦃G,L⦄ ⊢ ⓝU1.T1 ➡[n,h] X → ⓝU1.T1 ≛ X → ∃∃U0,U2,T2. ⦃G,L⦄ ⊢ U1 ➡*[h] U0 & ⦃G,L⦄ ⊢ T1 ➡*[1,h] U0 - & ⦃G,L⦄ ⊢ U1 ![a,h] & ⦃G,L⦄ ⊢ U1 ➡[n,h] U2 & U1 ≛ U2 - & ⦃G,L⦄ ⊢ T1 ![a,h] & ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓝU2.T2. -#a #h #n #G #L #U1 #T1 #H0 #X #H1 #H2 + & ⦃G,L⦄ ⊢ U1 ![h,a] & ⦃G,L⦄ ⊢ U1 ➡[n,h] U2 & U1 ≛ U2 + & ⦃G,L⦄ ⊢ T1 ![h,a] & ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓝU2.T2. +#h #a #n #G #L #U1 #T1 #H0 #X #H1 #H2 elim (cpm_inv_cast1 … H1) -H1 [ * || * ] [ #U2 #T2 #HU12 #HT12 #H destruct elim (tdeq_inv_pair … H2) -H2 #_ #H2U12 #H2T12 @@ -113,11 +113,11 @@ elim (cpm_inv_cast1 … H1) -H1 [ * || * ] ] qed-. -lemma cpm_tdeq_inv_bind_dx (a) (h) (n) (p) (I) (G) (L): - ∀X. ⦃G,L⦄ ⊢ X ![a,h] → +lemma cpm_tdeq_inv_bind_dx (h) (a) (n) (p) (I) (G) (L): + ∀X. ⦃G,L⦄ ⊢ X ![h,a] → ∀V,T2. ⦃G,L⦄ ⊢ X ➡[n,h] ⓑ{p,I}V.T2 → X ≛ ⓑ{p,I}V.T2 → - ∃∃T1. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓑ{p,I}V.T1. -#a #h #n #p #I #G #L #X #H0 #V #T2 #H1 #H2 + ∃∃T1. ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓑ{p,I}V.T1. +#h #a #n #p #I #G #L #X #H0 #V #T2 #H1 #H2 elim (tdeq_inv_pair2 … H2) #V0 #T1 #_ #_ #H destruct elim (cpm_tdeq_inv_bind_sn … H0 … H1 H2) -H0 -H1 -H2 #T0 #HV #HT1 #H1T12 #H2T12 #H destruct /2 width=5 by ex5_intro/ @@ -125,27 +125,27 @@ qed-. (* Eliminators with restricted rt-transition for terms **********************) -lemma cpm_tdeq_ind (a) (h) (n) (G) (Q:relation3 …): +lemma cpm_tdeq_ind (h) (a) (n) (G) (Q:relation3 …): (∀I,L. n = 0 → Q L (⓪{I}) (⓪{I})) → (∀L,s. n = 1 → Q L (⋆s) (⋆(⫯[h]s))) → - (∀p,I,L,V,T1. ⦃G,L⦄⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T1![a,h] → + (∀p,I,L,V,T1. ⦃G,L⦄⊢ V![h,a] → ⦃G,L.ⓑ{I}V⦄⊢T1![h,a] → ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2) ) → - (∀m. appl a m → - ∀L,V. ⦃G,L⦄ ⊢ V ![a,h] → ∀W. ⦃G,L⦄ ⊢ V ➡*[1,h] W → - ∀p,T1,U1. ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![a,h] → + (∀m. ad a m → + ∀L,V. ⦃G,L⦄ ⊢ V ![h,a] → ∀W. ⦃G,L⦄ ⊢ V ➡*[1,h] W → + ∀p,T1,U1. ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → Q L T1 T2 → Q L (ⓐV.T1) (ⓐV.T2) ) → (∀L,U0,U1,T1. ⦃G,L⦄ ⊢ U1 ➡*[h] U0 → ⦃G,L⦄ ⊢ T1 ➡*[1,h] U0 → - ∀U2. ⦃G,L⦄ ⊢ U1 ![a,h] → ⦃G,L⦄ ⊢ U1 ➡[n,h] U2 → U1 ≛ U2 → - ∀T2. ⦃G,L⦄ ⊢ T1 ![a,h] → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → + ∀U2. ⦃G,L⦄ ⊢ U1 ![h,a] → ⦃G,L⦄ ⊢ U1 ➡[n,h] U2 → U1 ≛ U2 → + ∀T2. ⦃G,L⦄ ⊢ T1 ![h,a] → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → Q L U1 U2 → Q L T1 T2 → Q L (ⓝU1.T1) (ⓝU2.T2) ) → - ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀L,T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → Q L T1 T2. -#a #h #n #G #Q #IH1 #IH2 #IH3 #IH4 #IH5 #L #T1 +#h #a #n #G #Q #IH1 #IH2 #IH3 #IH4 #IH5 #L #T1 @(insert_eq_0 … G) #F @(fqup_wf_ind_eq (Ⓣ) … F L T1) -L -T1 -F #G0 #L0 #T0 #IH #F #L * [| * [| * ]] @@ -168,11 +168,11 @@ qed-. (* Advanced properties with restricted rt-transition for terms **************) -lemma cpm_tdeq_free (a) (h) (n) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → +lemma cpm_tdeq_free (h) (a) (n) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → ∀F,K. ⦃F,K⦄ ⊢ T1 ➡[n,h] T2. -#a #h #n #G #L #T1 #H0 #T2 #H1 #H2 +#h #a #n #G #L #T1 #H0 #T2 #H1 #H2 @(cpm_tdeq_ind … H0 … H1 H2) -L -T1 -T2 [ #I #L #H #F #K destruct // | #L #s #H #F #K destruct // @@ -187,11 +187,11 @@ qed-. (* Advanced inversion lemmas with restricted rt-transition for terms ********) -lemma cpm_tdeq_inv_bind_sn_void (a) (h) (n) (p) (I) (G) (L): - ∀V,T1. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] → +lemma cpm_tdeq_inv_bind_sn_void (h) (a) (n) (p) (I) (G) (L): + ∀V,T1. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ![h,a] → ∀X. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ➡[n,h] X → ⓑ{p,I}V.T1 ≛ X → - ∃∃T2. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G,L.ⓧ⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓑ{p,I}V.T2. -#a #h #n #p #I #G #L #V #T1 #H0 #X #H1 #H2 + ∃∃T2. ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ![h,a] & ⦃G,L.ⓧ⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓑ{p,I}V.T2. +#h #a #n #p #I #G #L #V #T1 #H0 #X #H1 #H2 elim (cpm_tdeq_inv_bind_sn … H0 … H1 H2) -H0 -H1 -H2 #T2 #HV #HT1 #H1T12 #H2T12 #H /3 width=5 by ex5_intro, cpm_tdeq_free/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma index 43952ffcf..54cd32a9e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma @@ -17,8 +17,8 @@ include "basic_2/dynamic/cnv_cpm_tdeq.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -definition IH_cnv_cpm_tdeq_conf_lpr (a) (h): relation3 genv lenv term ≝ - λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![a,h] → +definition IH_cnv_cpm_tdeq_conf_lpr (h) (a): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] → ∀n1,T1. ⦃G,L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛ T1 → ∀n2,T2. ⦃G,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛ T2 → ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ➡[h] L2 → @@ -38,14 +38,14 @@ fact cnv_cpm_tdeq_conf_lpr_atom_ess_aux (h) (G0) (L1) (L2) (s): /3 width=5 by tdeq_sort, ex4_intro/ qed-. -fact cnv_cpm_tdeq_conf_lpr_bind_bind_aux (a) (h) (p) (I) (G0) (L0) (V0) (T0): - (∀G,L,T. ⦃G0,L0,ⓑ{p,I}V0.T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr a h G L T) → - ⦃G0,L0⦄ ⊢ ⓑ{p,I}V0.T0 ![a,h] → +fact cnv_cpm_tdeq_conf_lpr_bind_bind_aux (h) (a) (p) (I) (G0) (L0) (V0) (T0): + (∀G,L,T. ⦃G0,L0,ⓑ{p,I}V0.T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr h a G L T) → + ⦃G0,L0⦄ ⊢ ⓑ{p,I}V0.T0 ![h,a] → ∀n1,T1. ⦃G0,L0.ⓑ{I}V0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛ T1 → ∀n2,T2. ⦃G0,L0.ⓑ{I}V0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛ T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ ⓑ{p,I}V0.T1 ➡[n2-n1,h] T & ⓑ{p,I}V0.T1 ≛ T & ⦃G0,L2⦄ ⊢ ⓑ{p,I}V0.T2 ➡[n1-n2,h] T & ⓑ{p,I}V0.T2 ≛ T. -#a #h #p #I #G0 #L0 #V0 #T0 #IH #H0 +#h #a #p #I #G0 #L0 #V0 #T0 #IH #H0 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #_ #HT0 @@ -54,14 +54,14 @@ elim (IH … H1T01 H2T01 … H1T02 H2T02 (L1.ⓑ{I}V0) … (L2.ⓑ{I}V0)) [|*: / /3 width=7 by cpm_bind, tdeq_pair, ex4_intro/ qed-. -fact cnv_cpm_tdeq_conf_lpr_appl_appl_aux (a) (h) (G0) (L0) (V0) (T0): - (∀G,L,T. ⦃G0,L0,ⓐV0.T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr a h G L T) → - ⦃G0,L0⦄ ⊢ ⓐV0.T0 ![a,h] → +fact cnv_cpm_tdeq_conf_lpr_appl_appl_aux (h) (a) (G0) (L0) (V0) (T0): + (∀G,L,T. ⦃G0,L0,ⓐV0.T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr h a G L T) → + ⦃G0,L0⦄ ⊢ ⓐV0.T0 ![h,a] → ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛ T1 → ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛ T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ ⓐV0.T1 ➡[n2-n1,h] T & ⓐV0.T1 ≛ T & ⦃G0,L2⦄ ⊢ ⓐV0.T2 ➡[n1-n2,h] T & ⓐV0.T2 ≛ T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #_ #HT0 #_ #_ -n0 -p0 -X01 -X02 @@ -70,16 +70,16 @@ elim (IH … H1T01 H2T01 … H1T02 H2T02 … HL01 … HL02) [|*: /2 width=1 by f /3 width=7 by cpm_appl, tdeq_pair, ex4_intro/ qed-. -fact cnv_cpm_tdeq_conf_lpr_cast_cast_aux (a) (h) (G0) (L0) (V0) (T0): - (∀G,L,T. ⦃G0,L0,ⓝV0.T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr a h G L T) → - ⦃G0,L0⦄ ⊢ ⓝV0.T0 ![a,h] → +fact cnv_cpm_tdeq_conf_lpr_cast_cast_aux (h) (a) (G0) (L0) (V0) (T0): + (∀G,L,T. ⦃G0,L0,ⓝV0.T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr h a G L T) → + ⦃G0,L0⦄ ⊢ ⓝV0.T0 ![h,a] → ∀n1,V1. ⦃G0,L0⦄ ⊢ V0 ➡[n1,h] V1 → V0 ≛ V1 → ∀n2,V2. ⦃G0,L0⦄ ⊢ V0 ➡[n2,h] V2 → V0 ≛ V2 → ∀T1. ⦃G0,L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛ T1 → ∀T2. ⦃G0,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛ T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⓝV1.T1 ≛ T & ⦃G0,L2⦄ ⊢ ⓝV2.T2 ➡[n1-n2,h] T & ⓝV2.T2 ≛ T. -#a #h #G0 #L0 #V0 #T0 #IH #H0 +#h #a #G0 #L0 #V0 #T0 #IH #H0 #n1 #V1 #H1V01 #H2V01 #n2 #V2 #H1V02 #H2V02 #T1 #H1T01 #H2T01 #T2 #H1T02 #H2T02 #L1 #HL01 #L2 #HL02 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0 @@ -89,10 +89,10 @@ elim (IH … H1T01 H2T01 … H1T02 H2T02 … HL01 … HL02) [|*: /2 width=1 by f /3 width=7 by cpm_cast, tdeq_pair, ex4_intro/ qed-. -fact cnv_cpm_tdeq_conf_lpr_aux (a) (h) (G0) (L0) (T0): - (∀G,L,T. ⦃G0,L0,T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr a h G L T) → - ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpm_tdeq_conf_lpr a h G L T. -#a #h #G0 #L0 #T0 #IH1 #G #L * [| * [| * ]] +fact cnv_cpm_tdeq_conf_lpr_aux (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr h a G L T) → + ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpm_tdeq_conf_lpr h a G L T. +#h #a #G0 #L0 #T0 #IH1 #G #L * [| * [| * ]] [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #H1X2 #H2X2 #L1 #HL1 #L2 #HL2 destruct elim (cpm_tdeq_inv_atom_sn … H1X1 H2X1) -H1X1 -H2X1 * elim (cpm_tdeq_inv_atom_sn … H1X2 H2X2) -H1X2 -H2X2 * @@ -127,9 +127,9 @@ fact cnv_cpm_tdeq_conf_lpr_aux (a) (h) (G0) (L0) (T0): ] qed-. -lemma cnv_cpm_tdeq_conf_lpr (a) (h) (G0) (L0) (T0): - IH_cnv_cpm_tdeq_conf_lpr a h G0 L0 T0. -#a #h #G0 #L0 #T0 +lemma cnv_cpm_tdeq_conf_lpr (h) (a) (G0) (L0) (T0): + IH_cnv_cpm_tdeq_conf_lpr h a G0 L0 T0. +#h #a #G0 #L0 #T0 @(fqup_wf_ind (Ⓣ) … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH /3 width=17 by cnv_cpm_tdeq_conf_lpr_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma index fd77a19b2..c71ef297a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma @@ -17,19 +17,19 @@ include "basic_2/dynamic/cnv_cpm_tdeq.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -definition IH_cnv_cpm_tdeq_cpm_trans (a) (h): relation3 genv lenv term ≝ - λG,L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] → - ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛ T → +definition IH_cnv_cpm_tdeq_cpm_trans (h) (a): relation3 genv lenv term ≝ + λG,L,T1. ⦃G,L⦄ ⊢ T1 ![h,a] → + ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛ T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛ T2. (* Transitive properties restricted rt-transition for terms *****************) -fact cnv_cpm_tdeq_cpm_trans_sub (a) (h) (G0) (L0) (T0): - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_cpm_trans a h G L T) → - ∀G,L,T1. G0 = G → L0 = L → T0 = T1 → IH_cnv_cpm_tdeq_cpm_trans a h G L T1. -#a #h #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]] +fact cnv_cpm_tdeq_cpm_trans_sub (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_cpm_trans h a G L T) → + ∀G,L,T1. G0 = G → L0 = L → T0 = T1 → IH_cnv_cpm_tdeq_cpm_trans h a G L T1. +#h #a #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]] [ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -G0 -L0 -T0 elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X * [ #H1 #H2 destruct /2 width=4 by ex3_intro/ @@ -88,10 +88,10 @@ fact cnv_cpm_tdeq_cpm_trans_sub (a) (h) (G0) (L0) (T0): ] qed-. -fact cnv_cpm_tdeq_cpm_trans_aux (a) (h) (G0) (L0) (T0): - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - IH_cnv_cpm_tdeq_cpm_trans a h G0 L0 T0. -#a #h #G0 #L0 #T0 +fact cnv_cpm_tdeq_cpm_trans_aux (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + IH_cnv_cpm_tdeq_cpm_trans h a G0 L0 T0. +#h #a #G0 #L0 #T0 @(fqup_wf_ind (Ⓣ) … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #IH0 /5 width=10 by cnv_cpm_tdeq_cpm_trans_sub, fqup_fpbg_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma index f1c856801..84ef77264 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma @@ -23,12 +23,12 @@ include "basic_2/dynamic/lsubv_cnv.ma". (* Sub preservation propery with t-bound rt-transition for terms ************) -fact cnv_cpm_trans_lpr_aux (a) (h): +fact cnv_cpm_trans_lpr_aux (h) (a): ∀G0,L0,T0. - (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → - (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1. -#a #h #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ] + (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → + (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr h a G1 L1 T1. +#h #a #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1 elim (cpm_inv_sort1 … H2) -H2 #H #_ destruct // | #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma index 9e0da7d55..a3aa68739 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma @@ -20,17 +20,17 @@ include "basic_2/dynamic/cnv_preserve.ma". (* Properties with t-bound evaluation on terms ******************************) -lemma cnv_cpme_trans (a) (h) (n) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → - ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h]. -#a #h #n #G #L #T1 #HT1 #T2 * #HT12 #_ +lemma cnv_cpme_trans (h) (a) (n) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![h,a]. +#h #a #n #G #L #T1 #HT1 #T2 * #HT12 #_ /2 width=4 by cnv_cpms_trans/ qed-. -lemma cnv_cpme_cpms_conf (a) (h) (n) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → +lemma cnv_cpme_cpms_conf (h) (a) (n) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄. -#a #h #n #G #L #T0 #HT0 #T1 #HT01 #T2 * #HT02 #HT2 +#h #a #n #G #L #T0 #HT0 #T1 #HT01 #T2 * #HT02 #HT2 elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 [h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ⦃G0,L0⦄ ⊢ T0 ![a,h] → +fact cnv_cpms_conf_lpr_tdeq_tdeq_aux (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → + ⦃G0,L0⦄ ⊢ T0 ![h,a] → ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 → ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛ T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T. -#a #h #G #L0 #T0 #IH2 #IH1 #HT0 +#h #a #G #L0 #T0 #IH2 #IH1 #HT0 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02 #L1 #HL01 #L2 #HL02 elim (cnv_cpms_tdeq_conf_lpr_aux … IH2 IH1 … H1T01 … H1T02 … HL01 … HL02) -IH2 -IH1 -H1T01 -H1T02 -HL01 -HL02 /2 width=3 by ex2_intro/ qed-. -fact cnv_cpms_conf_lpr_refl_tdneq_sub (a) (h) (G0) (L0) (T0) (m21) (m22): - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ⦃G0,L0⦄ ⊢ T0 ![a,h] → +fact cnv_cpms_conf_lpr_refl_tdneq_sub (h) (a) (G0) (L0) (T0) (m21) (m22): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → + ⦃G0,L0⦄ ⊢ T0 ![h,a] → ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ T0 ➡*[m21+m22,h] T& ⦃G0,L2⦄ ⊢ T2 ➡*[h] T. -#a #h #G0 #L0 #T0 #m21 #m22 #IH2 #IH1 #H0 +#h #a #G0 #L0 #T0 #m21 #m22 #IH2 #IH1 #H0 #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2 @@ -56,15 +56,15 @@ lapply (cpms_trans … HTY2 … HY2) -Y2 #HT2Y /2 width=3 by ex2_intro/ qed-. -fact cnv_cpms_conf_lpr_step_tdneq_sub (a) (h) (G0) (L0) (T0) (m11) (m12) (m21) (m22): - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ⦃G0,L0⦄ ⊢ T0 ![a,h] → +fact cnv_cpms_conf_lpr_step_tdneq_sub (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (m22): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → + ⦃G0,L0⦄ ⊢ T0 ![h,a] → ∀X1. ⦃G0,L0⦄ ⊢ T0 ➡[m11,h] X1 → T0 ≛ X1 → ∀T1. ⦃G0,L0⦄ ⊢ X1 ➡*[m12,h] T1 → X1 ≛ T1 → ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → - ((∀G,L,T. ⦃G0,L0,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → + ((∀G,L,T. ⦃G0,L0,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → ∀m21,m22. ∀X2. ⦃G0,L0⦄ ⊢ X1 ➡[m21,h] X2 → (X1 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → @@ -72,7 +72,7 @@ fact cnv_cpms_conf_lpr_step_tdneq_sub (a) (h) (G0) (L0) (T0) (m11) (m12) (m21) ( ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-m12,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m12-(m21+m22),h]T ) → ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T. -#a #h #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #HT0 +#h #a #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #HT0 #X1 #H1X01 #H2X01 #T1 #H1XT1 #H2XT1 #X2 #H1X02 #H2X02 #T2 #HXT2 #L1 #HL01 #L2 #HL02 #IH lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X01 … L0 ?) // #HX1 @@ -98,15 +98,15 @@ lapply (cpms_trans … HTZ2 … HZ02) -Z2 [h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ⦃G0,L0⦄ ⊢ T0 ![a,h] → +fact cnv_cpms_conf_lpr_tdeq_tdneq_aux (h) (a) (G0) (L0) (T0) (n1) (m21) (m22): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → + ⦃G0,L0⦄ ⊢ T0 ![h,a] → ∀T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 → ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-n1,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-(m21+m22),h] T. -#a #h #G0 #L0 #T0 #n1 #m21 #m22 #IH2 #IH1 #HT0 +#h #a #G0 #L0 #T0 #n1 #m21 #m22 #IH2 #IH1 #HT0 #T1 #H1T01 #H2T01 generalize in match m22; generalize in match m21; -m21 -m22 generalize in match IH1; generalize in match IH2; @@ -121,15 +121,15 @@ generalize in match IH1; generalize in match IH2; ] qed-. -fact cnv_cpms_conf_lpr_tdneq_tdneq_aux (a) (h) (G0) (L0) (T0) (m11) (m12) (m21) (m22): - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ⦃G0,L0⦄ ⊢ T0 ![a,h] → +fact cnv_cpms_conf_lpr_tdneq_tdneq_aux (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (m22): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → + ⦃G0,L0⦄ ⊢ T0 ![h,a] → ∀X1. ⦃G0,L0⦄ ⊢ T0 ➡[m11,h] X1 → (T0 ≛ X1 → ⊥) → ∀T1. ⦃G0,L0⦄ ⊢ X1 ➡*[m12,h] T1 → ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T. -#a #h #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #H0 +#h #a #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #H0 #X1 #HX01 #HnX01 #T1 #HXT1 #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1 @@ -146,11 +146,11 @@ lapply (cpms_trans … HTZ2 … HZ02) -Z2 [h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpms_conf_lpr a h G L T. -#a #h #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT +fact cnv_cpms_conf_lpr_aux (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → + ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpms_conf_lpr h a G L T. +#h #a #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT #HT0 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 destruct elim (tdeq_dec T0 T1) #H2T01 elim (tdeq_dec T0 T2) #H2T02 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma index 8394bfa8d..b0c9d9e16 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma @@ -18,12 +18,12 @@ include "basic_2/dynamic/cnv_cpm_tdeq_trans.ma". (* Properties with restricted rt-computation for terms **********************) -fact cpms_tdneq_fwd_step_sn_aux (a) (h) (n) (G) (L) (T1): - ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ![a,h] → (T1 ≛ T2 → ⊥) → - (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → +fact cpms_tdneq_fwd_step_sn_aux (h) (a) (n) (G) (L) (T1): + ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ![h,a] → (T1 ≛ T2 → ⊥) → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) → ∃∃n1,n2,T0. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T0 & T1 ≛ T0 → ⊥ & ⦃G,L⦄ ⊢ T0 ➡*[n2,h] T2 & n1+n2 = n. -#a #h #n #G #L #T1 #T2 #H +#h #a #n #G #L #T1 #T2 #H @(cpms_ind_sn … H) -n -T1 [ #_ #H2T2 elim H2T2 -H2T2 // | #n1 #n2 #T1 #T #H1T1 #H1T2 #IH #H0T1 #H2T12 #IH2 #IH1 @@ -42,14 +42,14 @@ fact cpms_tdneq_fwd_step_sn_aux (a) (h) (n) (G) (L) (T1): ] qed-. -fact cpms_tdeq_ind_sn (a) (h) (G) (L) (T2) (Q:relation2 …): - (⦃G,L⦄ ⊢ T2 ![a,h] → Q 0 T2) → - (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ⦃G,L⦄ ⊢ T1 ![a,h] → T1 ≛ T → ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 → ⦃G,L⦄ ⊢ T ![a,h] → T ≛ T2 → Q n2 T → Q (n1+n2) T1) → - ∀n,T1. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ![a,h] → T1 ≛ T2 → - (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → +fact cpms_tdeq_ind_sn (h) (a) (G) (L) (T2) (Q:relation2 …): + (⦃G,L⦄ ⊢ T2 ![h,a] → Q 0 T2) → + (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ⦃G,L⦄ ⊢ T1 ![h,a] → T1 ≛ T → ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 → ⦃G,L⦄ ⊢ T ![h,a] → T ≛ T2 → Q n2 T → Q (n1+n2) T1) → + ∀n,T1. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ![h,a] → T1 ≛ T2 → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) → Q n T1. -#a #h #G #L #T2 #Q #IB1 #IB2 #n #T1 #H +#h #a #G #L #T2 #Q #IB1 #IB2 #n #T1 #H @(cpms_ind_sn … H) -n -T1 [ -IB2 #H0T2 #_ #_ #_ /2 width=1 by/ | #n1 #n2 #T1 #T #H1T1 #H1T2 #IH #H0T1 #H2T12 #IH2 #IH1 -IB1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma index 44d549d53..20759ddc7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma @@ -19,14 +19,14 @@ include "basic_2/dynamic/cnv_cpms_tdeq.ma". (* Sub confluence propery with restricted rt-transition for terms ***********) -fact cnv_cpms_tdeq_strip_lpr_aux (a) (h) (G0) (L0) (T0): - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![a,h] → T0 ≛ T1 → +fact cnv_cpms_tdeq_strip_lpr_aux (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → + ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![h,a] → T0 ≛ T1 → ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛ T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡[n2-n1,h] T & T1 ≛ T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T & T2 ≛ T. -#a #h #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01 +#h #a #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01 @(cpms_tdeq_ind_sn … H1T01 H0T0 H2T01 IH1 IH2) -n1 -T0 [ #H0T1 #n2 #T2 #H1T12 #H2T12 #L1 #HL01 #L2 #HL02 [h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![a,h] → T0 ≛ T1 → +fact cnv_cpms_tdeq_conf_lpr_aux (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr h a G L T) → + ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![h,a] → T0 ≛ T1 → ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛ T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & T1 ≛ T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T & T2 ≛ T. -#a #h #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01 +#h #a #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01 generalize in match IH1; generalize in match IH2; @(cpms_tdeq_ind_sn … H1T01 H0T0 H2T01 IH1 IH2) -n1 -T0 [ #H0T1 #IH2 #IH1 #n2 #T2 #H1T12 #H2T12 #L1 #HL01 #L2 #HL02 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma index 9ba812a95..09dcccc3d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma @@ -20,22 +20,23 @@ include "basic_2/dynamic/cnv_preserve.ma". (* Properties with t-unbound whd evaluation on terms ************************) -lemma cnv_cpmuwe_trans (a) (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → - ∀T2,n. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2 → ⦃G,L⦄ ⊢ T2 ![a,h]. +lemma cnv_cpmuwe_trans (h) (a) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → + ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2 → ⦃G,L⦄ ⊢ T2 ![h,a]. /3 width=4 by cpmuwe_fwd_cpms, cnv_cpms_trans/ qed-. -lemma cnv_R_cpmuwe_total (a) (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmuwe h G L T1 n. +lemma cnv_R_cpmuwe_total (h) (a) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∃n. R_cpmuwe h G L T1 n. /4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmuwe_total_csx/ qed-. (* Main inversions with head evaluation for t-bound rt-transition on terms **) -theorem cnv_cpmuwe_mono (a) (h) (G) (L): - ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n1] T1 → - ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n2] T2 → +theorem cnv_cpmuwe_mono (h) (a) (G) (L): + ∀T0. ⦃G,L⦄ ⊢ T0 ![h,a] → + ∀n1,T1. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n1] T1 → + ∀n2,T2. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n2] T2 → ∧∧ ⦃G,L⦄ ⊢ T1 ⬌*[h,n2-n1,n1-n2] T2 & T1 ≅ T2. -#a #h #G #L #T0 #HT0 #T1 #n1 * #HT01 #HT1 #T2 #n2 * #HT02 #HT2 +#h #a #G #L #T0 #HT0 #n1 #T1 * #HT01 #HT1 #n2 #T2 * #HT02 #HT2 elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20 /4 width=4 by cpms_div, tweq_canc_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma index 992588e0b..801a56a09 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma @@ -21,9 +21,9 @@ include "basic_2/dynamic/cnv_cpme.ma". (* Advanced Properties with t-unbound whd evaluation on terms ***************) -lemma cnv_R_cpmuwe_dec (a) (h) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmuwe h G L T n). -#a #h #G #L #T1 #HT1 #n +lemma cnv_R_cpmuwe_dec (h) (a) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀n. Decidable (R_cpmuwe h G L T n). +#h #a #G #L #T1 #HT1 #n elim (cnv_fwd_aaa … HT1) #A #HA elim (cpme_total_aaa h n … HA) -HA #T2 #HT12 elim (cnuw_dec h G L T2) #HnT1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma index 71e115777..bb1e540fe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma @@ -20,10 +20,10 @@ include "basic_2/dynamic/cnv.ma". (* Advanced dproperties *****************************************************) (* Basic_2A1: uses: snv_lref *) -lemma cnv_lref_drops (a) (h) (G): - ∀I,K,V,i,L. ⦃G,K⦄ ⊢ V ![a,h] → - ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G,L⦄ ⊢ #i ![a,h]. -#a #h #G #I #K #V #i elim i -i +lemma cnv_lref_drops (h) (a) (G): + ∀I,K,V,i,L. ⦃G,K⦄ ⊢ V ![h,a] → + ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G,L⦄ ⊢ #i ![h,a]. +#h #a #G #I #K #V #i elim i -i [ #L #HV #H lapply (drops_fwd_isid … H ?) -H // #H destruct /2 width=1 by cnv_zero/ @@ -36,10 +36,10 @@ qed. (* Advanced inversion lemmas ************************************************) (* Basic_2A1: uses: snv_inv_lref *) -lemma cnv_inv_lref_drops (a) (h) (G): - ∀i,L. ⦃G,L⦄ ⊢ #i ![a,h] → - ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ V ![a,h]. -#a #h #G #i elim i -i +lemma cnv_inv_lref_drops (h) (a) (G): + ∀i,L. ⦃G,L⦄ ⊢ #i ![h,a] → + ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ V ![h,a]. +#h #a #G #i elim i -i [ #L #H elim (cnv_inv_zero … H) -H #I #K #V #HV #H destruct /3 width=5 by drops_refl, ex2_3_intro/ @@ -50,26 +50,26 @@ lemma cnv_inv_lref_drops (a) (h) (G): ] qed-. -lemma cnv_inv_lref_pair (a) (h) (G): - ∀i,L. ⦃G,L⦄ ⊢ #i ![a,h] → - ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G,K⦄ ⊢ V ![a,h]. -#a #h #G #i #L #H #I #K #V #HLK +lemma cnv_inv_lref_pair (h) (a) (G): + ∀i,L. ⦃G,L⦄ ⊢ #i ![h,a] → + ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G,K⦄ ⊢ V ![h,a]. +#h #a #G #i #L #H #I #K #V #HLK elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #HX lapply (drops_mono … HLY … HLK) -L #H destruct // qed-. -lemma cnv_inv_lref_atom (a) (h) (b) (G): - ∀i,L. ⦃G,L⦄ ⊢ #i ![a,h] → ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⊥. -#a #h #b #G #i #L #H #Hi +lemma cnv_inv_lref_atom (h) (a) (b) (G): + ∀i,L. ⦃G,L⦄ ⊢ #i ![h,a] → ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⊥. +#h #a #b #G #i #L #H #Hi elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #_ lapply (drops_gen b … HLY) -HLY #HLY lapply (drops_mono … HLY … Hi) -L #H destruct qed-. -lemma cnv_inv_lref_unit (a) (h) (G): - ∀i,L. ⦃G,L⦄ ⊢ #i ![a,h] → +lemma cnv_inv_lref_unit (h) (a) (G): + ∀i,L. ⦃G,L⦄ ⊢ #i ![h,a] → ∀I,K. ⬇*[i] L ≘ K.ⓤ{I} → ⊥. -#a #h #G #i #L #H #I #K #HLK +#h #a #G #i #L #H #I #K #HLK elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #_ lapply (drops_mono … HLY … HLK) -L #H destruct qed-. @@ -77,8 +77,8 @@ qed-. (* Properties with generic slicing for local environments *******************) (* Basic_2A1: uses: snv_lift *) -lemma cnv_lifts (a) (h): ∀G. d_liftable1 (cnv a h G). -#a #h #G #K #T +lemma cnv_lifts (h) (a): ∀G. d_liftable1 (cnv h a G). +#h #a #G #K #T @(fqup_wf_ind_eq (Ⓣ) … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * * [|||| * ] [ #s #HG #HK #HT #_ #b #f #L #_ #X #H2 destruct >(lifts_inv_sort1 … H2) -X -K -f // @@ -116,8 +116,8 @@ qed-. (* Inversion lemmas with generic slicing for local environments *************) (* Basic_2A1: uses: snv_inv_lift *) -lemma cnv_inv_lifts (a) (h): ∀G. d_deliftable1 (cnv a h G). -#a #h #G #L #U +lemma cnv_inv_lifts (h) (a): ∀G. d_deliftable1 (cnv h a G). +#h #a #G #L #U @(fqup_wf_ind_eq (Ⓣ) … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * * [|||| * ] [ #s #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct >(lifts_inv_sort2 … H2) -X -L -f // diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma index 363774648..efd2c3cce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma @@ -23,9 +23,9 @@ include "basic_2/dynamic/cnv_preserve_cpes.ma". (* main properties with evaluations for rt-transition on terms **************) -theorem cnv_dec (a) (h) (G) (L) (T): ac_props a → - Decidable (⦃G,L⦄ ⊢ T ![a,h]). -#a #h #G #L #T #Ha +theorem cnv_dec (h) (a) (G) (L) (T): ac_props a → + Decidable (⦃G,L⦄ ⊢ T ![h,a]). +#h #a #G #L #T #Ha @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ] [ #s #HG #HL #HT destruct -Ha -IH /2 width=1 by cnv_sort, or_introl/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma index 1c30ccce1..50e4edbee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma @@ -20,10 +20,10 @@ include "basic_2/dynamic/cnv_drops.ma". (* Properties with supclosure ***********************************************) (* Basic_2A1: uses: snv_fqu_conf *) -lemma cnv_fqu_conf (a) (h): +lemma cnv_fqu_conf (h) (a): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂ ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h]. -#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 + ⦃G1,L1⦄ ⊢ T1 ![h,a] → ⦃G2,L2⦄ ⊢ T2 ![h,a]. +#h #a #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I1 #G1 #L1 #V1 #H elim (cnv_inv_zero … H) -H #I2 #L2 #V2 #HV2 #H destruct // | * [ #p #I1 | * ] #G1 #L1 #V1 #T1 #H @@ -44,25 +44,25 @@ lemma cnv_fqu_conf (a) (h): qed-. (* Basic_2A1: uses: snv_fquq_conf *) -lemma cnv_fquq_conf (a) (h): +lemma cnv_fquq_conf (h) (a): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮ ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h]. -#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [|*] + ⦃G1,L1⦄ ⊢ T1 ![h,a] → ⦃G2,L2⦄ ⊢ T2 ![h,a]. +#h #a #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [|*] /2 width=5 by cnv_fqu_conf/ qed-. (* Basic_2A1: uses: snv_fqup_conf *) -lemma cnv_fqup_conf (a) (h): +lemma cnv_fqup_conf (h) (a): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂+ ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h]. -#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 + ⦃G1,L1⦄ ⊢ T1 ![h,a] → ⦃G2,L2⦄ ⊢ T2 ![h,a]. +#h #a #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 /3 width=5 by fqup_strap1, cnv_fqu_conf/ qed-. (* Basic_2A1: uses: snv_fqus_conf *) -lemma cnv_fqus_conf (a) (h): +lemma cnv_fqus_conf (h) (a): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂* ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h]. -#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_fqup … H) -H [|*] + ⦃G1,L1⦄ ⊢ T1 ![h,a] → ⦃G2,L2⦄ ⊢ T2 ![h,a]. +#h #a #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_fqup … H) -H [|*] /2 width=5 by cnv_fqup_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma index 7f754d97f..3716f67ea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma @@ -21,21 +21,21 @@ include "basic_2/dynamic/cnv_aaa.ma". (* Note: this is the "big tree" theorem *) (* Basic_2A1: uses: snv_fwd_fsb *) -lemma cnv_fwd_fsb (a) (h): - ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ≥[h] 𝐒⦃G,L,T⦄. -#a #h #G #L #T #H elim (cnv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/ +lemma cnv_fwd_fsb (h) (a): + ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a] → ≥[h] 𝐒⦃G,L,T⦄. +#h #a #G #L #T #H elim (cnv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/ qed-. (* Forward lemmas with strongly rt-normalizing terms ************************) -lemma cnv_fwd_csx (a) (h): - ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. -#a #h #G #L #T #H +lemma cnv_fwd_csx (h) (a): + ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a] → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. +#h #a #G #L #T #H /3 width=2 by cnv_fwd_fsb, fsb_inv_csx/ qed-. (* Inversion lemmas with proper parallel rst-computation for closures *******) -lemma cnv_fpbg_refl_false (a) (h): - ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃G,L,T⦄ >[h] ⦃G,L,T⦄ → ⊥. +lemma cnv_fpbg_refl_false (h) (a): + ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a] → ⦃G,L,T⦄ >[h] ⦃G,L,T⦄ → ⊥. /3 width=7 by cnv_fwd_fsb, fsb_fpbg_refl_false/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma index 178a2b846..9763d082a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma @@ -19,10 +19,10 @@ include "basic_2/dynamic/cnv_cpms_conf.ma". (* Main preservation properties *********************************************) (* Basic_2A1: uses: snv_preserve *) -lemma cnv_preserve (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → - ∧∧ IH_cnv_cpms_conf_lpr a h G L T - & IH_cnv_cpm_trans_lpr a h G L T. -#a #h #G #L #T #HT +lemma cnv_preserve (h) (a): ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a] → + ∧∧ IH_cnv_cpms_conf_lpr h a G L T + & IH_cnv_cpm_trans_lpr h a G L T. +#h #a #G #L #T #HT lapply (cnv_fwd_fsb … HT) -HT #H @(fsb_ind_fpbg … H) -G -L -T #G #L #T #_ #IH @conj [ letin aux ≝ cnv_cpms_conf_lpr_aux | letin aux ≝ cnv_cpm_trans_lpr_aux ] @@ -30,46 +30,46 @@ lapply (cnv_fwd_fsb … HT) -HT #H elim (IH … H) -IH -H // qed-. -theorem cnv_cpms_conf_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_conf_lpr a h G L T. -#a #h #G #L #T #HT elim (cnv_preserve … HT) /2 width=1 by/ +theorem cnv_cpms_conf_lpr (h) (a) (G) (L) (T): IH_cnv_cpms_conf_lpr h a G L T. +#h #a #G #L #T #HT elim (cnv_preserve … HT) /2 width=1 by/ qed-. (* Basic_2A1: uses: snv_cpr_lpr *) -theorem cnv_cpm_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpm_trans_lpr a h G L T. -#a #h #G #L #T #HT elim (cnv_preserve … HT) /2 width=2 by/ +theorem cnv_cpm_trans_lpr (h) (a) (G) (L) (T): IH_cnv_cpm_trans_lpr h a G L T. +#h #a #G #L #T #HT elim (cnv_preserve … HT) /2 width=2 by/ qed-. (* Advanced preservation properties *****************************************) -lemma cnv_cpms_conf (a) (h) (G) (L): - ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → +lemma cnv_cpms_conf (h) (a) (G) (L): + ∀T0. ⦃G,L⦄ ⊢ T0 ![h,a] → ∀n1,T1. ⦃G,L⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T0 ➡*[n2,h] T2 → ∃∃T. ⦃G,L⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L⦄ ⊢ T2 ➡*[n1-n2,h] T. /2 width=8 by cnv_cpms_conf_lpr/ qed-. (* Basic_2A1: uses: snv_cprs_lpr *) -lemma cnv_cpms_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_trans_lpr a h G L T. -#a #h #G #L1 #T1 #HT1 #n #T2 #H +lemma cnv_cpms_trans_lpr (h) (a) (G) (L) (T): IH_cnv_cpms_trans_lpr h a G L T. +#h #a #G #L1 #T1 #HT1 #n #T2 #H @(cpms_ind_dx … H) -n -T2 /3 width=6 by cnv_cpm_trans_lpr/ qed-. -lemma cnv_cpm_trans (a) (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → - ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → ⦃G,L⦄ ⊢ T2 ![a,h]. +lemma cnv_cpm_trans (h) (a) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → + ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → ⦃G,L⦄ ⊢ T2 ![h,a]. /2 width=6 by cnv_cpm_trans_lpr/ qed-. (* Note: this is the preservation property *) -lemma cnv_cpms_trans (a) (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → - ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T2 ![a,h]. +lemma cnv_cpms_trans (h) (a) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → + ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T2 ![h,a]. /2 width=6 by cnv_cpms_trans_lpr/ qed-. -lemma cnv_lpr_trans (a) (h) (G): - ∀L1,T. ⦃G,L1⦄ ⊢ T ![a,h] → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T ![a,h]. +lemma cnv_lpr_trans (h) (a) (G): + ∀L1,T. ⦃G,L1⦄ ⊢ T ![h,a] → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T ![h,a]. /2 width=6 by cnv_cpm_trans_lpr/ qed-. -lemma cnv_lprs_trans (a) (h) (G): - ∀L1,T. ⦃G,L1⦄ ⊢ T ![a,h] → ∀L2. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L2⦄ ⊢ T ![a,h]. -#a #h #G #L1 #T #HT #L2 #H +lemma cnv_lprs_trans (h) (a) (G): + ∀L1,T. ⦃G,L1⦄ ⊢ T ![h,a] → ∀L2. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L2⦄ ⊢ T ![h,a]. +#h #a #G #L1 #T #HT #L2 #H @(lprs_ind_dx … H) -L2 /2 width=3 by cnv_lpr_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma index ba4b824ce..29d85f7bd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma @@ -19,20 +19,20 @@ include "basic_2/dynamic/cnv_preserve.ma". (* Forward lemmas with r-equivalence ****************************************) -lemma cnv_cpms_conf_eq (a) (h) (n) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → +lemma cnv_cpms_conf_eq (h) (a) (n) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2. -#a #h #n #G #L #T #HT #T1 #HT1 #T2 #HT2 +#h #a #n #G #L #T #HT #T1 #HT1 #T2 #HT2 elim (cnv_cpms_conf … HT … HT1 … HT2) -T [h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → - ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1. -#a #h #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H + (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) → + ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_trans_lpr h a G1 L1 T1. +#h #a #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H @(cpms_ind_dx … H) -n -T2 /3 width=7 by fpbg_cpms_trans/ qed-. -fact cnv_cpm_conf_lpr_sub (a) (h): +fact cnv_cpm_conf_lpr_sub (h) (a): ∀G0,L0,T0. - (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → - ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_conf_lpr a h G1 L1 T1. + (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → + ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_conf_lpr h a G1 L1 T1. /3 width=8 by cpm_cpms/ qed-. -fact cnv_cpms_strip_lpr_sub (a) (h): +fact cnv_cpms_strip_lpr_sub (h) (a): ∀G0,L0,T0. - (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → - ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1. + (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → + ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_strip_lpr h a G1 L1 T1. /3 width=8 by cpm_cpms/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma index fdf2ad803..2ff320b82 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma @@ -17,22 +17,22 @@ include "basic_2/dynamic/cnv.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) -inductive lsubv (a) (h) (G): relation lenv ≝ -| lsubv_atom: lsubv a h G (⋆) (⋆) -| lsubv_bind: ∀I,L1,L2. lsubv a h G L1 L2 → lsubv a h G (L1.ⓘ{I}) (L2.ⓘ{I}) -| lsubv_beta: ∀L1,L2,W,V. ⦃G,L1⦄ ⊢ ⓝW.V ![a,h] → - lsubv a h G L1 L2 → lsubv a h G (L1.ⓓⓝW.V) (L2.ⓛW) +inductive lsubv (h) (a) (G): relation lenv ≝ +| lsubv_atom: lsubv h a G (⋆) (⋆) +| lsubv_bind: ∀I,L1,L2. lsubv h a G L1 L2 → lsubv h a G (L1.ⓘ{I}) (L2.ⓘ{I}) +| lsubv_beta: ∀L1,L2,W,V. ⦃G,L1⦄ ⊢ ⓝW.V ![h,a] → + lsubv h a G L1 L2 → lsubv h a G (L1.ⓓⓝW.V) (L2.ⓛW) . interpretation "local environment refinement (native validity)" - 'LRSubEqV a h G L1 L2 = (lsubv a h G L1 L2). + 'LRSubEqV h a G L1 L2 = (lsubv h a G L1 L2). (* Basic inversion lemmas ***************************************************) -fact lsubv_inv_atom_sn_aux (a) (h) (G): - ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 = ⋆ → L2 = ⋆. -#a #h #G #L1 #L2 * -L1 -L2 +fact lsubv_inv_atom_sn_aux (h) (a) (G): + ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 → L1 = ⋆ → L2 = ⋆. +#h #a #G #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #_ #H destruct | #L1 #L2 #W #V #_ #_ #H destruct @@ -40,16 +40,16 @@ fact lsubv_inv_atom_sn_aux (a) (h) (G): qed-. (* Basic_2A1: uses: lsubsv_inv_atom1 *) -lemma lsubv_inv_atom_sn (a) (h) (G): - ∀L2. G ⊢ ⋆ ⫃![a,h] L2 → L2 = ⋆. +lemma lsubv_inv_atom_sn (h) (a) (G): + ∀L2. G ⊢ ⋆ ⫃![h,a] L2 → L2 = ⋆. /2 width=6 by lsubv_inv_atom_sn_aux/ qed-. -fact lsubv_inv_bind_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → +fact lsubv_inv_bind_sn_aux (h) (a) (G): ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 → ∀I,K1. L1 = K1.ⓘ{I} → - ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I} - | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] & G ⊢ K1 ⫃![a,h] K2 + ∨∨ ∃∃K2. G ⊢ K1 ⫃![h,a] K2 & L2 = K2.ⓘ{I} + | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![h,a] & G ⊢ K1 ⫃![h,a] K2 & I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW. -#a #h #G #L1 #L2 * -L1 -L2 +#h #a #G #L1 #L2 * -L1 -L2 [ #J #K1 #H destruct | #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by ex2_intro, or_introl/ | #L1 #L2 #W #V #HWV #HL12 #J #K1 #H destruct /3 width=7 by ex4_3_intro, or_intror/ @@ -57,16 +57,16 @@ fact lsubv_inv_bind_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → qed-. (* Basic_2A1: uses: lsubsv_inv_pair1 *) -lemma lsubv_inv_bind_sn (a) (h) (G): - ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 → - ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I} - | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] & G ⊢ K1 ⫃![a,h] K2 +lemma lsubv_inv_bind_sn (h) (a) (G): + ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![h,a] L2 → + ∨∨ ∃∃K2. G ⊢ K1 ⫃![h,a] K2 & L2 = K2.ⓘ{I} + | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![h,a] & G ⊢ K1 ⫃![h,a] K2 & I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW. /2 width=3 by lsubv_inv_bind_sn_aux/ qed-. -fact lsubv_inv_atom_dx_aux (a) (h) (G): - ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 = ⋆ → L1 = ⋆. -#a #h #G #L1 #L2 * -L1 -L2 +fact lsubv_inv_atom_dx_aux (h) (a) (G): + ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 → L2 = ⋆ → L1 = ⋆. +#h #a #G #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #_ #H destruct | #L1 #L2 #W #V #_ #_ #H destruct @@ -74,17 +74,17 @@ fact lsubv_inv_atom_dx_aux (a) (h) (G): qed-. (* Basic_2A1: uses: lsubsv_inv_atom2 *) -lemma lsubv_inv_atom2 (a) (h) (G): - ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → L1 = ⋆. +lemma lsubv_inv_atom2 (h) (a) (G): + ∀L1. G ⊢ L1 ⫃![h,a] ⋆ → L1 = ⋆. /2 width=6 by lsubv_inv_atom_dx_aux/ qed-. -fact lsubv_inv_bind_dx_aux (a) (h) (G): - ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → +fact lsubv_inv_bind_dx_aux (h) (a) (G): + ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 → ∀I,K2. L2 = K2.ⓘ{I} → - ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I} - | ∃∃K1,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] & - G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V. -#a #h #G #L1 #L2 * -L1 -L2 + ∨∨ ∃∃K1. G ⊢ K1 ⫃![h,a] K2 & L1 = K1.ⓘ{I} + | ∃∃K1,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![h,a] & + G ⊢ K1 ⫃![h,a] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V. +#h #a #G #L1 #L2 * -L1 -L2 [ #J #K2 #H destruct | #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or_introl/ | #L1 #L2 #W #V #HWV #HL12 #J #K2 #H destruct /3 width=7 by ex4_3_intro, or_intror/ @@ -92,19 +92,19 @@ fact lsubv_inv_bind_dx_aux (a) (h) (G): qed-. (* Basic_2A1: uses: lsubsv_inv_pair2 *) -lemma lsubv_inv_bind_dx (a) (h) (G): - ∀I,L1,K2. G ⊢ L1 ⫃![a,h] K2.ⓘ{I} → - ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I} - | ∃∃K1,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] & - G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V. +lemma lsubv_inv_bind_dx (h) (a) (G): + ∀I,L1,K2. G ⊢ L1 ⫃![h,a] K2.ⓘ{I} → + ∨∨ ∃∃K1. G ⊢ K1 ⫃![h,a] K2 & L1 = K1.ⓘ{I} + | ∃∃K1,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![h,a] & + G ⊢ K1 ⫃![h,a] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V. /2 width=3 by lsubv_inv_bind_dx_aux/ qed-. (* Advanced inversion lemmas ************************************************) -lemma lsubv_inv_abst_sn (a) (h) (G): - ∀K1,L2,W. G ⊢ K1.ⓛW ⫃![a,h] L2 → - ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓛW. -#a #h #G #K1 #L2 #W #H +lemma lsubv_inv_abst_sn (h) (a) (G): + ∀K1,L2,W. G ⊢ K1.ⓛW ⫃![h,a] L2 → + ∃∃K2. G ⊢ K1 ⫃![h,a] K2 & L2 = K2.ⓛW. +#h #a #G #K1 #L2 #W #H elim (lsubv_inv_bind_sn … H) -H // * #K2 #XW #XV #_ #_ #H1 #H2 destruct qed-. @@ -112,8 +112,8 @@ qed-. (* Basic properties *********************************************************) (* Basic_2A1: uses: lsubsv_refl *) -lemma lsubv_refl (a) (h) (G): reflexive … (lsubv a h G). -#a #h #G #L elim L -L /2 width=1 by lsubv_atom, lsubv_bind/ +lemma lsubv_refl (h) (a) (G): reflexive … (lsubv h a G). +#h #a #G #L elim L -L /2 width=1 by lsubv_atom, lsubv_bind/ qed. (* Basic_2A1: removed theorems 3: diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma index 271b5d5b8..122c30c41 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma @@ -19,10 +19,10 @@ include "basic_2/dynamic/lsubv_cpms.ma". (* Forward lemmas with native validity **************************************) (* Basic_2A1: uses: lsubsv_snv_trans *) -lemma lsubv_cnv_trans (a) (h) (G): - ∀L2,T. ⦃G,L2⦄ ⊢ T ![a,h] → - ∀L1. G ⊢ L1 ⫃![a,h] L2 → ⦃G,L1⦄ ⊢ T ![a,h]. -#a #h #G #L2 #T #H elim H -G -L2 -T // +lemma lsubv_cnv_trans (h) (a) (G): + ∀L2,T. ⦃G,L2⦄ ⊢ T ![h,a] → + ∀L1. G ⊢ L1 ⫃![h,a] L2 → ⦃G,L1⦄ ⊢ T ![h,a]. +#h #a #G #L2 #T #H elim H -G -L2 -T // [ #I #G #K2 #V #HV #IH #L1 #H elim (lsubv_inv_bind_dx … H) -H * /3 width=1 by cnv_zero/ | #I #G #K2 #i #_ #IH #L1 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma index c02ec80b0..aad53743d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma @@ -20,6 +20,6 @@ include "basic_2/dynamic/lsubv_lsubr.ma". (* Forward lemmas with context-sensitive r-equivalence for terms ************) (* Basic_2A1: uses: lsubsv_cprs_trans *) -lemma lsubv_cpcs_trans (a) (h) (G): lsub_trans … (cpcs h G) (lsubv a h G). +lemma lsubv_cpcs_trans (h) (a) (G): lsub_trans … (cpcs h G) (lsubv h a G). /3 width=6 by lsubv_fwd_lsubr, lsubr_cpcs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma index ba08f8818..6d53694c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma @@ -20,7 +20,7 @@ include "basic_2/dynamic/lsubv_lsubr.ma". (* Forward lemmas with t-bound contex-sensitive rt-computation for terms ****) (* Basic_2A1: uses: lsubsv_cprs_trans lsubsv_scpds_trans *) -lemma lsubv_cpms_trans (a) (n) (h) (G): - lsub_trans … (λL. cpms h G L n) (lsubv a h G). +lemma lsubv_cpms_trans (h) (a) (n) (G): + lsub_trans … (λL. cpms h G L n) (lsubv h a G). /3 width=6 by lsubv_fwd_lsubr, lsubr_cpms_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma index 63b53ec72..6b0daf223 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma @@ -21,11 +21,11 @@ include "basic_2/dynamic/lsubv.ma". (* Note: the premise 𝐔⦃f⦄ cannot be removed *) (* Basic_2A1: includes: lsubsv_drop_O1_conf *) -lemma lsubv_drops_conf_isuni (a) (h) (G): - ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → +lemma lsubv_drops_conf_isuni (h) (a) (G): + ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 → ∀b,f,K1. 𝐔⦃f⦄ → ⬇*[b,f] L1 ≘ K1 → - ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L2 ≘ K2. -#a #h #G #L1 #L2 #H elim H -L1 -L2 + ∃∃K2. G ⊢ K1 ⫃![h,a] K2 & ⬇*[b,f] L2 ≘ K2. +#h #a #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #HL12 #IH #b #f #K1 #Hf #H elim (drops_inv_bind1_isuni … Hf H) -Hf -H * @@ -46,11 +46,11 @@ qed-. (* Note: the premise 𝐔⦃f⦄ cannot be removed *) (* Basic_2A1: includes: lsubsv_drop_O1_trans *) -lemma lsubv_drops_trans_isuni (a) (h) (G): - ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → +lemma lsubv_drops_trans_isuni (h) (a) (G): + ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 → ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2 → - ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L1 ≘ K1. -#a #h #G #L1 #L2 #H elim H -L1 -L2 + ∃∃K1. G ⊢ K1 ⫃![h,a] K2 & ⬇*[b,f] L1 ≘ K1. +#h #a #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #HL12 #IH #b #f #K2 #Hf #H elim (drops_inv_bind1_isuni … Hf H) -Hf -H * diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma index daede63b3..969751d2d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma @@ -20,8 +20,8 @@ include "basic_2/dynamic/lsubv.ma". (* Forward lemmas with lenv refinement for atomic arity assignment **********) (* Basic_2A1: uses: lsubsv_fwd_lsuba *) -lemma lsubsv_fwd_lsuba (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → G ⊢ L1 ⫃⁝ L2. -#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_bind/ +lemma lsubsv_fwd_lsuba (h) (a) (G): ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 → G ⊢ L1 ⫃⁝ L2. +#h #a #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_bind/ #L1 #L2 #W #V #H #_ #IH elim (cnv_inv_cast … H) -H #W0 #HW #HV #HW0 #HVW0 elim (cnv_fwd_aaa … HW) -HW #B #HW diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma index 938c116c5..fe2f3760c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma @@ -20,6 +20,6 @@ include "basic_2/dynamic/lsubv.ma". (* Forward lemmas with restricted refinement for local environments *********) (* Basic_2A1: uses: lsubsv_fwd_lsubr *) -lemma lsubv_fwd_lsubr (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 ⫃ L2. -#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_beta/ +lemma lsubv_fwd_lsubr (h) (a) (G): ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 → L1 ⫃ L2. +#h #a #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_beta/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma index d416b5f40..0108c0163 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma @@ -19,8 +19,8 @@ include "basic_2/dynamic/lsubv_cnv.ma". (* Main properties **********************************************************) (* Note: not valid in Basic_2A1 *) -theorem lsubv_trans (a) (h) (G): Transitive … (lsubv a h G). -#a #h #G #L1 #L #H elim H -L1 -L // +theorem lsubv_trans (h) (a) (G): Transitive … (lsubv h a G). +#h #a #G #L1 #L #H elim H -L1 -L // [ #I #K1 #K #HK1 #IH #Y #H elim (lsubv_inv_bind_sn … H) -H * [ #K2 #HK2 #H destruct /3 width=1 by lsubv_bind/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma index e51a43fdc..c2c939388 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma @@ -13,54 +13,46 @@ (**************************************************************************) include "basic_2/notation/relations/colon_6.ma". -include "basic_2/notation/relations/colon_5.ma". -include "basic_2/notation/relations/colonstar_5.ma". include "basic_2/dynamic/cnv.ma". (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) -definition nta (a) (h): relation4 genv lenv term term ≝ - λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h]. +definition nta (h) (a): relation4 genv lenv term term ≝ + λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![h,a]. interpretation "native type assignment (term)" - 'Colon a h G L T U = (nta a h G L T U). - -interpretation "restricted native type assignment (term)" - 'Colon h G L T U = (nta (ac_eq (S O)) h G L T U). - -interpretation "extended native type assignment (term)" - 'ColonStar h G L T U = (nta ac_top h G L T U). + 'Colon h a G L T U = (nta h a G L T U). (* Basic properties *********************************************************) (* Basic_1: was by definition: ty3_sort *) (* Basic_2A1: was by definition: nta_sort ntaa_sort *) -lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(⫯[h]s). -#a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/ +lemma nta_sort (h) (a) (G) (L): ∀s. ⦃G,L⦄ ⊢ ⋆s :[h,a] ⋆(⫯[h]s). +#h #a #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/ qed. -lemma nta_bind_cnv (a) (h) (G) (K): - ∀V. ⦃G,K⦄ ⊢ V ![a,h] → - ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U → - ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] ⓑ{p,I}V.U. -#a #h #G #K #V #HV #I #T #U #H #p +lemma nta_bind_cnv (h) (a) (G) (K): + ∀V. ⦃G,K⦄ ⊢ V ![h,a] → + ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h,a] U → + ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[h,a] ⓑ{p,I}V.U. +#h #a #G #K #V #HV #I #T #U #H #p elim (cnv_inv_cast … H) -H #X #HU #HT #HUX #HTX /3 width=5 by cnv_bind, cnv_cast, cpms_bind_dx/ qed. (* Basic_2A1: was by definition: nta_cast *) -lemma nta_cast (a) (h) (G) (L): - ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ ⓝU.T :[a,h] U. -#a #h #G #L #T #U #H +lemma nta_cast (h) (a) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ⦃G,L⦄ ⊢ ⓝU.T :[h,a] U. +#h #a #G #L #T #U #H elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX /3 width=3 by cnv_cast, cpms_eps/ qed. (* Basic_1: was by definition: ty3_cast *) -lemma nta_cast_old (a) (h) (G) (L): - ∀T0,T1. ⦃G,L⦄ ⊢ T0 :[a,h] T1 → - ∀T2. ⦃G,L⦄ ⊢ T1 :[a,h] T2 → ⦃G,L⦄ ⊢ ⓝT1.T0 :[a,h] ⓝT2.T1. -#a #h #G #L #T0 #T1 #H1 #T2 #H2 +lemma nta_cast_old (h) (a) (G) (L): + ∀T0,T1. ⦃G,L⦄ ⊢ T0 :[h,a] T1 → + ∀T2. ⦃G,L⦄ ⊢ T1 :[h,a] T2 → ⦃G,L⦄ ⊢ ⓝT1.T0 :[h,a] ⓝT2.T1. +#h #a #G #L #T0 #T1 #H1 #T2 #H2 elim (cnv_inv_cast … H1) #X1 #_ #_ #HTX1 #HTX01 elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12 /3 width=3 by cnv_cast, cpms_eps/ @@ -68,25 +60,25 @@ qed. (* Basic inversion lemmas ***************************************************) -lemma nta_inv_gref_sn (a) (h) (G) (L): - ∀X2,l. ⦃G,L⦄ ⊢ §l :[a,h] X2 → ⊥. -#a #h #G #L #X2 #l #H +lemma nta_inv_gref_sn (h) (a) (G) (L): + ∀X2,l. ⦃G,L⦄ ⊢ §l :[h,a] X2 → ⊥. +#h #a #G #L #X2 #l #H elim (cnv_inv_cast … H) -H #X #_ #H #_ #_ elim (cnv_inv_gref … H) qed-. (* Basic_forward lemmas *****************************************************) -lemma nta_fwd_cnv_sn (a) (h) (G) (L): - ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h]. -#a #h #G #L #T #U #H +lemma nta_fwd_cnv_sn (h) (a) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ⦃G,L⦄ ⊢ T ![h,a]. +#h #a #G #L #T #U #H elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ // qed-. (* Note: this is nta_fwd_correct_cnv *) -lemma nta_fwd_cnv_dx (a) (h) (G) (L): - ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h]. -#a #h #G #L #T #U #H +lemma nta_fwd_cnv_dx (h) (a) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ⦃G,L⦄ ⊢ U ![h,a]. +#h #a #G #L #T #U #H elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma index c27755124..2a3eafa28 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma @@ -20,9 +20,9 @@ include "basic_2/dynamic/nta.ma". (* Forward lemmas with atomic arity assignment for terms ********************) (* Note: this means that no type is a universe *) -lemma nta_fwd_aaa (a) (h) (G) (L): - ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ∃∃A. ⦃G,L⦄ ⊢ T ⁝ A & ⦃G,L⦄ ⊢ U ⁝ A. -#a #h #G #L #T #U #H +lemma nta_fwd_aaa (h) (a) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ∃∃A. ⦃G,L⦄ ⊢ T ⁝ A & ⦃G,L⦄ ⊢ U ⁝ A. +#h #a #G #L #T #U #H elim (cnv_fwd_aaa … H) -H #A #H elim (aaa_inv_cast … H) -H #HU #HT /2 width=3 by ex2_intro/ @@ -31,9 +31,9 @@ qed-. (* Advanced inversion lemmas ************************************************) (* Basic_1: uses: ty3_predicative *) -lemma nta_abst_predicative (a) (h) (p) (G) (L): - ∀W,T. ⦃G,L⦄ ⊢ ⓛ{p}W.T :[a,h] W → ⊥. -#a #h #p #G #L #W #T #H +lemma nta_abst_predicative (h) (a) (p) (G) (L): + ∀W,T. ⦃G,L⦄ ⊢ ⓛ{p}W.T :[h,a] W → ⊥. +#h #a #p #G #L #W #T #H elim (nta_fwd_aaa … H) -a -h #X #H #H1W elim (aaa_inv_abst … H) -p #B #A #H2W #_ #H destruct -T lapply (aaa_mono … H1W … H2W) -G -L -W #H @@ -41,10 +41,10 @@ elim (discr_apair_xy_x … H) qed-. (* Basic_1: uses: ty3_repellent *) -theorem nta_abst_repellent (a) (h) (p) (G) (K): - ∀W,T,U1. ⦃G,K⦄ ⊢ ⓛ{p}W.T :[a,h] U1 → - ∀U2. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U2 → ⬆*[1] U1 ≘ U2 → ⊥. -#a #h #p #G #K #W #T #U1 #H1 #U2 #H2 #HU12 +theorem nta_abst_repellent (h) (a) (p) (G) (K): + ∀W,T,U1. ⦃G,K⦄ ⊢ ⓛ{p}W.T :[h,a] U1 → + ∀U2. ⦃G,K.ⓛW⦄ ⊢ T :[h,a] U2 → ⬆*[1] U1 ≘ U2 → ⊥. +#h #a #p #G #K #W #T #U1 #H1 #U2 #H2 #HU12 elim (nta_fwd_aaa … H2) -H2 #A2 #H2T #H2U2 elim (nta_fwd_aaa … H1) -H1 #X1 #H1 #HU1 elim (aaa_inv_abst … H1) -a -h -p #B #A1 #_ #H1T #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma index d4aec09f3..4e505925c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma @@ -19,10 +19,10 @@ include "basic_2/dynamic/nta.ma". (* Properties with r-equivalence for terms **********************************) -lemma nta_conv_cnv (a) (h) (G) (L) (T): - ∀U1. ⦃G,L⦄ ⊢ T :[a,h] U1 → - ∀U2. ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![a,h] → ⦃G,L⦄ ⊢ T :[a,h] U2. -#a #h #G #L #T #U1 #H1 #U2 #HU12 #HU2 +lemma nta_conv_cnv (h) (a) (G) (L) (T): + ∀U1. ⦃G,L⦄ ⊢ T :[h,a] U1 → + ∀U2. ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![h,a] → ⦃G,L⦄ ⊢ T :[h,a] U2. +#h #a #G #L #T #U1 #H1 #U2 #HU12 #HU2 elim (cnv_inv_cast … H1) -H1 #X1 #HU1 #HT #HUX1 #HTX1 lapply (cpcs_cprs_conf … HUX1 … HU12) -U1 #H elim (cpcs_inv_cprs … H) -H #X2 #HX12 #HU12 @@ -31,11 +31,11 @@ qed-. (* Basic_1: was by definition: ty3_conv *) (* Basic_2A1: was by definition: nta_conv ntaa_conv *) -lemma nta_conv (a) (h) (G) (L) (T): - ∀U1. ⦃G,L⦄ ⊢ T :[a,h] U1 → +lemma nta_conv (h) (a) (G) (L) (T): + ∀U1. ⦃G,L⦄ ⊢ T :[h,a] U1 → ∀U2. ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → - ∀W2. ⦃G,L⦄ ⊢ U2 :[a,h] W2 → ⦃G,L⦄ ⊢ T :[a,h] U2. -#a #h #G #L #T #U1 #H1 #U2 #HU12 #W2 #H2 + ∀W2. ⦃G,L⦄ ⊢ U2 :[h,a] W2 → ⦃G,L⦄ ⊢ T :[h,a] U2. +#h #a #G #L #T #U1 #H1 #U2 #HU12 #W2 #H2 /3 width=3 by nta_conv_cnv, nta_fwd_cnv_sn/ qed-. @@ -43,19 +43,19 @@ qed-. (* Basic_1: was: ty3_gen_sort *) (* Basic_2A1: was: nta_inv_sort1 *) -lemma nta_inv_sort_sn (a) (h) (G) (L) (X2): - ∀s. ⦃G,L⦄ ⊢ ⋆s :[a,h] X2 → - ∧∧ ⦃G,L⦄ ⊢ ⋆(⫯[h]s) ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h]. -#a #h #G #L #X2 #s #H +lemma nta_inv_sort_sn (h) (a) (G) (L) (X2): + ∀s. ⦃G,L⦄ ⊢ ⋆s :[h,a] X2 → + ∧∧ ⦃G,L⦄ ⊢ ⋆(⫯[h]s) ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a]. +#h #a #G #L #X2 #s #H elim (cnv_inv_cast … H) -H #X1 #HX2 #_ #HX21 #H lapply (cpms_inv_sort1 … H) -H #H destruct /3 width=1 by cpcs_cprs_sn, conj/ qed-. -lemma nta_inv_ldec_sn_cnv (a) (h) (G) (K) (V): - ∀X2. ⦃G,K.ⓛV⦄ ⊢ #0 :[a,h] X2 → - ∃∃U. ⦃G,K⦄ ⊢ V ![a,h] & ⬆*[1] V ≘ U & ⦃G,K.ⓛV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓛV⦄ ⊢ X2 ![a,h]. -#a #h #G #Y #X #X2 #H +lemma nta_inv_ldec_sn_cnv (h) (a) (G) (K) (V): + ∀X2. ⦃G,K.ⓛV⦄ ⊢ #0 :[h,a] X2 → + ∃∃U. ⦃G,K⦄ ⊢ V ![h,a] & ⬆*[1] V ≘ U & ⦃G,K.ⓛV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓛV⦄ ⊢ X2 ![h,a]. +#h #a #G #Y #X #X2 #H elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 elim (cnv_inv_zero … H1) -H1 #Z #K #V #HV #H destruct elim (cpms_inv_ell_sn … H2) -H2 * diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma index afe3079de..f45290268 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma @@ -21,11 +21,11 @@ include "basic_2/dynamic/nta.ma". (* Properties with advanced rt_computation for terms ************************) (* Basic_2A1: uses by definition nta_appl ntaa_appl *) -lemma nta_appl_abst (a) (h) (p) (G) (L): - ∀n. appl a n → - ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W → - ∀T,U. ⦃G,L.ⓛW⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U. -#a #h #p #G #L #n #Ha #V #W #H1 #T #U #H2 +lemma nta_appl_abst (h) (a) (p) (G) (L): + ∀n. ad a n → + ∀V,W. ⦃G,L⦄ ⊢ V :[h,a] W → + ∀T,U. ⦃G,L.ⓛW⦄ ⊢ T :[h,a] U → ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T :[h,a] ⓐV.ⓛ{p}W.U. +#h #a #p #G #L #n #Ha #V #W #H1 #T #U #H2 elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1 elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2 /4 width=11 by cnv_appl_ge, cnv_cast, cnv_bind, cpms_appl_dx, cpms_bind_dx/ @@ -33,11 +33,11 @@ qed. (* Basic_1: was by definition: ty3_appl *) (* Basic_2A1: was nta_appl_old *) -lemma nta_appl (a) (h) (p) (G) (L): - ∀n. 1 ≤ n → appl a n → - ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W → - ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[a,h] ⓐV.ⓛ{p}W.U. -#a #h #p #G #L #n #Hn #Ha #V #W #H1 #T #U #H2 +lemma nta_appl (h) (a) (p) (G) (L): + ∀n. 1 ≤ n → ad a n → + ∀V,W. ⦃G,L⦄ ⊢ V :[h,a] W → + ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[h,a] ⓐV.ⓛ{p}W.U. +#h #a #p #G #L #n #Hn #Ha #V #W #H1 #T #U #H2 elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1 elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2 elim (cpms_inv_abst_sn … HUX2) #W0 #U0 #HW0 #HU0 #H destruct @@ -52,10 +52,10 @@ qed. (* Inversion lemmas with advanced rt_computation for terms ******************) -lemma nta_inv_abst_bi_cnv (a) (h) (p) (G) (K) (W): - ∀T,U. ⦃G,K⦄ ⊢ ⓛ{p}W.T :[a,h] ⓛ{p}W.U → - ∧∧ ⦃G,K⦄ ⊢ W ![a,h] & ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U. -#a #h #p #G #K #W #T #U #H +lemma nta_inv_abst_bi_cnv (h) (a) (p) (G) (K) (W): + ∀T,U. ⦃G,K⦄ ⊢ ⓛ{p}W.T :[h,a] ⓛ{p}W.U → + ∧∧ ⦃G,K⦄ ⊢ W ![h,a] & ⦃G,K.ⓛW⦄ ⊢ T :[h,a] U. +#h #a #p #G #K #W #T #U #H elim (cnv_inv_cast … H) -H #X #HWU #HWT #HUX #HTX elim (cnv_inv_bind … HWU) -HWU #HW #HU elim (cnv_inv_bind … HWT) -HWT #_ #HT diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma index b65c1bdc8..29cce8c0c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma @@ -19,10 +19,10 @@ include "basic_2/dynamic/nta.ma". (* Advanced properties ******************************************************) -lemma nta_ldef (a) (h) (G) (K): - ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W → - ∀U. ⬆*[1] W ≘ U → ⦃G,K.ⓓV⦄ ⊢ #0 :[a,h] U. -#a #h #G #K #V #W #H #U #HWU +lemma nta_ldef (h) (a) (G) (K): + ∀V,W. ⦃G,K⦄ ⊢ V :[h,a] W → + ∀U. ⬆*[1] W ≘ U → ⦃G,K.ⓓV⦄ ⊢ #0 :[h,a] U. +#h #a #G #K #V #W #H #U #HWU elim (cnv_inv_cast … H) -H #X #HW #HV #HWX #HVX lapply (cnv_lifts … HW (Ⓣ) … (K.ⓓV) … HWU) -HW [ /3 width=3 by drops_refl, drops_drop/ ] #HU @@ -31,18 +31,18 @@ elim (cpms_lifts_sn … HWX … (Ⓣ) … (K.ⓓV) … HWU) -W /3 width=5 by cnv_zero, cnv_cast, cpms_delta/ qed. -lemma nta_ldec_cnv (a) (h) (G) (K): - ∀W. ⦃G,K⦄ ⊢ W ![a,h] → - ∀U. ⬆*[1] W ≘ U → ⦃G,K.ⓛW⦄ ⊢ #0 :[a,h] U. -#a #h #G #K #W #HW #U #HWU +lemma nta_ldec_cnv (h) (a) (G) (K): + ∀W. ⦃G,K⦄ ⊢ W ![h,a] → + ∀U. ⬆*[1] W ≘ U → ⦃G,K.ⓛW⦄ ⊢ #0 :[h,a] U. +#h #a #G #K #W #HW #U #HWU lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU) /3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/ qed. -lemma nta_lref (a) (h) (I) (G) (K): - ∀T,i. ⦃G,K⦄ ⊢ #i :[a,h] T → - ∀U. ⬆*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #(↑i) :[a,h] U. -#a #h #I #G #K #T #i #H #U #HTU +lemma nta_lref (h) (a) (I) (G) (K): + ∀T,i. ⦃G,K⦄ ⊢ #i :[h,a] T → + ∀U. ⬆*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #(↑i) :[h,a] U. +#h #a #I #G #K #T #i #H #U #HTU elim (cnv_inv_cast … H) -H #X #HT #Hi #HTX #H2 lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ{I}) … HTU) -HT [ /3 width=3 by drops_refl, drops_drop/ ] #HU @@ -55,8 +55,8 @@ qed. (* Properties with generic slicing for local environments *******************) -lemma nta_lifts_sn (a) (h) (G): d_liftable2_sn … lifts (nta a h G). -#a #h #G #K #T1 #T2 #H #b #f #L #HLK #U1 #HTU1 +lemma nta_lifts_sn (h) (a) (G): d_liftable2_sn … lifts (nta a h G). +#h #a #G #K #T1 #T2 #H #b #f #L #HLK #U1 #HTU1 elim (cnv_inv_cast … H) -H #X #HT2 #HT1 #HT2X #HT1X elim (lifts_total T2 f) #U2 #HTU2 lapply (cnv_lifts … HT2 … HLK … HTU2) -HT2 #HU2 @@ -69,23 +69,23 @@ qed-. (* Basic_1: was: ty3_lift *) (* Basic_2A1: was: nta_lift ntaa_lift *) -lemma nta_lifts_bi (a) (h) (G): d_liftable2_bi … lifts (nta a h G). +lemma nta_lifts_bi (h) (a) (G): d_liftable2_bi … lifts (nta a h G). /3 width=12 by nta_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-. (* Basic_1: was by definition: ty3_abbr *) (* Basic_2A1: was by definition: nta_ldef ntaa_ldef *) -lemma nta_ldef_drops (a) (h) (G) (K) (L) (i): - ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W → - ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[a,h] U. -#a #h #G #K #L #i #V #W #HVW #U #HWU #HLK +lemma nta_ldef_drops (h) (a) (G) (K) (L) (i): + ∀V,W. ⦃G,K⦄ ⊢ V :[h,a] W → + ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[h,a] U. +#h #a #G #K #L #i #V #W #HVW #U #HWU #HLK elim (lifts_split_trans … HWU (𝐔❴1❵) (𝐔❴i❵)) [| // ] #X #HWX #HXU /3 width=9 by nta_lifts_bi, nta_ldef/ qed. -lemma nta_ldec_drops_cnv (a) (h) (G) (K) (L) (i): - ∀W. ⦃G,K⦄ ⊢ W ![a,h] → - ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i :[a,h] U. -#a #h #G #K #L #i #W #HW #U #HWU #HLK +lemma nta_ldec_drops_cnv (h) (a) (G) (K) (L) (i): + ∀W. ⦃G,K⦄ ⊢ W ![h,a] → + ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i :[h,a] U. +#h #a #G #K #L #i #W #HW #U #HWU #HLK elim (lifts_split_trans … HWU (𝐔❴1❵) (𝐔❴i❵)) [| // ] #X #HWX #HXU /3 width=9 by nta_lifts_bi, nta_ldec_cnv/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma index 1b58977b0..3a8971fd8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma @@ -19,17 +19,17 @@ include "basic_2/dynamic/nta_preserve.ma". (* Properties with evaluations for rt-transition on terms *******************) -lemma nta_typecheck_dec (a) (h) (G) (L): ac_props a → - ∀T,U. Decidable … (⦃G,L⦄ ⊢ T :[a,h] U). +lemma nta_typecheck_dec (h) (a) (G) (L): ac_props a → + ∀T,U. Decidable … (⦃G,L⦄ ⊢ T :[h,a] U). /2 width=1 by cnv_dec/ qed-. (* Basic_1: uses: ty3_inference *) -lemma nta_inference_dec (a) (h) (G) (L) (T): ac_props a → - ∨∨ ∃U. ⦃G,L⦄ ⊢ T :[a,h] U - | ∀U. (⦃G,L⦄ ⊢ T :[a,h] U → ⊥). -#a #h #G #L #T #Ha -elim (cnv_dec … h G L T Ha) -Ha +lemma nta_inference_dec (h) (a) (G) (L) (T): ac_props a → + Decidable (∃U. ⦃G,L⦄ ⊢ T :[h,a] U). +#h #a #G #L #T #Ha +elim (cnv_dec h … G L T Ha) -Ha #HT [ /3 width=1 by cnv_nta_sn, or_introl/ -| /4 width=2 by nta_fwd_cnv_sn, or_intror/ +| @or_intror * #U #HTU + /3 width=2 by nta_fwd_cnv_sn/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma index a987f760f..5aea50a66 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma @@ -23,10 +23,10 @@ include "basic_2/dynamic/nta.ma". (* Note: this might use fsb_inv_cast (still to be proved) *) (* Basic_1: uses: ty3_sn3 *) (* Basic_2A1: uses: nta_fwd_csn *) -theorem nta_fwd_fsb (a) (h) (G) (L): - ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → +theorem nta_fwd_fsb (h) (a) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ∧∧ ≥[h] 𝐒⦃G,L,T⦄ & ≥[h] 𝐒⦃G,L,U⦄. -#a #h #G #L #T #U #H +#h #a #G #L #T #U #H elim (cnv_inv_cast … H) #X #HU #HT #_ #_ -X /3 width=2 by cnv_fwd_fsb, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma index 5c72abcb9..03ed818b1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma @@ -24,29 +24,29 @@ include "basic_2/dynamic/nta_preserve.ma". lemma nta_ind_rest_cnv (h) (Q:relation4 …): (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) → (∀G,K,V,W,U. - ⦃G,K⦄ ⊢ V :[h] W → ⬆*[1] W ≘ U → + ⦃G,K⦄ ⊢ V :[h,𝟐] W → ⬆*[1] W ≘ U → Q G K V W → Q G (K.ⓓV) (#0) U ) → - (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) → + (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h,𝟐] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) → (∀I,G,K,W,U,i. - ⦃G,K⦄ ⊢ #i :[h] W → ⬆*[1] W ≘ U → + ⦃G,K⦄ ⊢ #i :[h,𝟐] W → ⬆*[1] W ≘ U → Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U ) → (∀p,I,G,K,V,T,U. - ⦃G,K⦄ ⊢ V ![h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h] U → + ⦃G,K⦄ ⊢ V ![h,𝟐] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h,𝟐] U → Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U) ) → (∀p,G,L,V,W,T,U. - ⦃G,L⦄ ⊢ V :[h] W → ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U → + ⦃G,L⦄ ⊢ V :[h,𝟐] W → ⦃G,L⦄ ⊢ T :[h,𝟐] ⓛ{p}W.U → Q G L V W → Q G L T (ⓛ{p}W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U) ) → - (∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h] U → Q G L T U → Q G L (ⓝU.T) U + (∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,𝟐] U → Q G L T U → Q G L (ⓝU.T) U ) → (∀G,L,T,U1,U2. - ⦃G,L⦄ ⊢ T :[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![h] → + ⦃G,L⦄ ⊢ T :[h,𝟐] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![h,𝟐] → Q G L T U1 → Q G L T U2 ) → - ∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h] U → Q G L T U. + ∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,𝟐] U → Q G L T U. #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ] [ #s #HG #HL #HT #X #H destruct -IH @@ -81,33 +81,33 @@ qed-. lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …): (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) → (∀G,K,V,W,U. - ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U → + ⦃G,K⦄ ⊢ V :[h,𝛚] W → ⬆*[1] W ≘ U → Q G K V W → Q G (K.ⓓV) (#0) U ) → - (∀G,K,W,U. ⦃G,K⦄ ⊢ W !*[h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) → + (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h,𝛚] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) → (∀I,G,K,W,U,i. - ⦃G,K⦄ ⊢ #i :*[h] W → ⬆*[1] W ≘ U → + ⦃G,K⦄ ⊢ #i :[h,𝛚] W → ⬆*[1] W ≘ U → Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U ) → (∀p,I,G,K,V,T,U. - ⦃G,K⦄ ⊢ V !*[h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h] U → + ⦃G,K⦄ ⊢ V ![h,𝛚] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h,𝛚] U → Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U) ) → (∀p,G,L,V,W,T,U. - ⦃G,L⦄ ⊢ V :*[h] W → ⦃G,L⦄ ⊢ T :*[h] ⓛ{p}W.U → + ⦃G,L⦄ ⊢ V :[h,𝛚] W → ⦃G,L⦄ ⊢ T :[h,𝛚] ⓛ{p}W.U → Q G L V W → Q G L T (ⓛ{p}W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U) ) → (∀G,L,V,T,U. - ⦃G,L⦄ ⊢ T :*[h] U → ⦃G,L⦄ ⊢ ⓐV.U !*[h] → + ⦃G,L⦄ ⊢ T :[h,𝛚] U → ⦃G,L⦄ ⊢ ⓐV.U ![h,𝛚] → Q G L T U → Q G L (ⓐV.T) (ⓐV.U) ) → - (∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U → Q G L (ⓝU.T) U + (∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U ) → (∀G,L,T,U1,U2. - ⦃G,L⦄ ⊢ T :*[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 !*[h] → + ⦃G,L⦄ ⊢ T :[h,𝛚] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![h,𝛚] → Q G L T U1 → Q G L T U2 ) → - ∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U. + ∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,𝛚] U → Q G L T U. #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ] [ #s #HG #HL #HT #X #H destruct -IH @@ -146,33 +146,33 @@ qed-. lemma nta_ind_ext_cnv (h) (Q:relation4 …): (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) → (∀G,K,V,W,U. - ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U → + ⦃G,K⦄ ⊢ V :[h,𝛚] W → ⬆*[1] W ≘ U → Q G K V W → Q G (K.ⓓV) (#0) U ) → - (∀G,K,W,U. ⦃G,K⦄ ⊢ W !*[h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) → + (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h,𝛚] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) → (∀I,G,K,W,U,i. - ⦃G,K⦄ ⊢ #i :*[h] W → ⬆*[1] W ≘ U → + ⦃G,K⦄ ⊢ #i :[h,𝛚] W → ⬆*[1] W ≘ U → Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U ) → (∀p,I,G,K,V,T,U. - ⦃G,K⦄ ⊢ V !*[h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h] U → + ⦃G,K⦄ ⊢ V ![h,𝛚] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h,𝛚] U → Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U) ) → (∀p,G,K,V,W,T,U. - ⦃G,K⦄ ⊢ V :*[h] W → ⦃G,K.ⓛW⦄ ⊢ T :*[h] U → + ⦃G,K⦄ ⊢ V :[h,𝛚] W → ⦃G,K.ⓛW⦄ ⊢ T :[h,𝛚] U → Q G K V W → Q G (K.ⓛW) T U → Q G K (ⓐV.ⓛ{p}W.T) (ⓐV.ⓛ{p}W.U) ) → (∀G,L,V,T,U. - ⦃G,L⦄ ⊢ T :*[h] U → ⦃G,L⦄ ⊢ ⓐV.U !*[h] → + ⦃G,L⦄ ⊢ T :[h,𝛚] U → ⦃G,L⦄ ⊢ ⓐV.U ![h,𝛚] → Q G L T U → Q G L (ⓐV.T) (ⓐV.U) ) → - (∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U → Q G L (ⓝU.T) U + (∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U ) → (∀G,L,T,U1,U2. - ⦃G,L⦄ ⊢ T :*[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 !*[h] → + ⦃G,L⦄ ⊢ T :[h,𝛚] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![h,𝛚] → Q G L T U1 → Q G L T U2 ) → - ∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U. + ∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,𝛚] U → Q G L T U. #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T #U #H @(nta_ind_ext_cnv_mixed … IH1 IH2 IH3 IH4 IH5 … IH7 IH8 IH9 … H) -G -L -T -U -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9 #p #G #L #V #W #T #U #HVW #HTU #_ #IHTU diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma index 86575032b..de01c6a0d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma @@ -20,31 +20,31 @@ include "basic_2/dynamic/nta.ma". (* Properties based on preservation *****************************************) -lemma cnv_cpms_nta (a) (h) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀U.⦃G,L⦄ ⊢ T ➡*[1,h] U → ⦃G,L⦄ ⊢ T :[a,h] U. +lemma cnv_cpms_nta (h) (a) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀U.⦃G,L⦄ ⊢ T ➡*[1,h] U → ⦃G,L⦄ ⊢ T :[h,a] U. /3 width=4 by cnv_cast, cnv_cpms_trans/ qed. -lemma cnv_nta_sn (a) (h) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T :[a,h] U. -#a #h #G #L #T #HT +lemma cnv_nta_sn (h) (a) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∃U. ⦃G,L⦄ ⊢ T :[h,a] U. +#h #a #G #L #T #HT elim (cnv_fwd_cpm_SO … HT) #U #HTU /4 width=2 by cnv_cpms_nta, cpm_cpms, ex_intro/ qed-. (* Basic_1: was: ty3_typecheck *) -lemma nta_typecheck (a) (h) (G) (L): - ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ∃T0. ⦃G,L⦄ ⊢ ⓝU.T :[a,h] T0. +lemma nta_typecheck (h) (a) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ∃T0. ⦃G,L⦄ ⊢ ⓝU.T :[h,a] T0. /3 width=1 by cnv_cast, cnv_nta_sn/ qed-. (* Basic_1: was: ty3_correct *) (* Basic_2A1: was: ntaa_fwd_correct *) -lemma nta_fwd_correct (a) (h) (G) (L): - ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ∃T0. ⦃G,L⦄ ⊢ U :[a,h] T0. +lemma nta_fwd_correct (h) (a) (G) (L): + ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ∃T0. ⦃G,L⦄ ⊢ U :[h,a] T0. /3 width=2 by nta_fwd_cnv_dx, cnv_nta_sn/ qed-. lemma nta_pure_cnv (h) (G) (L): - ∀T,U. ⦃G,L⦄ ⊢ T :*[h] U → - ∀V. ⦃G,L⦄ ⊢ ⓐV.U !*[h] → ⦃G,L⦄ ⊢ ⓐV.T :*[h] ⓐV.U. + ∀T,U. ⦃G,L⦄ ⊢ T :[h,𝛚] U → + ∀V. ⦃G,L⦄ ⊢ ⓐV.U ![h,𝛚] → ⦃G,L⦄ ⊢ ⓐV.T :[h,𝛚] ⓐV.U. #h #G #L #T #U #H1 #V #H2 elim (cnv_inv_cast … H1) -H1 #X0 #HU #HT #HUX0 #HTX0 elim (cnv_inv_appl … H2) #n #p #X1 #X2 #_ #HV #_ #HVX1 #HUX2 @@ -56,52 +56,52 @@ elim (cpms_inv_abst_sn … H) -H #X3 #X4 #HX13 #HX24 #H destruct qed. (* Basic_1: uses: ty3_sred_wcpr0_pr0 *) -lemma nta_cpr_conf_lpr (a) (h) (G): - ∀L1,T1,U. ⦃G,L1⦄ ⊢ T1 :[a,h] U → ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[h] T2 → - ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T2 :[a,h] U. -#a #h #G #L1 #T1 #U #H #T2 #HT12 #L2 #HL12 +lemma nta_cpr_conf_lpr (h) (a) (G): + ∀L1,T1,U. ⦃G,L1⦄ ⊢ T1 :[h,a] U → ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[h] T2 → + ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T2 :[h,a] U. +#h #a #G #L1 #T1 #U #H #T2 #HT12 #L2 #HL12 /3 width=6 by cnv_cpm_trans_lpr, cpm_cast/ qed-. (* Basic_1: uses: ty3_sred_pr2 ty3_sred_pr0 *) -lemma nta_cpr_conf (a) (h) (G) (L): - ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U → - ∀T2. ⦃G,L⦄ ⊢ T1 ➡[h] T2 → ⦃G,L⦄ ⊢ T2 :[a,h] U. -#a #h #G #L #T1 #U #H #T2 #HT12 +lemma nta_cpr_conf (h) (a) (G) (L): + ∀T1,U. ⦃G,L⦄ ⊢ T1 :[h,a] U → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡[h] T2 → ⦃G,L⦄ ⊢ T2 :[h,a] U. +#h #a #G #L #T1 #U #H #T2 #HT12 /3 width=6 by cnv_cpm_trans, cpm_cast/ qed-. (* Note: this is the preservation property *) (* Basic_1: uses: ty3_sred_pr3 ty3_sred_pr1 *) -lemma nta_cprs_conf (a) (h) (G) (L): - ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U → - ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h] T2 → ⦃G,L⦄ ⊢ T2 :[a,h] U. -#a #h #G #L #T1 #U #H #T2 #HT12 +lemma nta_cprs_conf (h) (a) (G) (L): + ∀T1,U. ⦃G,L⦄ ⊢ T1 :[h,a] U → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h] T2 → ⦃G,L⦄ ⊢ T2 :[h,a] U. +#h #a #G #L #T1 #U #H #T2 #HT12 /3 width=6 by cnv_cpms_trans, cpms_cast/ qed-. (* Basic_1: uses: ty3_cred_pr2 *) -lemma nta_lpr_conf (a) (h) (G): - ∀L1,T,U. ⦃G,L1⦄ ⊢ T :[a,h] U → - ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T :[a,h] U. -#a #h #G #L1 #T #U #HTU #L2 #HL12 +lemma nta_lpr_conf (h) (a) (G): + ∀L1,T,U. ⦃G,L1⦄ ⊢ T :[h,a] U → + ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T :[h,a] U. +#h #a #G #L1 #T #U #HTU #L2 #HL12 /2 width=3 by cnv_lpr_trans/ qed-. (* Basic_1: uses: ty3_cred_pr3 *) -lemma nta_lprs_conf (a) (h) (G): - ∀L1,T,U. ⦃G,L1⦄ ⊢ T :[a,h] U → - ∀L2. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L2⦄ ⊢ T :[a,h] U. -#a #h #G #L1 #T #U #HTU #L2 #HL12 +lemma nta_lprs_conf (h) (a) (G): + ∀L1,T,U. ⦃G,L1⦄ ⊢ T :[h,a] U → + ∀L2. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L2⦄ ⊢ T :[h,a] U. +#h #a #G #L1 #T #U #HTU #L2 #HL12 /2 width=3 by cnv_lprs_trans/ qed-. (* Inversion lemmas based on preservation ***********************************) -lemma nta_inv_ldef_sn (a) (h) (G) (K) (V): - ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 :[a,h] X2 → - ∃∃W,U. ⦃G,K⦄ ⊢ V :[a,h] W & ⬆*[1] W ≘ U & ⦃G,K.ⓓV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓓV⦄ ⊢ X2 ![a,h]. -#a #h #G #Y #X #X2 #H +lemma nta_inv_ldef_sn (h) (a) (G) (K) (V): + ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 :[h,a] X2 → + ∃∃W,U. ⦃G,K⦄ ⊢ V :[h,a] W & ⬆*[1] W ≘ U & ⦃G,K.ⓓV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓓV⦄ ⊢ X2 ![h,a]. +#h #a #G #Y #X #X2 #H elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 elim (cnv_inv_zero … H1) -H1 #Z #K #V #HV #H destruct elim (cpms_inv_delta_sn … H2) -H2 * @@ -111,10 +111,10 @@ elim (cpms_inv_delta_sn … H2) -H2 * ] qed-. -lemma nta_inv_lref_sn (a) (h) (G) (L): - ∀X2,i. ⦃G,L⦄ ⊢ #↑i :[a,h] X2 → - ∃∃I,K,T2,U2. ⦃G,K⦄ ⊢ #i :[a,h] T2 & ⬆*[1] T2 ≘ U2 & ⦃G,K.ⓘ{I}⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,K.ⓘ{I}⦄ ⊢ X2 ![a,h] & L = K.ⓘ{I}. -#a #h #G #L #X2 #i #H +lemma nta_inv_lref_sn (h) (a) (G) (L): + ∀X2,i. ⦃G,L⦄ ⊢ #↑i :[h,a] X2 → + ∃∃I,K,T2,U2. ⦃G,K⦄ ⊢ #i :[h,a] T2 & ⬆*[1] T2 ≘ U2 & ⦃G,K.ⓘ{I}⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,K.ⓘ{I}⦄ ⊢ X2 ![h,a] & L = K.ⓘ{I}. +#h #a #G #L #X2 #i #H elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 elim (cnv_inv_lref … H1) -H1 #I #K #Hi #H destruct elim (cpms_inv_lref_sn … H2) -H2 * @@ -124,11 +124,11 @@ elim (cpms_inv_lref_sn … H2) -H2 * ] qed-. -lemma nta_inv_lref_sn_drops_cnv (a) (h) (G) (L): - ∀X2,i. ⦃G,L⦄ ⊢ #i :[a,h] X2 → - ∨∨ ∃∃K,V,W,U. ⬇*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V :[a,h] W & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h] - | ∃∃K,W,U. ⬇*[i] L ≘ K. ⓛW & ⦃G,K⦄ ⊢ W ![a,h] & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h]. -#a #h #G #L #X2 #i #H +lemma nta_inv_lref_sn_drops_cnv (h) (a) (G) (L): + ∀X2,i. ⦃G,L⦄ ⊢ #i :[h,a] X2 → + ∨∨ ∃∃K,V,W,U. ⬇*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V :[h,a] W & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a] + | ∃∃K,W,U. ⬇*[i] L ≘ K. ⓛW & ⦃G,K⦄ ⊢ W ![h,a] & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a]. +#h #a #G #L #X2 #i #H elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 elim (cnv_inv_lref_drops … H1) -H1 #I #K #V #HLK #HV elim (cpms_inv_lref1_drops … H2) -H2 * @@ -145,10 +145,10 @@ elim (cpms_inv_lref1_drops … H2) -H2 * ] qed-. -lemma nta_inv_bind_sn_cnv (a) (h) (p) (I) (G) (K) (X2): - ∀V,T. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] X2 → - ∃∃U. ⦃G,K⦄ ⊢ V ![a,h] & ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U & ⦃G,K⦄ ⊢ ⓑ{p,I}V.U ⬌*[h] X2 & ⦃G,K⦄ ⊢ X2 ![a,h]. -#a #h #p * #G #K #X2 #V #T #H +lemma nta_inv_bind_sn_cnv (h) (a) (p) (I) (G) (K) (X2): + ∀V,T. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[h,a] X2 → + ∃∃U. ⦃G,K⦄ ⊢ V ![h,a] & ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h,a] U & ⦃G,K⦄ ⊢ ⓑ{p,I}V.U ⬌*[h] X2 & ⦃G,K⦄ ⊢ X2 ![h,a]. +#h #a #p * #G #K #X2 #V #T #H elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 elim (cnv_inv_bind … H1) -H1 #HV #HT [ elim (cpms_inv_abbr_sn_dx … H2) -H2 * @@ -164,8 +164,8 @@ qed-. (* Basic_1: uses: ty3_gen_appl *) lemma nta_inv_appl_sn (h) (G) (L) (X2): - ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :[h] X2 → - ∃∃p,W,U. ⦃G,L⦄ ⊢ V :[h] W & ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h]. + ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :[h,𝟐] X2 → + ∃∃p,W,U. ⦃G,L⦄ ⊢ V :[h,𝟐] W & ⦃G,L⦄ ⊢ T :[h,𝟐] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,𝟐]. #h #G #L #X2 #V #T #H elim (cnv_inv_cast … H) -H #X #HX2 #H1 #HX2 #H2 elim (cnv_inv_appl … H1) #n #p #W #U #H (plus_minus_m_m_commutative … Hn) in HTU0; #H + elim (cpms_inv_plus … H) -H #U #HTU #HU0 + lapply (cpms_appl_dx … V V … HTU) [ // ] #H + elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H (plus_minus_m_m_commutative … Hnm) in HTU0; #H + elim (cpms_inv_plus … H) -H #U #HTU #HU0 + lapply (cpms_appl_dx … V V … HTU) [ // ] #H + elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H