From f663836446db6814e2d0cbb11638070ede01bdb4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 1 Dec 2013 21:24:28 +0000 Subject: [PATCH] commit of the "substitution" component and of some auxiliary files ... --- .../lambdadelta/basic_2/etc/leq/leq.etc | 65 +++++++++++++++++++ .../lambdadelta/basic_2/etc/leq/leq_old.etc | 44 +++++++++++++ .../lambdadelta/basic_2/etc/leq/leqdx.etc | 58 +++++++++++++++++ .../lambdadelta/basic_2/etc/leq/leqdx_3.etc | 19 ++++++ .../basic_2/substitution/fqup_fqup.ma | 2 +- .../basic_2/substitution/fqup_lleq.ma | 32 +++++++++ .../basic_2/substitution/fqus_fqus.ma | 2 +- .../basic_2/substitution/fqus_lleq.ma | 29 +++++++++ .../lambdadelta/basic_2/web/basic_2.ldw.xml | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 22 ++++--- .../lambdadelta/ground_2/web/ground_2_src.tbl | 2 +- 11 files changed, 264 insertions(+), 13 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_old.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx_3.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc new file mode 100644 index 000000000..a21457b4e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_length.ma". + +(* LOCAL ENVIRONMENT EQUALITY ***********************************************) + +notation "hvbox( T1 break [ d , break e ] ≈ break T2 )" + non associative with precedence 45 + for @{ 'Eq $T1 $d $e $T2 }. + +inductive leq: nat → nat → relation lenv ≝ +| leq_sort: ∀d,e. leq d e (⋆) (⋆) +| leq_OO: ∀L1,L2. leq 0 0 L1 L2 +| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 → + leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V) +| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e. + leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2) +. + +interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2). + +definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R. + ∀L1,s1,s2. R L1 s1 s2 → + ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2. + +(* Basic properties *********************************************************) + +lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))). +#S #R #HR #L1 #s1 #s2 #H elim H -H s2 +[ /3 width=5/ +| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 + lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/ +] +qed. + +lemma leq_refl: ∀d,e,L. L [d, e] ≈ L. +#d elim d -d +[ #e elim e -e // #e #IHe #L elim L -L /2/ +| #d #IHd #e #L elim L -L /2/ +] +qed. + +lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1. +#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/ +qed. + +lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d → + ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2. + +#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ +qed. + +(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_old.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_old.etc new file mode 100644 index 000000000..37deba7ac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_old.etc @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_length.ma". + +(* LOCAL ENVIRONMENT EQUALITY ***********************************************) + +interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2). + +(* Basic properties *********************************************************) + +| leq_comp: ∀L1,L2,I1,I2,V1,V2. + leq L1 0 0 L2 → leq (L1. 𝕓{I1} V1) 0 0 (L2. 𝕓{I2} V2) + +lemma leq_fwd_length: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → |L1| = |L2|. +#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize // +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma leq_inv_sort1_aux: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L1 = ⋆ → L2 = ⋆. +#L1 #L2 #d #e #H elim H -H L1 L2 d e +[ // +| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #H destruct +| #L1 #L2 #I #V #e #_ #_ #H destruct +| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #_ #H destruct +qed. + +lemma leq_inv_sort1: ∀L2,d,e. ⋆ [d, e] ≈ L2 → L2 = ⋆. +/2 width=5/ qed. + +lemma leq_inv_sort2: ∀L1,d,e. L1 [d, e] ≈ ⋆ → L1 = ⋆. +/3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx.etc new file mode 100644 index 000000000..63b43d876 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx.etc @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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/leqdx_3.ma". +include "basic_2/grammar/lenv_length.ma". + +(* DX GUARDED EQUIVALENCE FOR LOCAL ENVIRONMENTS ****************************) + +inductive leqdx: nat → relation lenv ≝ +| leqdx_atom: ∀d. leqdx d (⋆) (⋆) +| leqdx_zero: ∀I1,I2,L1,L2,V1,V2. + leqdx 0 L1 L2 → leqdx 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) +| leqdx_succ: ∀I,L1,L2,V,d. + leqdx d L1 L2 → leqdx (d+1) (L1.ⓑ{I}V) (L2.ⓑ{I}V) +. + +interpretation + "guarded equivalence (local environment, dx variant)" + 'LEqDx d L1 L2 = (leqdx d L1 L2). + +(* Basic properties *********************************************************) + +lemma leqdx_O: ∀L1,L2. |L1| = |L2| → L1 ≚[0] L2. +#L1 elim L1 -L1 +[ #L2 #H >(length_inv_zero_sn … H) -L2 // +| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H + #I2 #L2 #V2 #HL12 #H destruct /3 width=1 by leqdx_zero/ +] +qed. + +(* Basic inversion lemmas ***************************************************) + +fact leqdx_inv_succ2_aux: ∀L1,L2,d. L1 ≚[d] L2 → + ∀I,K2,V,e. L2 = K2.ⓑ{I}V → d = e + 1 → + ∃∃K1. K1 ≚[e] K2 & L1 = K1.ⓑ{I}V. +#L1 #L2 #d * -L1 -L2 -d +[ #d #J #K2 #W #e #H destruct +| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K2 #W #e #_ + >commutative_plus normalize #H destruct +| #I #L1 #L2 #V #d #HL12 #J #K2 #W #e #H1 #H2 destruct + /2 width=3 by ex2_intro/ +] +qed-. + +lemma leqdx_inv_succ2: ∀I,L1,K2,V,d. L1 ≚[d+1] K2.ⓑ{I}V → + ∃∃K1. K1 ≚[d] K2 & L1 = K1.ⓑ{I}V. +/2 width=5 by leqdx_inv_succ2_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx_3.etc new file mode 100644 index 000000000..54a9c5f50 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx_3.etc @@ -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 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LEqDx $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma index a6bff5ede..0dd0e336f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma @@ -16,7 +16,7 @@ include "basic_2/substitution/fqup.ma". (* PLUS-ITERATED SUPCLOSURE *************************************************) -(* Main propertis ***********************************************************) +(* Main properties **********************************************************) theorem fqup_trans: tri_transitive … fqup. /2 width=5 by tri_TC_transitive/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma new file mode 100644 index 000000000..582888e21 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fqu_lleq.ma". +include "basic_2/substitution/fqup.ma". + +(* PLUS-ITERATED SUPCLOSURE *************************************************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[0, T] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃+ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. +#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U +[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2 + /3 width=3 by fqu_fqup, ex2_intro/ +| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2 + #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K + /3 width=5 by fqup_strap1, ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma index de58e2d76..295d45b17 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma @@ -16,7 +16,7 @@ include "basic_2/substitution/fqus.ma". (* STAR-ITERATED SUPCLOSURE *************************************************) -(* Advaveded properties *****************************************************) +(* Main properties **********************************************************) theorem fqus_trans: tri_transitive … fqus. /2 width=5 by tri_TC_transitive/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma new file mode 100644 index 000000000..7c0cc1340 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/fqup_lleq.ma". +include "basic_2/substitution/fqus_alt.ma". + +(* STAR-ITERATED SUPCLOSURE *************************************************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃* ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[0, T] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃* ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. +#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H +[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/ +| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ +] +qed-. 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 f596851ee..21d828012 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 @@ -83,7 +83,7 @@
Logical Structure of the Specification
The source files are grouped in planes and components according to the following table. - A notation file covering the whole specification is provided. + Notation files covering the whole specification are provided. The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders). 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 5e21f5395..aa69b6572 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 @@ -104,7 +104,7 @@ table { ] [ { "context-sensitive extended computation" * } { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] [ { "context-sensitive computation" * } { @@ -134,8 +134,8 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_aaa" + "lpx_lpx" * ] - [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cix" + "cpx_cpx" * ] + [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] + [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_lleq" + "cpx_cix" * ] } ] [ { "context-sensitive extended irreducible forms" * } { @@ -212,8 +212,8 @@ table { } ] [ { "iterated structural successor for closures" * } { - [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ] - [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ] + [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_lleq" + "fqus_fqus" * ] + [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_lleq" + "fqup_fqup" * ] } ] [ { "generic local env. slicing" * } { @@ -234,12 +234,12 @@ table { class "orange" [ { "relocation" * } { [ { "structural successor for closures" * } { - [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_fquq" * ] - [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_fqu" * ] + [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_lleq" * ] + [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_lleq" * ] } ] [ { "lazy equivalence for local environments" * } { - [ "lleq ( ? ⋕[?] ? )" "lleq_fleq" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_lleq" * ] } ] [ { "global env. slicing" * } { @@ -247,7 +247,7 @@ table { } ] [ { "basic local env. slicing" * } { - [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ] + [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_leq" + "ldrop_ldrop" * ] } ] [ { "basic term relocation" * } { @@ -259,6 +259,10 @@ table { ] class "red" [ { "grammar" * } { + [ { "equivalence for local environments" * } { + [ "leq ( ? ≃[?,?] ? ) " * ] + } + ] [ { "pointwise extension of a relation" * } { [ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 827a8fcf8..56159d210 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -8,7 +8,7 @@ table { ] class "yellow" [ { "natural numbers with infinity" * } { - [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" "ynat_plus ( ? + ? )" * ] + [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" "ynat_minus ( ? - ? )" "ynat_plus ( ? + ? )" * ] } ] class "orange" -- 2.39.2