From cacd7323994f7621286dbfd93bbf4c50acfbe918 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 19 Aug 2019 23:31:18 +0200 Subject: [PATCH] still more additions and corrections for the article + one theorem was missing + some renaming --- .../lambdadelta/basic_2/dynamic/cnv.ma | 68 +++++++----- .../lambdadelta/basic_2/dynamic/cnv_aaa.ma | 2 +- .../lambdadelta/basic_2/dynamic/cnv_cpes.ma | 2 +- .../basic_2/dynamic/cnv_cpm_conf.ma | 8 +- .../basic_2/dynamic/cnv_cpm_tdeq.ma | 83 +++++++------- .../basic_2/dynamic/cnv_cpm_trans.ma | 8 +- .../lambdadelta/basic_2/dynamic/cnv_cpme.ma | 10 ++ .../basic_2/dynamic/cnv_cpms_conf.ma | 18 +-- .../lambdadelta/basic_2/dynamic/cnv_drops.ma | 20 ++-- .../lambdadelta/basic_2/dynamic/cnv_fqus.ma | 20 ++-- .../lambdadelta/basic_2/dynamic/cnv_fsb.ma | 11 +- .../basic_2/dynamic/cnv_preserve.ma | 4 +- .../basic_2/dynamic/cnv_preserve_sub.ma | 18 +-- .../lambdadelta/basic_2/dynamic/lsubv.ma | 56 +++++----- .../lambdadelta/basic_2/dynamic/lsubv_cnv.ma | 4 +- .../lambdadelta/basic_2/dynamic/lsubv_cpms.ma | 3 +- .../basic_2/dynamic/lsubv_drops.ma | 12 +- .../lambdadelta/basic_2/dynamic/nta.ma | 4 +- .../lambdadelta/basic_2/dynamic/nta_aaa.ma | 2 +- .../basic_2/dynamic/nta_preserve.ma | 6 +- .../basic_2/rt_computation/fsb_aaa.ma | 1 - .../basic_2/rt_transition/rpx_rdeq.ma | 8 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 4 +- .../lambdadelta/ground_2/lib/relations.ma | 103 ++++++++++-------- 24 files changed, 259 insertions(+), 216 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma index 0fa415ae4..962b6d775 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma @@ -44,8 +44,9 @@ interpretation "context-sensitive extended native validity (term)" (* 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. +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 [ #G #L #s #H destruct | #I #G #K #V #HV #_ /2 width=5 by ex2_3_intro/ @@ -56,12 +57,14 @@ fact cnv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → X = #0 → ] 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 (a) (h): + ∀G,L. ⦃G,L⦄ ⊢ #0 ![a,h] → + ∃∃I,K,V. ⦃G,K⦄ ⊢ V ![a,h] & 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}. +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 [ #G #L #s #j #H destruct | #I #G #K #V #_ #j #H destruct @@ -72,8 +75,9 @@ fact cnv_inv_lref_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀i. X = #( ] 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 (a) (h): + ∀G,L,i. ⦃G,L⦄ ⊢ #↑i ![a,h] → + ∃∃I,K. ⦃G,K⦄ ⊢ #i ![a,h] & 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 → ⊥. @@ -91,10 +95,10 @@ qed-. lemma cnv_inv_gref (a) (h): ∀G,L,l. ⦃G,L⦄ ⊢ §l ![a,h] → ⊥. /2 width=8 by cnv_inv_gref_aux/ qed-. -fact cnv_inv_bind_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → - ∀p,I,V,T. X = ⓑ{p,I}V.T → - ∧∧ ⦃G,L⦄ ⊢ V ![a,h] - & ⦃G,L.ⓑ{I}V⦄ ⊢ T ![a,h]. +fact cnv_inv_bind_aux (a) (h): + ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → + ∀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 #s #q #Z #X1 #X2 #H destruct | #I #G #K #V #_ #q #Z #X1 #X2 #H destruct @@ -106,14 +110,15 @@ fact cnv_inv_bind_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![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 (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]. /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. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & - ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0. +fact cnv_inv_appl_aux (a) (h): + ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀V,T. X = ⓐV.T → + ∃∃n,p,W0,U0. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & + ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0. #a #h #G #L #X * -L -X [ #G #L #s #X1 #X2 #H destruct | #I #G #K #V #_ #X1 #X2 #H destruct @@ -125,14 +130,16 @@ fact cnv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀V,T. X = 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. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & - ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0. +lemma cnv_inv_appl (a) (h): + ∀G,L,V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → + ∃∃n,p,W0,U0. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & + ⦃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] & - ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[1,h] U0. +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] & + ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[1,h] U0. #a #h #G #L #X * -G -L -X [ #G #L #s #X1 #X2 #H destruct | #I #G #K #V #_ #X1 #X2 #H destruct @@ -143,17 +150,18 @@ fact cnv_inv_cast_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀U,T. X = ] qed-. -(* Basic_2A1: uses: snv_inv_appl *) -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] & - ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[1,h] U0. +(* 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] & + ⦃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]. + ∀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 [ elim (cnv_inv_appl … H) #n #p #W #U #_ #HV #HT #_ #_ | elim (cnv_inv_cast … H) #U #HV #HT #_ #_ 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 aa0c10865..c7735d20c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma @@ -66,7 +66,7 @@ qed-. lemma cnv_inv_appl_pred (a) (h) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] → ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & - ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W0.U0. + ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W0.U0. #a #h #G #L #V #T #H elim (cnv_inv_appl … H) -H #n #p #W #U #Ha #HV #HT #HVW #HTU lapply (ylt_inv_inj … Ha) -Ha #Ha 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 190165fe6..e0775c021 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma @@ -48,7 +48,7 @@ qed-. lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] → ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & - ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W.U. + ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W.U. #a #h #G #L #V #T #H elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU /3 width=7 by cpms_div, ex4_3_intro/ 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 c10e470dd..56e5ffd9b 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 @@ -387,10 +387,10 @@ elim (cnv_cpm_conf_lpr_sub … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 w qed-. fact cnv_cpm_conf_lpr_aux (a) (h): - ∀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. + ∀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 * [| * [| * ]] [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct elim (cpm_inv_atom1_drops … HX1) -HX1 * 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 e3057788c..e8f59293c 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 @@ -23,8 +23,7 @@ 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. + ∀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 [ // | #G #K #V1 #V2 #X2 #_ #_ #_ #H1 #_ -a -G -K -V1 -V2 @@ -55,9 +54,9 @@ 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] → - ∀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. + ∀V,T1. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] → + ∀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 elim (cpm_inv_bind1 … H1) -H1 * [ #XV #T2 #HXV #HT12 #H destruct @@ -73,10 +72,10 @@ 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] → - ∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛ X → - ∃∃m,q,W,U1,T2. yinj m < a & ⦃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. + ∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![a,h] → + ∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛ X → + ∃∃m,q,W,U1,T2. yinj m < a & ⦃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 elim (cpm_inv_appl1 … H1) -H1 * [ #XV #T2 #HXV #HT12 #H destruct @@ -92,11 +91,11 @@ 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] → - ∀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. + ∀U1,T1. ⦃G,L⦄ ⊢ ⓝU1.T1 ![a,h] → + ∀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 elim (cpm_inv_cast1 … H1) -H1 [ * || * ] [ #U2 #T2 #HU12 #HT12 #H destruct @@ -115,9 +114,9 @@ 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] → - ∀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. + ∀X. ⦃G,L⦄ ⊢ X ![a,h] → + ∀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 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 @@ -127,25 +126,25 @@ qed-. (* Eliminators with restricted rt-transition for terms **********************) lemma cpm_tdeq_ind (a) (h) (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] → - ∀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. yinj m < a → - ∀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] → - ∀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 → - Q L U1 U2 → Q L T1 T2 → Q L (ⓝU1.T1) (ⓝU2.T2) - ) → - ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] → - ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → Q L T1 T2. + (∀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] → + ∀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. yinj m < a → + ∀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] → + ∀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 → + Q L U1 U2 → Q L T1 T2 → Q L (ⓝU1.T1) (ⓝU2.T2) + ) → + ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀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 @(insert_eq_0 … G) #F @(fqup_wf_ind_eq (Ⓣ) … F L T1) -L -T1 -F @@ -170,9 +169,9 @@ qed-. (* Advanced properties with restricted rt-transition for terms **************) lemma cpm_tdeq_free (a) (h) (n) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → - ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → - ∀F,K. ⦃F,K⦄ ⊢ T1 ➡[n,h] T2. + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀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 @(cpm_tdeq_ind … H0 … H1 H2) -L -T1 -T2 [ #I #L #H #F #K destruct // @@ -189,9 +188,9 @@ 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] → - ∀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. + ∀V,T1. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] → + ∀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 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/ 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 21f0e500c..3b4b54740 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 @@ -24,10 +24,10 @@ 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): - ∀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. + ∀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 * * [|||| * ] [ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1 elim (cpm_inv_sort1 … H2) -H2 #H #_ destruct // 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 be0443bca..a9091b059 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma @@ -35,3 +35,13 @@ 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,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ∀m21,m22. - ∀X2. ⦃G0,L0⦄ ⊢ X1 ➡[m21,h] X2 → (X1 ≛ X2 → ⊥) → - ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → - ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-m12,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m12-(m21+m22),h]T + (∀G,L,T. ⦃G0,L0,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → + ∀m21,m22. + ∀X2. ⦃G0,L0⦄ ⊢ X1 ➡[m21,h] X2 → (X1 ≛ X2 → ⊥) → + ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → + ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → + ∃∃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 @@ -147,9 +147,9 @@ 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. + (∀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) → + ∀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 #HT0 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 destruct elim (tdeq_dec T0 T1) #H2T01 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 9483346c4..71e115777 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma @@ -20,8 +20,9 @@ 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]. +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 [ #L #HV #H lapply (drops_fwd_isid … H ?) -H // #H destruct @@ -36,8 +37,8 @@ qed. (* 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]. + ∀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 [ #L #H elim (cnv_inv_zero … H) -H #I #K #V #HV #H destruct @@ -50,16 +51,15 @@ 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]. + ∀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 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 ≘ ⋆ → ⊥. + ∀i,L. ⦃G,L⦄ ⊢ #i ![a,h] → ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⊥. #a #h #b #G #i #L #H #Hi elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #_ lapply (drops_gen b … HLY) -HLY #HLY @@ -67,8 +67,8 @@ lapply (drops_mono … HLY … Hi) -L #H destruct qed-. lemma cnv_inv_lref_unit (a) (h) (G): - ∀i,L. ⦃G,L⦄ ⊢ #i ![a,h] → - ∀I,K. ⬇*[i] L ≘ K.ⓤ{I} → ⊥. + ∀i,L. ⦃G,L⦄ ⊢ #i ![a,h] → + ∀I,K. ⬇*[i] L ≘ K.ⓤ{I} → ⊥. #a #h #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 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 fbac6d7f7..1c30ccce1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma @@ -20,8 +20,9 @@ include "basic_2/dynamic/cnv_drops.ma". (* Properties with supclosure ***********************************************) (* Basic_2A1: uses: snv_fqu_conf *) -lemma cnv_fqu_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂ ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h]. +lemma cnv_fqu_conf (a) (h): + ∀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 [ #I1 #G1 #L1 #V1 #H elim (cnv_inv_zero … H) -H #I2 #L2 #V2 #HV2 #H destruct // @@ -43,22 +44,25 @@ lemma cnv_fqu_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂ ⦃G2,L2,T2 qed-. (* Basic_2A1: uses: snv_fquq_conf *) -lemma cnv_fquq_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮ ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h]. +lemma cnv_fquq_conf (a) (h): + ∀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 [|*] /2 width=5 by cnv_fqu_conf/ qed-. (* Basic_2A1: uses: snv_fqup_conf *) -lemma cnv_fqup_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂+ ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h]. +lemma cnv_fqup_conf (a) (h): + ∀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 /3 width=5 by fqup_strap1, cnv_fqu_conf/ qed-. (* Basic_2A1: uses: snv_fqus_conf *) -lemma cnv_fqus_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂* ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h]. +lemma cnv_fqus_conf (a) (h): + ∀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 [|*] /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 bf6732dab..7f754d97f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma @@ -19,20 +19,23 @@ include "basic_2/dynamic/cnv_aaa.ma". (* Forward lemmas with strongly rst-normalizing closures ********************) +(* 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⦄. +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/ 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⦄. +lemma cnv_fwd_csx (a) (h): + ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. #a #h #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 (a) (h): + ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃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 483ea690e..178a2b846 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma @@ -20,8 +20,8 @@ include "basic_2/dynamic/cnv_cpms_conf.ma". (* 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. + ∧∧ 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 lapply (cnv_fwd_fsb … HT) -HT #H @(fsb_ind_fpbg … H) -G -L -T #G #L #T #_ #IH diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma index 2eedc2889..244f82718 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma @@ -50,22 +50,22 @@ definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝ (* Auxiliary properties for preservation ************************************) fact cnv_cpms_trans_lpr_sub (a) (h): - ∀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_trans_lpr a h G1 L1 T1. + ∀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_trans_lpr a h G1 L1 T1. #a #h #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): - ∀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. + ∀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. /3 width=8 by cpm_cpms/ qed-. fact cnv_cpms_strip_lpr_sub (a) (h): - ∀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. + ∀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. /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 17a22da58..fdf2ad803 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma @@ -30,7 +30,8 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact lsubv_inv_atom_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 = ⋆ → L2 = ⋆. +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 [ // | #I #L1 #L2 #_ #H destruct @@ -39,15 +40,15 @@ fact lsubv_inv_atom_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 = 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 (a) (h) (G): + ∀L2. G ⊢ ⋆ ⫃![a,h] 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 → - ∀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 & - I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW. + ∀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 + & I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW. #a #h #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/ @@ -56,14 +57,15 @@ 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 & - I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW. +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 + & 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 = ⋆. +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 [ // | #I #L1 #L2 #_ #H destruct @@ -72,14 +74,16 @@ fact lsubv_inv_atom_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 = qed-. (* Basic_2A1: uses: lsubsv_inv_atom2 *) -lemma lsubv_inv_atom2 (a) (h) (G): ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → L1 = ⋆. +lemma lsubv_inv_atom2 (a) (h) (G): + ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → 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 → - ∀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. +fact lsubv_inv_bind_dx_aux (a) (h) (G): + ∀L1,L2. G ⊢ L1 ⫃![a,h] 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 [ #J #K2 #H destruct | #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or_introl/ @@ -88,16 +92,18 @@ fact lsubv_inv_bind_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → 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 (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. /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. +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 elim (lsubv_inv_bind_sn … H) -H // * #K2 #XW #XV #_ #_ #H1 #H2 destruct 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 e5c87b05f..271b5d5b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma @@ -20,8 +20,8 @@ include "basic_2/dynamic/lsubv_cpms.ma". (* 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]. + ∀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 // [ #I #G #K2 #V #HV #IH #L1 #H elim (lsubv_inv_bind_dx … H) -H * /3 width=1 by cnv_zero/ 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 81d385add..ba08f8818 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma @@ -20,6 +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 (a) (n) (h) (G): + lsub_trans … (λL. cpms h G L n) (lsubv a h 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 06d302d57..63b53ec72 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma @@ -22,9 +22,9 @@ 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 → - ∀b,f,K1. 𝐔⦃f⦄ → ⬇*[b,f] L1 ≘ K1 → - ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L2 ≘ K2. + ∀L1,L2. G ⊢ L1 ⫃![a,h] 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 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #HL12 #IH #b #f #K1 #Hf #H @@ -47,9 +47,9 @@ 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 → - ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2 → - ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L1 ≘ K1. + ∀L1,L2. G ⊢ L1 ⫃![a,h] 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 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #HL12 #IH #b #f #K2 #Hf #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma index 84bbfeda9..187370fab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma @@ -78,14 +78,14 @@ 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]. + ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h]. #a #h #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]. + ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h]. #a #h #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 0161996dd..c27755124 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_aaa.ma @@ -40,7 +40,7 @@ lapply (aaa_mono … H1W … H2W) -G -L -W #H elim (discr_apair_xy_x … H) qed-. -(* Basic_2A1: uses: ty3_repellent *) +(* 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 → ⊥. 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 ebc6fd96d..ec8f6bfea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma @@ -174,9 +174,9 @@ qed-. (* Basic_2A1: uses: nta_fwd_pure1 *) lemma nta_inv_pure_sn_cnv (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] - | ∃∃U. ⦃G,L⦄ ⊢ T :*[h] U & ⦃G,L⦄ ⊢ ⓐV.U !*[h] & ⦃G,L⦄ ⊢ ⓐV.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] + | ∃∃U. ⦃G,L⦄ ⊢ T :*[h] U & ⦃G,L⦄ ⊢ ⓐV.U !*[h] & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h]. #h #G #L #X2 #V #T #H elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H elim (cnv_inv_appl … H1) * [| #n ] #p #W0 #T0 #Hn #HV #HT #HW0 #HT0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma index 7ea1776a0..b95c6ced6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma @@ -21,7 +21,6 @@ include "basic_2/rt_computation/fsb_csx.ma". (* Main properties with atomic arity assignment for terms *******************) -(* Note: this is the "big tree" theorem *) theorem aaa_fsb: ∀h,G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ≥[h] 𝐒⦃G,L,T⦄. /3 width=2 by aaa_csx, csx_fsb/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma index 602285337..b8117c047 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma @@ -44,7 +44,7 @@ lemma rpx_tdeq_div: ∀h,T1,T2. T1 ≛ T2 → ∀G,L1,L2. ⦃G,L1⦄ ⊢ ⬈[h,T2] L2 → ⦃G,L1⦄ ⊢ ⬈[h,T1] L2. /2 width=5 by tdeq_rex_div/ qed-. -lemma cpx_tdeq_conf_sex: ∀h,G. R_confluent2_rex … (cpx h G) cdeq (cpx h G) cdeq. +lemma cpx_tdeq_conf_rex: ∀h,G. R_confluent2_rex … (cpx h G) cdeq (cpx h G) cdeq. #h #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/ [ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02 elim (tdeq_inv_sort1 … H0) -H0 #s1 #H destruct @@ -129,7 +129,7 @@ lemma cpx_tdeq_conf: ∀h,G,L. ∀T0:term. ∀T1. ⦃G,L⦄ ⊢ T0 ⬈[h] T1 → ∀T2. T0 ≛ T2 → ∃∃T. T1 ≛ T & ⦃G,L⦄ ⊢ T2 ⬈[h] T. #h #G #L #T0 #T1 #HT01 #T2 #HT02 -elim (cpx_tdeq_conf_sex … HT01 … HT02 L … L) -HT01 -HT02 +elim (cpx_tdeq_conf_rex … HT01 … HT02 L … L) -HT01 -HT02 /2 width=3 by rex_refl, ex2_intro/ qed-. @@ -145,7 +145,7 @@ lemma cpx_rdeq_conf: ∀h,G,L0,T0,T1. ⦃G,L0⦄ ⊢ T0 ⬈[h] T1 → ∀L2. L0 ≛[T0] L2 → ∃∃T. ⦃G,L2⦄ ⊢ T0 ⬈[h] T & T1 ≛ T. #h #G #L0 #T0 #T1 #HT01 #L2 #HL02 -elim (cpx_tdeq_conf_sex … HT01 T0 … L0 … HL02) -HT01 -HL02 +elim (cpx_tdeq_conf_rex … HT01 T0 … L0 … HL02) -HT01 -HL02 /2 width=3 by rex_refl, ex2_intro/ qed-. @@ -159,7 +159,7 @@ elim (cpx_rdeq_conf … HT01 L2) -HT01 qed-. lemma rpx_rdeq_conf: ∀h,G,T. confluent2 … (rpx h G T) (rdeq T). -/3 width=6 by rpx_fsge_comp, rdeq_fsge_comp, cpx_tdeq_conf_sex, rex_conf/ qed-. +/3 width=6 by rpx_fsge_comp, rdeq_fsge_comp, cpx_tdeq_conf_rex, rex_conf/ qed-. lemma rdeq_rpx_trans: ∀h,G,T,L2,K2. ⦃G,L2⦄ ⊢ ⬈[h,T] K2 → ∀L1. L1 ≛[T] L2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index bf8f10608..be3c16d73 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -29,10 +29,10 @@ Stage "B" Parametrized applicability condition - allows λδ-2B to generalize both λδ-1A and λδ-1B. + allows λδ-2B to generalize both λδ-2A and λδ-1B. - Extended (λδ-2A) and restricted (λδ-1A) validity is decidable + Extended (λδ-2A) and restricted (λδ-1B) validity is decidable (anniversary milestone). diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma index fa8bae343..d272c0dbe 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma @@ -18,7 +18,7 @@ include "ground_2/lib/logic.ma". (* GENERIC RELATIONS ********************************************************) definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝ - λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2. + λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2. (* Inclusion ****************************************************************) @@ -36,81 +36,93 @@ interpretation "3-relation inclusion" (* Properties of relations **************************************************) -definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] -≝ λA,B,C,D,E.A→B→C→D→E→Prop. +definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝ + λA,B,C,D,E.A→B→C→D→E→Prop. -definition relation6: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] -≝ λA,B,C,D,E,F.A→B→C→D→E→F→Prop. +definition relation6: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝ + λA,B,C,D,E,F.A→B→C→D→E→F→Prop. -(**) (* we dont use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *) +(**) (* we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *) definition c_reflexive (A) (B): predicate (relation3 A B B) ≝ - λR. ∀a,b. R a b b. + λR. ∀a,b. R a b b. definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥). -definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R. - ∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2. +definition Transitive (A) (R:relation A): Prop ≝ + ∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2. -definition left_cancellable: ∀A. ∀R: relation A. Prop ≝ λA,R. - ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 → R a1 a2. +definition left_cancellable (A) (R:relation A): Prop ≝ + ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 → R a1 a2. -definition right_cancellable: ∀A. ∀R: relation A. Prop ≝ λA,R. - ∀a1,a0. R a1 a0 → ∀a2. R a2 a0 → R a1 a2. +definition right_cancellable (A) (R:relation A): Prop ≝ + ∀a1,a0. R a1 a0 → ∀a2. R a2 a0 → R a1 a2. -definition pw_confluent2: ∀A. relation A → relation A → predicate A ≝ λA,R1,R2,a0. - ∀a1. R1 a0 a1 → ∀a2. R2 a0 a2 → - ∃∃a. R2 a1 a & R1 a2 a. +definition pw_confluent2 (A) (R1,R2:relation A): predicate A ≝ + λa0. + ∀a1. R1 a0 a1 → ∀a2. R2 a0 a2 → + ∃∃a. R2 a1 a & R1 a2 a. -definition confluent2: ∀A. relation (relation A) ≝ λA,R1,R2. - ∀a0. pw_confluent2 A R1 R2 a0. +definition confluent2 (A): relation (relation A) ≝ + λR1,R2. + ∀a0. pw_confluent2 A R1 R2 a0. -definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. - ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 → - ∃∃a. R2 a1 a & R1 a a2. +definition transitive2 (A) (R1,R2:relation A): Prop ≝ + ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 → + ∃∃a. R2 a1 a & R1 a a2. -definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. - ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 → - ∃∃a,b. R a1 b1 a b & R a2 b2 a b. +definition bi_confluent (A) (B) (R: bi_relation A B): Prop ≝ + ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 → + ∃∃a,b. R a1 b1 a b & R a2 b2 a b. -definition lsub_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. - ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 T1 T2. +definition lsub_trans (A) (B): relation2 (A→relation B) (relation A) ≝ + λR1,R2. + ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 T1 T2. -definition s_r_confluent1: ∀A,B. relation2 (A→relation B) (B→relation A) ≝ λA,B,R1,R2. - ∀L1,T1,T2. R1 L1 T1 T2 → ∀L2. R2 T1 L1 L2 → R2 T2 L1 L2. +definition s_r_confluent1 (A) (B): relation2 (A→relation B) (B→relation A) ≝ + λR1,R2. + ∀L1,T1,T2. R1 L1 T1 T2 → ∀L2. R2 T1 L1 L2 → R2 T2 L1 L2. -definition is_mono: ∀B:Type[0]. predicate (predicate B) ≝ - λB,R. ∀b1. R b1 → ∀b2. R b2 → b1 = b2. +definition is_mono (B:Type[0]): predicate (predicate B) ≝ + λR. ∀b1. R b1 → ∀b2. R b2 → b1 = b2. -definition is_inj2: ∀A,B:Type[0]. predicate (relation2 A B) ≝ - λA,B,R. ∀a1,b. R a1 b → ∀a2. R a2 b → a1 = a2. +definition is_inj2 (A,B:Type[0]): predicate (relation2 A B) ≝ + λR. ∀a1,b. R a1 b → ∀a2. R a2 b → a1 = a2. + +(* Main properties of equality **********************************************) + +theorem canc_sn_eq (A): left_cancellable A (eq …). +// qed-. + +theorem canc_dx_eq (A): right_cancellable A (eq …). +// qed-. (* Normal form and strong normalization *************************************) -definition NF: ∀A. relation A → relation A → predicate A ≝ - λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2. +definition NF (A): relation A → relation A → predicate A ≝ + λR,S,a1. ∀a2. R a1 a2 → S a1 a2. -definition NF_dec: ∀A. relation A → relation A → Prop ≝ - λA,R,S. ∀a1. NF A R S a1 ∨ - ∃∃a2. R … a1 a2 & (S a1 a2 → ⊥). +definition NF_dec (A): relation A → relation A → Prop ≝ + λR,S. ∀a1. NF A R S a1 ∨ + ∃∃a2. R … a1 a2 & (S a1 a2 → ⊥). inductive SN (A) (R,S:relation A): predicate A ≝ | SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → ⊥) → SN A R S a2) → SN A R S a1 . -lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a. +lemma NF_to_SN (A) (R) (S): ∀a. NF A R S a → SN A R S a. #A #R #S #a1 #Ha1 @SN_intro #a2 #HRa12 #HSa12 elim HSa12 -HSa12 /2 width=1 by/ qed. -definition NF_sn: ∀A. relation A → relation A → predicate A ≝ - λA,R,S,a2. ∀a1. R a1 a2 → S a1 a2. +definition NF_sn (A): relation A → relation A → predicate A ≝ + λR,S,a2. ∀a1. R a1 a2 → S a1 a2. inductive SN_sn (A) (R,S:relation A): predicate A ≝ | SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a1 a2 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2 . -lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a. +lemma NF_to_SN_sn (A) (R) (S): ∀a. NF_sn A R S a → SN_sn A R S a. #A #R #S #a2 #Ha2 @SN_sn_intro #a1 #HRa12 #HSa12 elim HSa12 -HSa12 /2 width=1 by/ @@ -118,9 +130,10 @@ qed. (* Relations on unboxed triples *********************************************) -definition tri_RC: ∀A,B,C. tri_relation A B C → tri_relation A B C ≝ - λA,B,C,R,a1,b1,c1,a2,b2,c2. R … a1 b1 c1 a2 b2 c2 ∨ - ∧∧ a1 = a2 & b1 = b2 & c1 = c2. +definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝ + λR,a1,b1,c1,a2,b2,c2. + ∨∨ R … a1 b1 c1 a2 b2 c2 + | ∧∧ a1 = a2 & b1 = b2 & c1 = c2. -lemma tri_RC_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_RC … R). +lemma tri_RC_reflexive (A) (B) (C): ∀R. tri_reflexive A B C (tri_RC … R). /3 width=1 by and3_intro, or_intror/ qed. -- 2.39.2