From 0e16720654c6667b94433e91dddc3c53b904e200 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 8 Nov 2018 17:32:40 +0100 Subject: [PATCH] update in basic_2 and in web site + updates on cpce an related concepts + "versions" table updated for web site --- helm/www/lambdadelta/web/home/versions.tbl | 20 ++++---- .../cnv_lpce.ma => etc/cpce/cnv_cpce.etc} | 21 ++++---- .../lambdadelta/basic_2/etc/cpce/cnv_lpce.etc | 51 +++++++++++++++++++ .../lambdadelta/basic_2/etc/cpce/cpce_lpr.etc | 42 +++++++++++++++ .../lambdadelta/basic_2/rt_conversion/cpce.ma | 23 ++++----- .../rt_conversion/cpce_ext.ma} | 18 +++---- .../lambdadelta/basic_2/rt_conversion/lpce.ma | 19 ++++++- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 8 +-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 1 + .../ground_2/notation/xoa/ex_2_4.ma | 26 ---------- .../lambdadelta/ground_2/xoa2.conf.xml | 1 - 11 files changed, 154 insertions(+), 76 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/cnv_lpce.ma => etc/cpce/cnv_cpce.etc} (69%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_lpr.etc rename matita/matita/contribs/lambdadelta/{ground_2/xoa/ex_2_4.ma => basic_2/rt_conversion/cpce_ext.ma} (68%) delete mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_2_4.ma diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl index cb3c4f99e..0d84b3b1f 100644 --- a/helm/www/lambdadelta/web/home/versions.tbl +++ b/helm/www/lambdadelta/web/home/versions.tbl @@ -16,27 +16,29 @@ table { class "orange" { [ { @@("html/specification#v2" "Version 2") * } { "\"basic_2\"" * } - { [ "\"A2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.3") - "October 2015" "" "" "" + { [ "\"B\"" @("http://matita.cs.unibo.it/" "Matita 0.99.3") + "October 2015" "November 2018" "" "" "" * ] - [ "\"A1\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2") + [ "\"A\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2") "April 2011" "June 2014" "October 2014" "August 2015" @@("html/documentation#ldV2a" "V2a") + " " + @@("html/documentation#ldR2c" "R2c") * ] } ] [ "Abandoned" "" - "" @("http://coq.inria.fr/" "Coq 7.3.1") - "March 2008" "" "" "February 2011" - "" * + [ "" @("http://coq.inria.fr/" "Coq 7.3.1") + "March 2008" "" "" "February 2011" + "" * + ] ] } class "red" [ @@("html/specification#v1" "Version 1") "\"basic_1\"" - "" @("http://coq.inria.fr/" "Coq 7.3.1") - "May 2004" "December 2005" "November 2006" "May 2008" - @@("html/documentation#ldV1a" "V1a") + " " + @@("html/documentation#ldJ1a" "J1a") * + [ "\"A\"" @("http://coq.inria.fr/" "Coq 7.3.1") + "May 2004" "December 2005" "November 2006" "May 2008" + @@("html/documentation#ldV1a" "V1a") + " " + @@("html/documentation#ldJ1a" "J1a") * + ] ] } diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce.etc similarity index 69% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce.etc index 61d4bf476..5c3b02334 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce.etc @@ -12,15 +12,18 @@ (* *) (**************************************************************************) -include "basic_2/rt_conversion/lpce.ma". -include "basic_2/dynamic/cnv.ma". +include "basic_2/rt_conversion/cpce.ma". +include "basic_2/dynamic/cnv_preserve.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -theorem cnv_cpce_trans_lpce (h) (G): - ∀L1,T1,T2. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T2 → ⦃G,L1⦄ ⊢ T1 !*[h] → - ∀L2. ⦃G,L1⦄ ⊢ ⬌η[h] L2 → ⦃G,L2⦄ ⊢ T2 !*[h]. -#h #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -[ #G #L1 #s #_ #L2 #_ // -| #G #K1 #V1 #_ #Y2 #HY - elim (lpce_inv_pair_sn … HY) -HY #K2 #V2 #HK #HV #H destruct \ No newline at end of file +theorem cnv_cpce_mono (a) (h) (G) (L) (T): + ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ⦃G,L⦄ ⊢ T ![a,h] → + ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T @(fqup_wf_ind (Ⓣ) … G L T) -G -L -T +#G0 #L0 #T0 #IH #T1 +@(insert_eq_0 … G0) #G +@(insert_eq_0 … L0) #L +@(insert_eq_0 … T0) #T +* -G -L -T +[ #G #L1 #s #_ #_ #_ #_ #L2 #_ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc new file mode 100644 index 000000000..0e84ad097 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/s_computation/fqup_weight.ma". +include "basic_2/rt_conversion/lpce.ma". +include "basic_2/dynamic/cnv_drops.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +theorem cnv_cpce_trans_lpce (h) (G): + ∀L1,T1,T2. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T2 → ⦃G,L1⦄ ⊢ T1 !*[h] → + ∀L2. ⦃G,L1⦄ ⊢ ⬌η[h] L2 → ⦃G,L2⦄ ⊢ T2 !*[h]. +#h #G #L1 #T1 @(fqup_wf_ind (Ⓣ) … G L1 T1) -G -L1 -T1 +#G0 #L0 #T0 #IH #T2 +@(insert_eq_0 … G0) #G +@(insert_eq_0 … L0) #L1 +@(insert_eq_0 … T0) #T1 +* -G -L1 -T1 +[ #G #L1 #s #_ #_ #_ #_ #L2 #_ // +| #G #K1 #V1 #HT #HL #HG #H0 #Y2 #HY2 destruct + elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct + elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct + /4 width=6 by cnv_zero, fqu_fqup, fqu_lref_O/ +| #n #G #K1 #V1 #s #_ #HT #HL #HG #H0 #Y2 #HY2 destruct + elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct + elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct + /4 width=6 by cnv_zero, fqu_fqup, fqu_lref_O/ +| #n #p #G #K1 #V1 #W1 #W2 #T1 #HVT1 #HW12 #HT #HL #HG #H0 #Y2 #HY2 destruct + elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct + elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct +| #I #G #K1 #T1 #U1 #i #H0 #HTU1 #HT #HL #HG #H0 #Y2 #HY2 destruct + elim (cnv_inv_lref … H0) -H0 #Z1 #Y1 #Hi #H destruct + elim (lpce_inv_bind_sn … HY2) -HY2 #Z2 #K2 #HK12 #_ #H destruct + @(cnv_lifts … K2 … (Ⓣ) … HTU1) [| /3 width=1 by drops_refl, drops_drop/ ] -U1 + /3 width=6 by fqu_fqup/ +| #p #I #G #K1 #V1 #V2 #T1 #T2 #HV12 #HT12 #HT #HL #HG #H0 #K2 #HK12 destruct + elim (cnv_inv_bind … H0) -H0 #HV1 #HT1 + /4 width=8 by lpce_pair, cnv_bind/ +| * #G #L1 #V1 #V2 #T1 #T2 #HV12 #HT12 #HT #HL #HG #H0 #L2 #HK12 destruct + \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_lpr.etc new file mode 100644 index 000000000..f0a3a1534 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_lpr.etc @@ -0,0 +1,42 @@ +include "basic_2/rt_transition/lpr.ma". +include "basic_2/rt_conversion/lpce.ma". +include "basic_2/dynamic/cnv_preserve.ma". + +lemma cpce_cpm_conf_lpce_lpr (a) (h) (n) (G): + ∀L1,T1. ⦃G,L1⦄ ⊢ T1 ![a,h] → + ∀U1. ⦃G,L1⦄ ⊢ T1 ⬌η[h] U1 → ∀K1. ⦃G,L1⦄ ⊢ ⬌η[h] K1 → + ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[n,h] T2 → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → + ∃∃K2,U2. ⦃G,K1⦄ ⊢ ➡[h] K2 & ⦃G,L2⦄ ⊢ ⬌η[h] K2 & ⦃G,K2⦄ ⊢ U1 ➡[n,h] U2 & ⦃G,L2⦄ ⊢ T2 ⬌η[h] U2. +#a #h #n #G #L1 #T1 #HT1 +letin o ≝ (sd_O h) +lapply (cnv_fwd_fsb … o … HT1) -HT1 #H +@(fsb_ind_fpbg … H) -G -L1 -T1 #G #L1 #T1 #_ #IH +#U1 + +#H elim H -G -L1 -T1 -U1 +[ #G #L1 elim L1 -L1 [| #L1 #I1 #IH ] #s #K1 #HLK1 #X2 #HX2 #Y2 #HY2 + elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn destruct + [ lapply (lpr_inv_atom_sn … HY2) -HY2 #H destruct + lapply (lpce_inv_atom_sn … HLK1) -HLK1 #H destruct + /3 width=6 by cpce_sort, cpm_sort, ex4_2_intro/ + | elim (lpr_inv_bind_sn … HY2) -HY2 #I2 #L2 #HL12 #HI12 #H destruct + elim (lpce_inv_bind_sn … HLK1) -HLK1 #J1 #K0 #HLK1 #HIJ1 #H destruct + elim (IH s ? HLK1 (⋆((next h)^n s)) … HL12) -IH -HLK1 -HL12 + [| /2 width=1 by cpm_sort/ ] #K2 #U2 #HK12 #HLK2 #H1s #H2s + +| #G #L1 #s elim L1 -L1 + [ #Y2 #HY2 #X2 #HX2 #K1 #HLK1 + lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct + /3 width=6 by cpce_sort, ex4_2_intro/ + | #L1 #I1 #IH #Y2 #HY2 #X2 #HX2 #K1 #HLK1 + lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct + + +| #n #G #K1 #V1 #V2 #X1 #HV12 #_ #HX1 #X2 #HX2 #Y2 #HY2 + elim (lpr_inv_pair_sn … HY2) -HY2 #K2 #W1 #HK12 #HVW1 #H destruct + lapply (cpce_inv_ldef_sn … HX2) -HX2 #H destruct + elim (lifts_total W1 (𝐔❴1❵)) #X2 #HX2 + @(ex2_intro … X2) [ @(cpm_delta … HX2) /3 width=5 by _/ + + /3 width=3 by cpce_ldef, ex2_intro/ + | \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma index b9d162530..259fc7b07 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/xoa/ex_2_4.ma". include "basic_2/notation/relations/pconveta_5.ma". include "basic_2/rt_computation/cpms.ma". @@ -24,8 +23,8 @@ inductive cpce (h): relation4 genv lenv term term ≝ | cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0) | cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s → cpce h G (K.ⓛV) (#0) (#0) -| cpce_eta : ∀n,p,G,K,V,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T → - cpce h G (K.ⓛV) (#0) (+ⓛW.ⓐ#0.#1) +| cpce_eta : ∀n,p,G,K,V,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T → + cpce h G K W1 W2 → cpce h G (K.ⓛV) (#0) (+ⓛW2.ⓐ#0.#1) | cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T → ⬆*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U | cpce_bind: ∀p,I,G,K,V1,V2,T1,T2. @@ -37,8 +36,8 @@ inductive cpce (h): relation4 genv lenv term term ≝ . interpretation - "context-sensitive parallel eta-conversion (term)" - 'PConvEta h G L T1 T2 = (cpce h G L T1 T2). + "context-sensitive parallel eta-conversion (term)" + 'PConvEta h G L T1 T2 = (cpce h G L T1 T2). (* Basic inversion lemmas ***************************************************) @@ -49,7 +48,7 @@ lemma cpce_inv_sort_sn (h) (G) (L) (X2): [ #G #L #s #_ // | #G #K #V #_ // | #n #G #K #V #s #_ #_ // -| #n #p #G #K #V #W #T #_ #H destruct +| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H destruct | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct @@ -65,7 +64,7 @@ lemma cpce_inv_ldef_sn (h) (G) (K) (X2): [ #G #L #s #_ #_ // | #G #K #V #_ #_ // | #n #G #K #V #s #_ #_ #_ // -| #n #p #G #K #V #W #T #_ #_ #H destruct +| #n #p #G #K #V #W1 #W2 #T #_ #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H #_ destruct | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct @@ -75,7 +74,7 @@ qed-. lemma cpce_inv_ldec_sn (h) (G) (K) (X2): ∀V. ⦃G,K.ⓛV⦄ ⊢ #0 ⬌η[h] X2 → ∨∨ ∃∃n,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s & #0 = X2 - | ∃∃n,p,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T & +ⓛW.ⓐ#0.#1 = X2. + | ∃∃n,p,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T & ⦃G,K⦄ ⊢ W1 ⬌η[h] W2 & +ⓛW2.ⓐ#0.#1 = X2. #h #G #Y #X2 #X @(insert_eq_0 … (Y.ⓛX)) #Y1 @(insert_eq_0 … (#0)) #X1 @@ -83,7 +82,7 @@ lemma cpce_inv_ldec_sn (h) (G) (K) (X2): [ #G #L #s #H #_ destruct | #G #K #V #_ #H destruct | #n #G #K #V #s #HV #_ #H destruct /3 width=3 by ex2_2_intro, or_introl/ -| #n #p #G #K #V #W #T #HV #_ #H destruct /3 width=6 by or_intror, ex2_4_intro/ +| #n #p #G #K #V #W1 #W2 #T #HV #HW #_ #H destruct /3 width=8 by ex3_5_intro, or_intror/ | #I #G #K #T #U #i #_ #_ #H #_ destruct | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct @@ -100,7 +99,7 @@ lemma cpce_inv_lref_sn (h) (G) (K) (X2): [ #G #L #s #H #_ destruct | #G #K #V #H #_ destruct | #n #G #K #V #s #_ #H #_ destruct -| #n #p #G #K #V #W #T #_ #H #_ destruct +| #n #p #G #K #V #W1 #W2 #T #_ #_ #H #_ destruct | #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/ | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct @@ -115,7 +114,7 @@ lemma cpce_inv_bind_sn (h) (G) (K) (X2): [ #G #L #s #H destruct | #G #K #V #H destruct | #n #G #K #V #s #_ #H destruct -| #n #p #G #K #V #W #T #_ #H destruct +| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H destruct | #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/ | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct @@ -130,7 +129,7 @@ lemma cpce_inv_flat_sn (h) (G) (L) (X2): [ #G #L #s #H destruct | #G #K #V #H destruct | #n #G #K #V #s #_ #H destruct -| #n #p #G #K #V #W #T #_ #H destruct +| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H destruct | #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct | #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_ext.ma similarity index 68% rename from matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_ext.ma index af891c071..5596e40a5 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_ext.ma @@ -12,17 +12,13 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +include "static_2/syntax/cext2.ma". +include "basic_2/rt_conversion/cpce.ma". -include "basics/pts.ma". +(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR BINDERS ********************) -include "ground_2/notation/xoa/ex_2_4.ma". - -(* multiple existental quantifier (2, 4) *) - -inductive ex2_4 (A0,A1,A2,A3:Type[0]) (P0,P1:A0→A1→A2→A3→Prop) : Prop ≝ - | ex2_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → ex2_4 ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (2, 4)" 'Ex4 P0 P1 = (ex2_4 ? ? ? ? P0 P1). +definition cpce_ext (h) (G): relation3 lenv bind bind ≝ cext2 (cpce h G). +interpretation + "context-sensitive parallel eta-conversion (binder)" + 'PConvEta h G L I1 I2 = (cpce_ext h G L I1 I2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma index 8aca0e26b..b74313dae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma @@ -14,7 +14,7 @@ include "static_2/relocation/lex.ma". include "basic_2/notation/relations/pconveta_4.ma". -include "basic_2/rt_conversion/cpce.ma". +include "basic_2/rt_conversion/cpce_ext.ma". (* PARALLEL ETA-CONVERSION FOR FULL LOCAL ENVIRONMENTS **********************) @@ -24,6 +24,13 @@ interpretation "parallel eta-conversion on all entries (local environment)" 'PConvEta h G L1 L2 = (lpce h G L1 L2). +(* Basic properties *********************************************************) + +lemma lpce_bind (h) (G): + ∀K1,K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 → + ∀I1,I2. ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 → ⦃G,K1.ⓘ{I1}⦄ ⊢ ⬌η[h] K2.ⓘ{I2}. +/2 width=1 by lex_bind/ qed. + (* Advanced properties ******************************************************) lemma lpce_pair (h) (G): @@ -37,10 +44,20 @@ lemma lpce_inv_atom_sn (h) (G): ∀L2. ⦃G,⋆⦄ ⊢ ⬌η[h] L2 → L2 = ⋆. /2 width=2 by lex_inv_atom_sn/ qed-. +lemma lpce_inv_bind_sn (h) (G): + ∀I1,L2,K1. ⦃G,K1.ⓘ{I1}⦄ ⊢ ⬌η[h] L2 → + ∃∃I2,K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 & L2 = K2.ⓘ{I2}. +/2 width=1 by lex_inv_bind_sn/ qed-. + lemma lpce_inv_atom_dx (h) (G): ∀L1. ⦃G,L1⦄ ⊢ ⬌η[h] ⋆ → L1 = ⋆. /2 width=2 by lex_inv_atom_dx/ qed-. +lemma lpce_inv_bind_dx (h) (G): + ∀I2,L1,K2. ⦃G,L1⦄ ⊢ ⬌η[h] K2.ⓘ{I2} → + ∃∃I1,K1. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 & L1 = K1.ⓘ{I1}. +/2 width=1 by lex_inv_bind_dx/ qed-. + (* Advanced inversion lemmas ************************************************) lemma lpce_inv_unit_sn (h) (G): 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 3aff8e423..66fb5e30c 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 @@ -27,13 +27,7 @@ Stage "B" - - + Extended (λδ-2) and restricted (λδ-1) type rules justified. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 8cd2fd30f..850588ce1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -42,6 +42,7 @@ table { [ { "rt-conversion" * } { [ { "context-sensitive parallel eta-conversion" * } { [ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" * ] + [ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ] [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_2_4.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_2_4.ma deleted file mode 100644 index b4f405729..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_2_4.ma +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was generated by xoa.native: do not edit *********************) - -(* multiple existental quantifier (2, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) }. - diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml index 149052483..d40726d02 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml @@ -5,7 +5,6 @@ ground_2/xoa ground_2/notation/xoa basics/pts.ma - 2 4 5 1 5 7 9 3 -- 2.39.2