From f86ab1580e0bab7f8cada3cc7ffdf80f40e3de9a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 8 May 2018 20:57:08 +0200 Subject: [PATCH] update in grond_2 and models + denotation is preserved by lifts in extensional models --- .../apps_2/etc/models/model_lift.etc | 40 ---------------- .../lambdadelta/apps_2/models/veq_lifts.ma | 31 +++++++++---- .../lambdadelta/apps_2/web/apps_2_src.tbl | 2 +- .../ground_2/notation/functions/basic_2.ma | 19 ++++++++ .../ground_2/relocation/rtmap_basic.ma | 46 +++++++++++++++++++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 1 + 6 files changed, 90 insertions(+), 49 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/functions/basic_2.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lift.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lift.etc deleted file mode 100644 index 9775f57df..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lift.etc +++ /dev/null @@ -1,40 +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/substitution/lift.ma". -include "apps_2/models/model_lower.ma". -include "apps_2/models/model_sound.ma". - -(* MODEL ********************************************************************) - -(* Forward lemmas on basic relocation ***************************************) - -lemma sound_fwd_lift: ∀M. sound M → extensional M → - ∀sv,gv,T1,T2,l,m. ⬆[l, m] T1 ≡ T2 → - ∀lv. 〚T1〛{sv, gv, ↓[l, m]⦋M⦌ lv} = 〚T2〛{sv, gv, lv}. -#M #H1M #H2M #sv #gv #T1 #T2 #l #m #H elim H -T1 -T2 -l -m -[ #k #l #m #lv >(m1 … H1M) >(m1 … H1M) -H1M // -| #i #l #m #Hil #lv >(m2 … H1M) >(m2 … H1M) -H1M >lower_lt // -| #i #l #m #Hli #lv >(m2 … H1M) >(m2 … H1M) -H1M >lower_ge // -| #p #l #m #lv >(m3 … H1M) >(m3 … H1M) -H1M // -| #a * #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #lv - [ >(m4 … H1M) >(m4 … H1M) /3 width=1 by raise_lower_lt, sound_ti_eq_l/ - | @(mx … H2M) /3 width=1 by raise_lower_lt, sound_ti_eq_l/ - ] -| * #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #lv - [ >(m6 … H1M) >(m6 … H1M) /3 width=1 by eq_f2/ - | >(m7 … H1M) >(m7 … H1M) /2 width=1 by/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma index fce7d4281..80a103a48 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma @@ -12,35 +12,50 @@ (* *) (**************************************************************************) +include "ground_2/relocation/rtmap_basic.ma". include "basic_2/relocation/lifts.ma". include "apps_2/models/veq.ma". (* EVALUATION EQUIVALENCE **************************************************) -lemma pippo (M) (gv): is_model M → is_extensional M → - ∀f,T1,T2. ⬆*[f] T1 ≘ T2 → ∀n. ⫯*[n] 𝐔❴1❵ = f → - ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[n←d]lv]. +(* Forward lemmas with generic relocation ***********************************) + +fact lifts_fwd_vlift_aux (M) (gv): is_model M → is_extensional M → + ∀f,T1,T2. ⬆*[f] T1 ≘ T2 → ∀m. 𝐁❴m,1❵ = f → + ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[m←d]lv]. #M #gv #H1M #H2M #f #T1 #T2 #H elim H -f -T1 -T2 [ /4 width=3 by seq_trans, seq_sym, ms/ -| #f #i1 #i2 #Hi12 #n #Hn #lv #d +| #f #i1 #i2 #Hi12 #m #Hm #lv #d destruct @(mr … H1M) [4,5: @(seq_sym … H1M) @(ml … H1M) |1,2: skip ] + elim (lt_or_ge i1 m) #Hi1 + [ lapply (at_basic_inv_lt … Hi12) -Hi12 // #H destruct + >vlift_lt /2 width=1 by mq/ + | lapply (at_basic_inv_ge … Hi12) -Hi12 // #H destruct + >vlift_gt /2 width=1 by mq, le_S_S/ + ] | /4 width=3 by seq_trans, seq_sym, mg/ -| #f #p * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #n #Hn #lv #d +| #f #p * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #lv #d destruct [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(md … H1M) |1,2: skip ] @(seq_trans … H1M) [2: @(ti_comp_l … H1M) | skip ] [2: @(vlift_comp … lv lv) | skip ] [3: /2 width=1 by veq_refl/ ] [2: @(IHV … d) // | skip ] - @(seq_trans … H1M) [2: @(IHT … d) // | skip ] + @(seq_trans … H1M) [2: @(IHT (↑m) … d) // | skip ] /4 width=1 by seq_sym, ti_ext_l, vlift_swap/ | @mx /2 width=1 by/ #d0 @(seq_trans … H1M) [3: @(seq_sym … H1M) @(ti_ext_l … H1M) | skip ] [2: @vlift_swap // | skip ] /2 width=1 by/ ] -| #f * #V1 #v2 #T1 #T2 #_ #_ #IHV #IHT #n #Hn #lv #d +| #f * #V1 #v2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #lv #d [ /4 width=5 by seq_sym, ma, mc, mr/ | /4 width=5 by seq_sym, me, mr/ ] -] +] +qed-. + +lemma lifts_SO_fwd_vlift (M) (gv): is_model M → is_extensional M → + ∀T1,T2. ⬆*[1] T1 ≘ T2 → + ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[d]lv]. +/2 width=3 by lifts_fwd_vlift_aux/ 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 3388f4350..b68727314 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 @@ -16,7 +16,7 @@ table { } ] [ { "evaluation equivalence" * } { - [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" * ] + [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" "veq_lifts" * ] } ] [ { "evaluation drop" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/basic_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/basic_2.ma new file mode 100644 index 000000000..f18cd54f3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/basic_2.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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( 𝐁❴ break term 46 l, break term 46 h ❵ )" + non associative with precedence 90 + for @{ 'Basic $l $h }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma new file mode 100644 index 000000000..b0dc5e24f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/functions/basic_2.ma". +include "ground_2/relocation/rtmap_at.ma". + +(* RELOCATION MAP ***********************************************************) + +definition basic: nat → nat → rtmap ≝ λm,n. ⫯*[m] 𝐔❴n❵. + +interpretation "basic relocation (rtmap)" + 'Basic m n = (basic m n). + +(* Prioerties with application **********************************************) + +lemma at_basic_lt: ∀m,n,i. i < m → @⦃i, 𝐁❴m,n❵⦄ ≘ i. +#m elim m -m [ #n #i #H elim (lt_zero_false … H) ] +#m #IH #n * [ /2 width=2 by refl, at_refl/ ] +#i #H lapply (lt_S_S_to_lt … H) -H /3 width=7 by refl, at_push/ +qed. + +lemma at_basic_ge: ∀m,n,i. m ≤ i → @⦃i, 𝐁❴m,n❵⦄ ≘ n+i. +#m elim m -m // +#m #IH #n #j #H +elim (le_inv_S1 … H) -H #i #Hmi #H destruct +/3 width=7 by refl, at_push/ +qed. + +(* Inversion lemmas with application ****************************************) + +lemma at_basic_inv_lt: ∀m,n,i,j. i < m → @⦃i, 𝐁❴m,n❵⦄ ≘ j → i = j. +/3 width=4 by at_basic_lt, at_mono/ qed-. + +lemma at_basic_inv_ge: ∀m,n,i,j. m ≤ i → @⦃i, 𝐁❴m,n❵⦄ ≘ j → n+i = j. +/3 width=4 by at_basic_ge, at_mono/ qed-. 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 5d0f40bd8..06ff4be72 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 @@ -25,6 +25,7 @@ table { "rtmap_fcla ( 𝐂⦃?⦄ ≘ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≘ ? )" "rtmap_sor ( ? ⋓ ? ≘ ? )" "rtmap_at ( @⦃?,?⦄ ≘ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )" + "rtmap_basic ( 𝐁❴?,?❵ )" * ] [ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" -- 2.39.2