From: Ferruccio Guidi Date: Mon, 6 Mar 2017 22:20:11 +0000 (+0000) Subject: - advances on lfxs for lfpxs X-Git-Tag: make_still_working~491 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10b733131aa2667d8ba4318d517f0ba3cf137359;p=helm.git - advances on lfxs for lfpxs - ex_cpr_omega (2-steps loop) --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma new file mode 100644 index 000000000..0bbe88b88 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpr.ma". + +(* EXAMPLES *****************************************************************) + +(* A reduction cycle in two steps: the term Omega ***************************) + +definition Delta: term → term ≝ λW. +ⓛW.ⓐ#0.#0. + +definition Omega1: term → term ≝ λW. ⓐ(Delta W).(Delta W). + +definition Omega2: term → term ≝ λW. +ⓓⓝW.(Delta W).ⓐ#0.#0. + +(* Basic properties *********************************************************) + +lemma Delta_lifts: ∀W1,W2,f. ⬆*[f] W1 ≡ W2 → + ⬆*[f] (Delta W1) ≡ (Delta W2). +/4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed. + +(* Main properties **********************************************************) + +theorem cpr_Omega_12: ∀h,G,L,W. ⦃G, L⦄ ⊢ Omega1 W ➡[h] Omega2 W. +/2 width=1 by cpm_beta/ qed. + +theorem cpr_Omega_21: ∀h,G,L,W. ⦃G, L⦄ ⊢ Omega2 W ➡[h] Omega1 W. +#h #G #L #W1 elim (lifts_total W1 (𝐔❴1❵)) +/5 width=5 by lifts_flat, cpm_zeta, cpm_eps, cpm_appl, cpm_delta, Delta_lifts/ +qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma new file mode 100644 index 000000000..e37f8831f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/fpbg_fpbs.ma". + +(* EXAMPLES *****************************************************************) + +(* Reflexivity of proper qrst-computation: the term ApplOmega ***************) + +definition ApplDelta: term → nat → term ≝ λW,s. +ⓛW.ⓐ⋆s.ⓐ#0.#0. + +definition ApplOmega1: term → nat → term ≝ λW,s. ⓐ(ApplDelta W s).(ApplDelta W s). + +definition ApplOmega2: term → nat → term ≝ λW,s. +ⓓⓝW.(ApplDelta W s).ⓐ⋆s.ⓐ#0.#0. + +definition ApplOmega3: term → nat → term ≝ λW,s. ⓐ⋆s.(ApplOmega1 W s). + +(* Basic properties *********************************************************) + +lemma ApplDelta_lift: ∀W1,W2,s,l,k. ⬆[l, k] W1 ≡ W2 → + ⬆[l, k] (ApplDelta W1 s) ≡ (ApplDelta W2 s). +/5 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed. + +lemma cpr_ApplOmega_12: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡ ApplOmega2 W s. +/2 width=1 by cpr_beta/ qed. + +lemma cpr_ApplOmega_23: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega2 W s ➡ ApplOmega3 W s. +#G #L #W1 #s elim (lift_total W1 0 1) #W2 #HW12 +@(cpr_zeta … (ApplOmega3 W2 s)) /4 width=1 by ApplDelta_lift, lift_flat/ +@cpr_flat // @cpr_flat @(cpr_delta … (ApplDelta W1 s) ? 0) +[3,5,8,10: /2 width=2 by ApplDelta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ] +qed. + +lemma cpxs_ApplOmega_13: ∀h,o,G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡*[h,o] ApplOmega3 W s. +/4 width=3 by cpxs_strap1, cpr_cpx/ qed. + +lemma fqup_ApplOmega_13: ∀G,L,W,s. ⦃G, L, ApplOmega3 W s⦄ ⊐+ ⦃G, L, ApplOmega1 W s⦄. +/2 width=1 by/ qed. + +(* Main properties **********************************************************) + +theorem fpbg_refl: ∀h,o,G,L,W,s. ⦃G, L, ApplOmega1 W s⦄ >≡[h,o] ⦃G, L, ApplOmega1 W s⦄. +/3 width=5 by fpbs_fpbg_trans, fqup_fpbg, cpxs_fpbs/ qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma new file mode 100644 index 000000000..af66f2c97 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/dynamic/snv.ma". + +(* EXAMPLES *****************************************************************) + +(* Extended validy (basic?_2) vs. restricted validity (basic_1) *************) + +(* extended validity of a closure, last arg of snv_appl > 1 *) +lemma snv_extended: ∀h,o,a,G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{a}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ¡[h, o]. +#h #o #a #G #L #s elim (deg_total h o s) +#d #Hd @(snv_appl … a … (⋆s) … (⋆s) (0+1+1)) +[ /4 width=5 by snv_lref, drop_drop_lt/ +| /4 width=13 by snv_bind, snv_lref/ +| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/ +| @(lstas_scpds … (d+1+1)) + /5 width=11 by lstas_bind, lstas_succ, da_bind, da_ldec, da_sort, lift_bind/ +] +qed. + +(* restricted validity of the η-expanded closure, last arg of snv_appl = 1 **) +lemma snv_restricted: ∀h,o,a,G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{a}⋆s.⋆s.ⓛⓛ{a}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ¡[h, o]. +#h #o #a #G #L #s elim (deg_total h o s) +#d #Hd @(snv_appl … a … (⋆s) … (ⓐ#0.#2) (0+1)) +[ /4 width=5 by snv_lref, drop_drop_lt/ +| @snv_lref [4: // |1,2,3: skip ] + @snv_bind // + @(snv_appl … a … (⋆s) … (⋆s) (0+1)) + [ @snv_lref [4: // |1,2,3: skip ] // + | @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind // + | @(lstas_scpds … (d+1)) /3 width=6 by da_sort, da_ldec, lstas_succ/ + | @(lstas_scpds … (d+1)) /3 width=8 by lstas_succ, lstas_bind, drop_drop, lift_bind/ + @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] /3 width=1 by da_sort, da_bind/ + ] +| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/ +| @(lstas_scpds … (d+1+1)) // + [ @da_ldec [3: // |1,2: skip ] + @da_bind @da_flat @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] + /3 width=1 by da_sort, da_bind/ + | @lstas_succ [4: // |1,2: skip ] + [2: @lstas_bind | skip ] + [2: @lstas_appl | skip ] + [2: @lstas_zero + [4: /2 width=1 by drop_drop_lt/ |5: /2 width=2 by lstas_bind/ |*: skip ] + |1: skip ] + /4 width=2 by lift_flat, lift_bind, lift_lref_ge_minus, lift_lref_lt/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_sta_ldec.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_sta_ldec.ma new file mode 100644 index 000000000..260430451 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_sta_ldec.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/unfold/lstas.ma". + +(* EXAMPLES *****************************************************************) + +(* Static type assignment (iterated vs primitive): the declared variable ****) + +(* basic_1: we have "L.ⓛⓝ⋆k1.⋆k2⦄ ⊢ #0 • ⓝ⋆k1.⋆k2". *) +theorem sta_ldec: ∀h,G,L,s1,s2. ⦃G, L.ⓛⓝ⋆s1.⋆s2⦄ ⊢ #0 •*[h, 1] ⋆s2. +/3 width=6 by lstas_sort, lstas_succ, lstas_cast, drop_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 9a19a7715..d43a58823 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -10,7 +10,7 @@ table { } ] (* - class "orange" + class "yellow" [ { "MLTT1" * } { [ { "" * } { [ "genv_primitive" "judgment" * ] @@ -19,7 +19,7 @@ table { } ] *) - class "red" + class "orange" [ { "functional" * } { [ { "reduction and type machine" * } { [ "rtm" "rtm_step ( ? ⇨ ? )" * ] @@ -31,6 +31,14 @@ table { ] } ] + class "red" + [ { "examples" * } { + [ { "terms with special features" * } { + [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" + "ex_snv_eta" * ] + } + ] + } + ] } class "top" { * } diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc index 89e1466f7..ada873d81 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc @@ -7,8 +7,7 @@ lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ cpr_cpx/ qed. -lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] -𝐍⦃T⦄ → T = U. +lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → T = U. #h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T // #T0 #T #H1T0 #_ #IHT #H2T0 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs.etc deleted file mode 100644 index f09a2cfc2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs.etc +++ /dev/null @@ -1,264 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground_2/relocation/rtmap_id.ma". -include "basic_2/notation/relations/relationstar_4.ma". -include "basic_2/relocation/lexs.ma". -include "basic_2/static/frees.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -definition lfxs (R) (T): relation lenv ≝ - λL1,L2. ∃∃f. L1 ⊢ 𝐅*⦃T⦄ ≡ f & L1 ⦻*[R, cfull, f] L2. - -interpretation "generic extension on referred entries (local environment)" - 'RelationStar R T L1 L2 = (lfxs R T L1 L2). - -definition R_frees_confluent: predicate (relation3 lenv term term) ≝ - λRN. - ∀f1,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀T2. RN L T1 T2 → - ∃∃f2. L ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. - -definition lexs_frees_confluent: relation (relation3 lenv term term) ≝ - λRN,RP. - ∀f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → - ∀L2. L1 ⦻*[RN, RP, f1] L2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. - -definition R_confluent2_lfxs: relation4 (relation3 lenv term term) - (relation3 lenv term term) … ≝ - λR1,R2,RP1,RP2. - ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. - -(* Basic properties ***********************************************************) - -lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆. -/3 width=3 by lexs_atom, frees_atom, ex2_intro/ -qed. - -lemma lfxs_sort: ∀R,I,L1,L2,V1,V2,s. - L1 ⦻*[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻*[R, ⋆s] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #s * /3 width=3 by lexs_push, frees_sort, ex2_intro/ -qed. - -lemma lfxs_zero: ∀R,I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 → - R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, #0] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 * /3 width=3 by lexs_next, frees_zero, ex2_intro/ -qed. - -lemma lfxs_lref: ∀R,I,L1,L2,V1,V2,i. - L1 ⦻*[R, #i] L2 → L1.ⓑ{I}V1 ⦻*[R, #⫯i] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ -qed. - -lemma lfxs_gref: ∀R,I,L1,L2,V1,V2,l. - L1 ⦻*[R, §l] L2 → L1.ⓑ{I}V1 ⦻*[R, §l] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #l * /3 width=3 by lexs_push, frees_gref, ex2_intro/ -qed. - -lemma lfxs_pair_repl_dx: ∀R,I,L1,L2,T,V,V1. - L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V1 → - ∀V2. R L1 V V2 → - L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V2. -#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR -/3 width=5 by lexs_pair_repl, ex2_intro/ -qed-. - -lemma lfxs_sym: ∀R. lexs_frees_confluent R cfull → - (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀T. symmetric … (lfxs R T). -#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1 -/4 width=5 by sle_lexs_trans, lexs_sym, ex2_intro/ -qed-. - -lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → - ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2. -#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. -#R #I #Y2 * /2 width=4 by lexs_inv_atom1/ -qed-. - -lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. -#R #I #Y1 * /2 width=4 by lexs_inv_atom2/ -qed-. - -lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2 -[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ -| lapply (frees_inv_sort … H1) -H1 #Hf - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct - elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct - /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/ -] -qed-. - -lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * -[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ -| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg - /4 width=9 by ex4_5_intro, ex2_intro, or_intror/ -] -qed-. - -lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * -[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ -| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg - /4 width=8 by ex3_5_intro, ex2_intro, or_intror/ -] -qed-. - -lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2 -[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ -| lapply (frees_inv_gref … H1) -H1 #Hf - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct - elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct - /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/ -] -qed-. - -lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → - L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. -#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf -/6 width=6 by sle_lexs_trans, lexs_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ -qed-. - -lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → - L1 ⦻*[R, V] L2 ∧ L1 ⦻*[R, T] L2. -#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf -/5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ -qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 → - ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → - ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & - Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct - /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & - Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct - /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 → - ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 → - ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. -#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf -/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ -qed-. - -lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → - R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. -#R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV // -qed-. - -lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2. -#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // -qed-. - -lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, T] L2. -#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // -qed-. - -lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. -#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ -qed-. - -(* Basic_2A1: removed theorems 24: - llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref - llpx_sn_bind llpx_sn_flat - llpx_sn_inv_bind llpx_sn_inv_flat - llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length - llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx - llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co - llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc deleted file mode 100644 index 0a3f287bb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc +++ /dev/null @@ -1,93 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/drops_ceq.ma". -include "basic_2/relocation/drops_lexs.ma". -include "basic_2/static/frees_drops.ma". -include "basic_2/static/lfxs.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -definition dedropable_sn: predicate (relation3 lenv term term) ≝ - λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → - ∀K2,T. K1 ⦻*[R, T] K2 → ∀U. ⬆*[f] T ≡ U → - ∃∃L2. L1 ⦻*[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. - -definition dropable_sn: predicate (relation3 lenv term term) ≝ - λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ → - ∀L2,U. L1 ⦻*[R, U] L2 → ∀T. ⬆*[f] T ≡ U → - ∃∃K2. K1 ⦻*[R, T] K2 & ⬇*[b, f] L2 ≡ K2. - -definition dropable_dx: predicate (relation3 lenv term term) ≝ - λR. ∀L1,L2,U. L1 ⦻*[R, U] L2 → - ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U → - ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[R, T] K2. - -(* Properties with generic slicing for local environments *******************) - -(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *) -lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → - d_liftable2 R → dedropable_sn R. -#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU -elim (frees_total L1 U) #f2 #Hf2 -lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf -elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1 -/3 width=6 by cfull_lift, ex3_intro, ex2_intro/ -qed-. - -(* Inversion lemmas with generic slicing for local environments *************) - -(* Basic_2A1: restricts: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *) -(* Basic_2A1: was: llpx_sn_drop_conf_O *) -lemma lfxs_dropable_sn: ∀R. dropable_sn R. -#R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU -elim (frees_total K1 T) #f1 #Hf1 -lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #H2f -elim (lexs_co_dropable_sn … HLK1 … HL12 … H2f) -f2 -L1 -/3 width=3 by ex2_intro/ -qed-. - -(* Basic_2A1: was: llpx_sn_drop_trans_O *) -(* Note: the proof might be simplified *) -lemma lfxs_dropable_dx: ∀R. dropable_dx R. -#R #L1 #L2 #U * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #H1f #T #HTU -elim (drops_isuni_ex … H1f L1) #K1 #HLK1 -elim (frees_total K1 T) #f1 #Hf1 -lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -K1 #H2f -elim (lexs_co_dropable_dx … HL12 … HLK2 … H2f) -L2 -/4 width=9 by frees_inv_lifts, ex2_intro/ -qed-. - -(* Basic_2A1: was: llpx_sn_inv_lift_O *) -lemma lfxs_inv_lift_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 → - ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → - ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2. -#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU -elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY -lapply (drops_mono … HY … HLK2) -L2 -i #H destruct // -qed-. - -lemma lfxs_inv_lref_sn: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[R, V1] K2 & R K1 V1 V2. -#R #L1 #L2 #i #HL12 #I #K1 #V1 #HLK1 elim (lfxs_dropable_sn … HLK1 … HL12 (#0)) -HLK1 -HL12 // -#Y #HY #HLK2 elim (lfxs_inv_zero_pair_sn … HY) -HY -#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ -qed-. - -lemma lfxs_inv_lref_dx: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[R, V1] K2 & R K1 V1 V2. -#R #L1 #L2 #i #HL12 #I #K2 #V2 #HLK2 elim (lfxs_dropable_dx … HL12 … HLK2 … (#0)) -HLK2 -HL12 // -#Y #HLK1 #HY elim (lfxs_inv_zero_pair_dx … HY) -HY -#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_fqup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_fqup.etc deleted file mode 100644 index 62c5b0564..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_fqup.etc +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/frees_fqup.ma". -include "basic_2/static/lfxs.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -(* Advanced properties ******************************************************) - -lemma lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀L,T. L ⦻*[R, T] L. -#R #HR #L #T elim (frees_total L T) /3 width=3 by lexs_refl, ex2_intro/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_length.etc deleted file mode 100644 index 01dd82cf4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_length.etc +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/lexs_length.ma". -include "basic_2/static/lfxs.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -(* Forward lemmas with length for local environments ************************) - -lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⦻*[R, T] L2 → |L1| = |L2|. -#R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc index 307740bea..4ca71664c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc @@ -1,41 +1,3 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/lexs_lexs.ma". -include "basic_2/static/frees_fqup.ma". -include "basic_2/static/frees_frees.ma". -include "basic_2/static/lfxs.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -(* Main properties **********************************************************) - -theorem lfxs_bind: ∀R,p,I,L1,L2,V1,V2,T. - L1 ⦻*[R, V1] L2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2 → - L1 ⦻*[R, ⓑ{p,I}V1.T] L2. -#R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 -elim (lexs_fwd_pair … Hf2) -Hf2 #Hf2 #_ elim (sor_isfin_ex f1 (⫱f2)) -/3 width=7 by frees_fwd_isfin, frees_bind, lexs_join, isfin_tl, ex2_intro/ -qed. - -theorem lfxs_flat: ∀R,I,L1,L2,V,T. - L1 ⦻*[R, V] L2 → L1 ⦻*[R, T] L2 → - L1 ⦻*[R, ⓕ{I}V.T] L2. -#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) -/3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ -qed. - theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull → ∀T. Transitive … (lfxs R T). #R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 @@ -47,24 +9,3 @@ lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1 /4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/ qed-. - -theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull → - R_confluent2_lfxs R R R R → - ∀T. confluent … (lfxs R T). -#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02 -lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12 -lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01 -elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] -[ #L #HL1 #HL2 - elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1 - elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2 - lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1 - lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2 - /3 width=5 by ex2_intro/ -| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02 - elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0 - lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01 - lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02 - elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma deleted file mode 100644 index ad4d40bb9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma +++ /dev/null @@ -1,43 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reduction/cpr.ma". - -(* EXAMPLES *****************************************************************) - -(* A reduction cycle in two steps: the term Omega ***************************) - -definition Delta: term → term ≝ λW. +ⓛW.ⓐ#0.#0. - -definition Omega1: term → term ≝ λW. ⓐ(Delta W).(Delta W). - -definition Omega2: term → term ≝ λW. +ⓓⓝW.(Delta W).ⓐ#0.#0. - -(* Basic properties *********************************************************) - -lemma Delta_lift: ∀W1,W2,l,k. ⬆[l, k] W1 ≡ W2 → - ⬆[l, k] (Delta W1) ≡ (Delta W2). -/4 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed. - -(* Main properties **********************************************************) - -theorem cpr_Omega_12: ∀G,L,W. ⦃G, L⦄ ⊢ Omega1 W ➡ Omega2 W. -/2 width=1 by cpr_beta/ qed. - -theorem cpr_Omega_21: ∀G,L,W. ⦃G, L⦄ ⊢ Omega2 W ➡ Omega1 W. -#G #L #W1 elim (lift_total W1 0 1) #W2 #HW12 -@(cpr_zeta … (Omega1 W2)) /3 width=1 by Delta_lift, lift_flat/ -@cpr_flat @(cpr_delta … (Delta W1) ? 0) -[3,5,8,10: /2 width=2 by Delta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma deleted file mode 100644 index e37f8831f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma +++ /dev/null @@ -1,54 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/fpbg_fpbs.ma". - -(* EXAMPLES *****************************************************************) - -(* Reflexivity of proper qrst-computation: the term ApplOmega ***************) - -definition ApplDelta: term → nat → term ≝ λW,s. +ⓛW.ⓐ⋆s.ⓐ#0.#0. - -definition ApplOmega1: term → nat → term ≝ λW,s. ⓐ(ApplDelta W s).(ApplDelta W s). - -definition ApplOmega2: term → nat → term ≝ λW,s. +ⓓⓝW.(ApplDelta W s).ⓐ⋆s.ⓐ#0.#0. - -definition ApplOmega3: term → nat → term ≝ λW,s. ⓐ⋆s.(ApplOmega1 W s). - -(* Basic properties *********************************************************) - -lemma ApplDelta_lift: ∀W1,W2,s,l,k. ⬆[l, k] W1 ≡ W2 → - ⬆[l, k] (ApplDelta W1 s) ≡ (ApplDelta W2 s). -/5 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed. - -lemma cpr_ApplOmega_12: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡ ApplOmega2 W s. -/2 width=1 by cpr_beta/ qed. - -lemma cpr_ApplOmega_23: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega2 W s ➡ ApplOmega3 W s. -#G #L #W1 #s elim (lift_total W1 0 1) #W2 #HW12 -@(cpr_zeta … (ApplOmega3 W2 s)) /4 width=1 by ApplDelta_lift, lift_flat/ -@cpr_flat // @cpr_flat @(cpr_delta … (ApplDelta W1 s) ? 0) -[3,5,8,10: /2 width=2 by ApplDelta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ] -qed. - -lemma cpxs_ApplOmega_13: ∀h,o,G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡*[h,o] ApplOmega3 W s. -/4 width=3 by cpxs_strap1, cpr_cpx/ qed. - -lemma fqup_ApplOmega_13: ∀G,L,W,s. ⦃G, L, ApplOmega3 W s⦄ ⊐+ ⦃G, L, ApplOmega1 W s⦄. -/2 width=1 by/ qed. - -(* Main properties **********************************************************) - -theorem fpbg_refl: ∀h,o,G,L,W,s. ⦃G, L, ApplOmega1 W s⦄ >≡[h,o] ⦃G, L, ApplOmega1 W s⦄. -/3 width=5 by fpbs_fpbg_trans, fqup_fpbg, cpxs_fpbs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma deleted file mode 100644 index af66f2c97..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma +++ /dev/null @@ -1,61 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/dynamic/snv.ma". - -(* EXAMPLES *****************************************************************) - -(* Extended validy (basic?_2) vs. restricted validity (basic_1) *************) - -(* extended validity of a closure, last arg of snv_appl > 1 *) -lemma snv_extended: ∀h,o,a,G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{a}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ¡[h, o]. -#h #o #a #G #L #s elim (deg_total h o s) -#d #Hd @(snv_appl … a … (⋆s) … (⋆s) (0+1+1)) -[ /4 width=5 by snv_lref, drop_drop_lt/ -| /4 width=13 by snv_bind, snv_lref/ -| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/ -| @(lstas_scpds … (d+1+1)) - /5 width=11 by lstas_bind, lstas_succ, da_bind, da_ldec, da_sort, lift_bind/ -] -qed. - -(* restricted validity of the η-expanded closure, last arg of snv_appl = 1 **) -lemma snv_restricted: ∀h,o,a,G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{a}⋆s.⋆s.ⓛⓛ{a}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ¡[h, o]. -#h #o #a #G #L #s elim (deg_total h o s) -#d #Hd @(snv_appl … a … (⋆s) … (ⓐ#0.#2) (0+1)) -[ /4 width=5 by snv_lref, drop_drop_lt/ -| @snv_lref [4: // |1,2,3: skip ] - @snv_bind // - @(snv_appl … a … (⋆s) … (⋆s) (0+1)) - [ @snv_lref [4: // |1,2,3: skip ] // - | @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind // - | @(lstas_scpds … (d+1)) /3 width=6 by da_sort, da_ldec, lstas_succ/ - | @(lstas_scpds … (d+1)) /3 width=8 by lstas_succ, lstas_bind, drop_drop, lift_bind/ - @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] /3 width=1 by da_sort, da_bind/ - ] -| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/ -| @(lstas_scpds … (d+1+1)) // - [ @da_ldec [3: // |1,2: skip ] - @da_bind @da_flat @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] - /3 width=1 by da_sort, da_bind/ - | @lstas_succ [4: // |1,2: skip ] - [2: @lstas_bind | skip ] - [2: @lstas_appl | skip ] - [2: @lstas_zero - [4: /2 width=1 by drop_drop_lt/ |5: /2 width=2 by lstas_bind/ |*: skip ] - |1: skip ] - /4 width=2 by lift_flat, lift_bind, lift_lref_ge_minus, lift_lref_lt/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma deleted file mode 100644 index 260430451..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/unfold/lstas.ma". - -(* EXAMPLES *****************************************************************) - -(* Static type assignment (iterated vs primitive): the declared variable ****) - -(* basic_1: we have "L.ⓛⓝ⋆k1.⋆k2⦄ ⊢ #0 • ⓝ⋆k1.⋆k2". *) -theorem sta_ldec: ∀h,G,L,s1,s2. ⦃G, L.ⓛⓝ⋆s1.⋆s2⦄ ⊢ #0 •*[h, 1] ⋆s2. -/3 width=6 by lstas_sort, lstas_succ, lstas_cast, drop_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma new file mode 100644 index 000000000..757d3e684 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma @@ -0,0 +1,234 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/relationstarstar_4.ma". +include "basic_2/static/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +definition lfxss (R) (T): relation lenv ≝ TC … (lfxs R T). + +interpretation "tc of generic extension on referred entries (local environment)" + 'RelationStarStar R T L1 L2 = (lfxss R T L1 L2). + +(* Basic properties ***********************************************************) + +lemma lfxss_atom: ∀R,I. ⋆ ⦻**[R, ⓪{I}] ⋆. +/2 width=1 by inj/ qed. + +lemma lfxss_sort: ∀R,I,L1,L2,V1,V2,s. + L1 ⦻**[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻**[R, ⋆s] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #s #H elim H -L2 +/3 width=4 by lfxs_sort, step, inj/ +qed. + +lemma lfxss_lref: ∀R,I,L1,L2,V1,V2,i. + L1 ⦻**[R, #i] L2 → L1.ⓑ{I}V1 ⦻**[R, #⫯i] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #i #H elim H -L2 +/3 width=4 by lfxs_lref, step, inj/ +qed. + +lemma lfxss_gref: ∀R,I,L1,L2,V1,V2,l. + L1 ⦻**[R, §l] L2 → L1.ⓑ{I}V1 ⦻**[R, §l] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #l #H elim H -L2 +/3 width=4 by lfxs_gref, step, inj/ +qed. + +lemma lfxss_sym: ∀R. lexs_frees_confluent R cfull → + (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀T. symmetric … (lfxss R T). +#R #H1R #H2R #T #L1 #L2 #H elim H -L2 +/4 width=3 by lfxs_sym, TC_strap, inj/ +qed-. + +lemma lfxss_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → + ∀L1,L2,T. L1 ⦻**[R1, T] L2 → L1 ⦻**[R2, T] L2. +#R1 #R2 #HR #L1 #L2 #T #H elim H -L2 +/4 width=5 by lfxs_co, step, inj/ +qed-. +(* +(* Basic inversion lemmas ***************************************************) + +lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. +#R #I #Y2 * /2 width=4 by lexs_inv_atom1/ +qed-. + +lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. +#R #I #Y1 * /2 width=4 by lexs_inv_atom2/ +qed-. + +lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2 +[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ +| lapply (frees_inv_sort … H1) -H1 #Hf + elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct + /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=9 by ex4_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=8 by ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2 +[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ +| lapply (frees_inv_gref … H1) -H1 #Hf + elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct + /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → + L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. +#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf +/6 width=6 by sle_lexs_trans, lexs_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +qed-. + +lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → + L1 ⦻*[R, V] L2 ∧ L1 ⦻*[R, T] L2. +#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf +/5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 → + ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → + ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 → + ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 → + ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. +#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf +/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ +qed-. + +lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → + R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. +#R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV // +qed-. + +lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // +qed-. + +lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, T] L2. +#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // +qed-. + +lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ +qed-. + +(* Basic_2A1: removed theorems 24: + llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref + llpx_sn_bind llpx_sn_flat + llpx_sn_inv_bind llpx_sn_inv_flat + llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length + llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx + llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co + llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx +*) +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma new file mode 100644 index 000000000..f063b1816 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma @@ -0,0 +1,31 @@ +(* +lemma lfxss_zero: ∀R,I,L1,L2,V1. L1 ⦻**[R, V1] L2 → ∀V2. + R L1 V1 V2 → L1.ⓑ{I}V1 ⦻**[R, #0] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #H + +elim H -L2 /3 width=5 by lfxs_zero, inj/ +#L #L2 #H0 #HL2 #IH #V2 #HV12 +lapply (IH … HV12) -IH #HL1 +@(step … HL1) -HL1 @lfxs_zero + +axiom pippo_fwd: ∀R,I,Y1,L2,V2,T. Y1 ⦻*[R, T] L2.ⓑ{I}V2 → + ∃∃L1,V1. Y1 = L1.ⓑ{I}V1. + +fact pippo: ∀R,I,L1,Y,T,V. L1.ⓑ{I}V ⦻**[R, T] Y → + ∀L2,V1. Y = L2.ⓑ{I}V1 → + ∀V2. R L1 V V2 → + L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V2. +#R #I #L1 #Y #T #V #H elim H -Y +[ /3 width=2 by lfxs_pair_repl_dx, inj/ +| #L #Y #_ #HL2 #IH #L2 #V1 #H #V2 #HV2 destruct + elim (pippo_fwd … HL2) #L0 #V0 #H destruct + @step [2: @(IH … HV2) // | skip ] -IH -HV2 + +lemma lfxss_pair_repl_dx: ∀R,I,L1,L2,T,V,V1. + L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V1 → + ∀V2. R L1 V V2 → + L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V2. +#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR +/3 width=5 by lexs_pair_repl, ex2_intro/ +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma new file mode 100644 index 000000000..d0362ba88 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h , break term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedTySnStar $h $T $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma new file mode 100644 index 000000000..145078d07 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ⦻ * * [ break term 46 R , break term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'RelationStarStar $R $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma index c9d5f5ae9..64f1facd2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma @@ -13,38 +13,30 @@ (**************************************************************************) include "basic_2/syntax/tsts.ma". -include "basic_2/computation/lpxs_cpxs.ma". +include "basic_2/rt_computation/lfpxs_cpxs.ma". -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) - -(* Forward lemmas involving same top term structure *************************) +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) +(* Forward lemmas with same top term structure ******************************) +(* lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ⬈*[h, o] U → T ≂ U. #h #o #G #L #T #HT #U #H >(cpxs_inv_cnx1 … H HT) -G -L -T // qed-. - -lemma cpxs_fwd_sort: ∀h,o,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h, o] U → - ⋆s ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h, o] U. -#h #o #G #L #U #s #H -elim (cpxs_inv_sort1 … H) -H #n #d generalize in match s; -s @(nat_ind_plus … n) -n -[ #s #_ #H -d destruct /2 width=1 by or_introl/ -| #n #IHn #s >plus_plus_comm_23 #Hnd #H destruct - lapply (deg_next_SO … Hnd) -Hnd #Hnd - elim (IHn … Hnd) -IHn - [ #H lapply (tsts_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/ - | generalize in match Hnd; -Hnd @(nat_ind_plus … n) -n - /4 width=3 by cpxs_strap2, cpx_st, or_intror/ - | >iter_SO >iter_n_Sm // - ] +*) +lemma cpxs_fwd_sort: ∀h,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U → + ⋆s ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U. +#h #G #L #U #s #H elim (cpxs_inv_sort1 … H) -H * +[ #H destruct /2 width=1 by or_introl/ +| #n #H destruct + @or_intror >iter_S <(iter_n_Sm … (next h)) // (**) ] qed-. (* Basic_1: was just: pr3_iso_beta *) -lemma cpxs_fwd_beta: ∀h,o,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ⬈*[h, o] U → - ⓐV.ⓛ{a}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ⬈*[h, o] U. -#h #o #a #G #L #V #W #T #U #H -elim (cpxs_inv_appl1 … H) -H * +lemma cpxs_fwd_beta: ∀h,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U → + ⓐV.ⓛ{p}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U. +#h #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * [ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma index 7d23b2f92..03651de12 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma @@ -13,27 +13,27 @@ (**************************************************************************) include "basic_2/syntax/term_vector.ma". -include "basic_2/computation/csx.ma". +include "basic_2/rt_computation/csx.ma". -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) +(* STRONGLY NORMALIZING TERMS VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION **) definition csxv: ∀h. sd h → relation3 genv lenv (list term) ≝ λh,o,G,L. all … (csx h o G L). interpretation - "context-sensitive strong normalization (term vector)" - 'SN h o G L Ts = (csxv h o G L Ts). + "strong normalization for uncounted context-sensitive parallel rt-transition (term vector)" + 'PRedTyStrong h o G L Ts = (csxv h o G L Ts). (* Basic inversion lemmas ***************************************************) -lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬊*[h, o] T @ Ts → - ⦃G, L⦄ ⊢ ⬊*[h, o] T ∧ ⦃G, L⦄ ⊢ ⬊*[h, o] Ts. +lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T@Ts⦄ → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Ts⦄. normalize // qed-. (* Basic forward lemmas *****************************************************) -lemma csx_fwd_applv: ∀h,o,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Ⓐ Vs.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, o] T. +lemma csx_fwd_applv: ∀h,o,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.T⦄ → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. #h #o #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/ #V #Vs #IHVs #HVs lapply (csx_fwd_pair_sn … HVs) #HV diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma new file mode 100644 index 000000000..7e1b32915 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/predtysnstar_5.ma". +include "basic_2/rt_transition/lfpx.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +definition lfpxs: ∀h. relation4 genv term lenv lenv ≝ + λh,G,T. TC … (lfpx h G T). + +interpretation + "uncounted parallel rt-computation on referred entries (local environment)" + 'PRedTySnStar h T G L1 L2 = (lfpxs h G T L1 L2). + +(* Basic properties *********************************************************) + +(* Basic_2A1: was just: lpx_lpxs *) +lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=1 by inj/ qed. + +(* Basic_2A1: was just: lpxs_strap1 *) +lemma lfpxs_strap1: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by step/ qed. + +(* Basic_2A1: was just: lpxs_strap2 *) +lemma lfpxs_strap2: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by TC_strap/ qed. +(* +(* Basic_2A1: was just: lpxs_pair_refl *) +lemma lfpxs_pair_refl: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V. +/2 width=1 by TC_lpx_sn_pair_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: was just: lpxs_inv_atom1 *) +lemma lfpxs_inv_atom1: ∀h,G,L2.T. ⦃G, ⋆⦄ ⊢ ⬈*[h, T] L2 → L2 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. + +(* Basic_2A1: was just: lpxs_inv_atom2 *) +lemma lfpxs_inv_atom2: ∀h,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] ⋆ → L1 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma new file mode 100644 index 000000000..8c8679a47 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma @@ -0,0 +1,3 @@ +(* Basic_2A1: was just: lprs_lpxs *) +lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. +/3 width=3 by lpr_lpx, monotonic_TC/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma new file mode 100644 index 000000000..ce2496b91 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/lfpx_fqup.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +(* Advanced eliminators *****************************************************) + +(* Basic_2A1: was just: lpxs_ind *) +lemma lfpxs_ind: ∀h,G,L1,T. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → R L → R L2) → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L2. +#h #G #L1 #T #R #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +(* Basic_2A1: was just: lpxs_ind_dx *) +lemma lfpxs_ind_dx: ∀h,G,L2,T. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → R L → R L1) → + ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L1. +#h #o #G #L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Advanced properties ******************************************************) + +(* Basic_2A1: was just: lpxs_refl *) +lemma lfpxs_refl: ∀h,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, T] L. +/2 width=1 by lfpx_lfpxs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma new file mode 100644 index 000000000..ac2f64dc5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma @@ -0,0 +1,7 @@ +(* Basic forward lemmas *****************************************************) + +(* Forward lemmas with length for local environments ************************) + +(* Basic_2A1: was just: lpxs_fwd_length *) +lemma lfpxs_fwd_length: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h, o] L2 → |L1| = |L2|. +/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma deleted file mode 100644 index b6c91c8b1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/predsnstar_5.ma". -include "basic_2/reduction/lpx.ma". -include "basic_2/computation/lprs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝ - λh,o,G. TC … (lpx h o G). - -interpretation "extended parallel computation (local environment, sn variant)" - 'PRedSnStar h o G L1 L2 = (lpxs h o G L1 L2). - -(* Basic eliminators ********************************************************) - -lemma lpxs_ind: ∀h,o,G,L1. ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L → ⦃G, L⦄ ⊢ ➡[h, o] L2 → R L → R L2) → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L2. -#h #o #G #L1 #R #HL1 #IHL1 #L2 #HL12 -@(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma lpxs_ind_dx: ∀h,o,G,L2. ∀R:predicate lenv. R L2 → - (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, o] L → ⦃G, L⦄ ⊢ ➡*[h, o] L2 → R L → R L1) → - ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1. -#h #o #G #L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma lprs_lpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/3 width=3 by lpr_lpx, monotonic_TC/ qed. - -lemma lpx_lpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/2 width=1 by inj/ qed. - -lemma lpxs_refl: ∀h,o,G,L. ⦃G, L⦄ ⊢ ➡*[h, o] L. -/2 width=1 by lprs_lpxs/ qed. - -lemma lpxs_strap1: ∀h,o,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L → ⦃G, L⦄ ⊢ ➡[h, o] L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/2 width=3 by step/ qed. - -lemma lpxs_strap2: ∀h,o,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L → ⦃G, L⦄ ⊢ ➡*[h, o] L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/2 width=3 by TC_strap/ qed. - -lemma lpxs_pair_refl: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V. -/2 width=1 by TC_lpx_sn_pair_refl/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma lpxs_inv_atom1: ∀h,o,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, o] L2 → L2 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. - -lemma lpxs_inv_atom2: ∀h,o,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, o] ⋆ → L1 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpxs_fwd_length: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → |L1| = |L2|. -/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 556cb5704..cb191dab1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,2 +1,4 @@ cpxs.ma cpxs_tdeq.ma cpxs_cpxs.ma +lfpxs.ma lfpxs_fqup.ma csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma +csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index 654ab4d0d..26289760b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -35,19 +35,7 @@ theorem lfxs_flat: ∀R,I,L1,L2,V,T. #R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) /3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ qed. -(* -theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull → - ∀T. Transitive … (lfxs R T). -#R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 -elim (H1R … Hf1 … HL1) #f #H0 #H1 -lapply (frees_mono … Hf2 … H0) -Hf2 -H0 #Hf2 -lapply (lexs_eq_repl_back … HL2 … Hf2) -f2 #HL2 -lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1 -@(ex2_intro … f) -/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/ -qed-. -*) theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull → R_confluent2_lfxs R R R R → ∀T. confluent … (lfxs R T). 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 03c104136..f3d9d6021 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 @@ -11,14 +11,6 @@ table { ] (* class "wine" - [ { "examples" * } { - [ { "terms with special features" * } { - [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" + "ex_snv_eta" * ] - } - ] - } - ] - class "magenta" [ { "" * } { [ { "" * } { [ "" * ] @@ -35,7 +27,7 @@ table { } ] *) - class "prune" + class "magenta" [ { "dynamic typing" * } { (* [ { "local env. ref. for native type assignment" * } { @@ -58,7 +50,7 @@ table { ] } ] - class "blue" + class "prune" [ { "equivalence" * } { [ { "decomposed rt-equivalence" * } { [ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] @@ -70,7 +62,7 @@ table { ] } ] - class "sky" + class "blue" [ { "conversion" * } { [ { "context-sensitive conversion" * } { [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )" "cpc_cpc" * ] @@ -79,7 +71,7 @@ table { } ] *) - class "cyan" + class "sky" [ { "rt-computation" * } { (* [ { "evaluation for context-sensitive rt-reduction" * } { @@ -121,13 +113,15 @@ table { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] *) + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_cpxs" * ] } ] } ] - class "water" + class "cyan" [ { "rt-transition" * } { [ { "parallel qrst-transition" * } { (* [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" + "fpbq_aaa" * ] *) @@ -159,6 +153,14 @@ table { ] } ] + class "water" + [ { "iterated static typing" * } { + [ { "generic extension on referred entries" * } { + [ "lfxss ( ? ⦻**[?,?] ? )" * ] + } + ] + } + ] class "green" [ { "static typing" * } { [ { "generic reducibility" * } { diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 1c14e9fed..7596031ba 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -4,3 +4,4 @@ basic_2/relocation basic_2/s_transition basic_2/s_computation basic_2/static +basic_2/i_static