From: Ferruccio Guidi Date: Mon, 7 May 2018 19:59:37 +0000 (+0200) Subject: update in apps_2 X-Git-Tag: make_still_working~329 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fdf7649cd98c08e6153f08ae5831191d9cbf1574;p=helm.git update in apps_2 + update to web site --- diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml index e1b5eb425..8e6135836 100644 --- a/helm/www/lambdadelta/web/home/home.ldw.xml +++ b/helm/www/lambdadelta/web/home/home.ldw.xml @@ -11,13 +11,14 @@ Foreword The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support - the foundational frameworks for Mathematics that require an underlying specification language - (for example the Minimalist Foundation - and its predecessors). + the foundational frameworks for Mathematics that require an underlying specification language, + for example the + Minimalist Foundation (MF) + and its predecessors. The λδ family is developed within the - Hypertextual Electronic Library of Mathematics + Hypertextual Electronic Library of Mathematics (HELM) as a set of machine-checked digital specifications. @@ -25,12 +26,9 @@ (revised ). - - To view this site correctly, please select a font + + to view this site correctly, please select a font with Unicode support. - For example "Lucida Sans Unicode" (it should be already installed on your system). - To change the current font follow: - "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button. @@ -41,13 +39,13 @@ - Matthias Weber: + M. Weber: An extended type system with lambda-typed lambda-expressions (2018). Technical report. Faculty of Computer Science, Technical University of Berlin. - Matthias Weber: + M. Weber: An extended type system with lambda-typed lambda-expressions (extended version) (2018). Technical report. Faculty of Computer Science, Technical University of Berlin. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma index 47d4a1b74..87a0800e7 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -42,14 +42,29 @@ lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv → (* Properties with evaluation evaluation lift *******************************) +theorem vlift_swap (M): ∀i1,i2. i1 ≤ i2 → + ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≐{?,dd M} ⫯[↑i2←d2] ⫯[i1←d1] lv. +#M #i1 #i2 #Hi12 #lv #d1 #d2 #j +elim (lt_or_eq_or_gt j i1) #Hji1 destruct +[ >vlift_lt // >vlift_lt /2 width=3 by lt_to_le_to_lt/ + >vlift_lt /3 width=3 by lt_S, lt_to_le_to_lt/ >vlift_lt // +| >vlift_eq >vlift_lt /2 width=1 by monotonic_le_plus_l/ >vlift_eq // +| >vlift_gt // elim (lt_or_eq_or_gt (↓j) i2) #Hji2 destruct + [ >vlift_lt // >vlift_lt /2 width=1 by lt_minus_to_plus/ >vlift_gt // + | >vlift_eq <(lt_succ_pred … Hji1) >vlift_eq // + | >vlift_gt // >vlift_gt /2 width=1 by lt_minus_to_plus_r/ >vlift_gt /2 width=3 by le_to_lt_to_lt/ + ] +] +qed-. + lemma vlift_comp (M): ∀i. compatible_3 … (vlift M i) (sq M) (veq M) (veq M). #m #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j elim (lt_or_eq_or_gt j i) #Hij destruct -[ >(vlift_lt … Hij) >(vlift_lt … Hij) // -| >(vlift_eq …) >(vlift_eq …) // -| >(vlift_gt … Hij) >(vlift_gt … Hij) // +[ >vlift_lt // >vlift_lt // +| >vlift_eq >vlift_eq // +| >vlift_gt // >vlift_gt // ] -qed. +qed-. (* Properies with term interpretation ***************************************) @@ -66,3 +81,8 @@ lemma ti_comp_l (M): is_model M → | /4 width=5 by seq_sym, me, mr/ ] qed. + +lemma ti_ext_l (M): is_model M → + ∀T,gv,lv1,lv2. lv1 ≐ lv2 → + ⟦T⟧[gv, lv1] ≗{M} ⟦T⟧[gv, lv2]. +/3 width=1 by ti_comp_l, ext_veq/ 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 new file mode 100644 index 000000000..fce7d4281 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.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 "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]. +#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 + @(mr … H1M) [4,5: @(seq_sym … H1M) @(ml … H1M) |1,2: skip ] +| /4 width=3 by seq_trans, seq_sym, mg/ +| #f #p * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #n #Hn #lv #d + [ @(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 ] + /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 + [ /4 width=5 by seq_sym, ma, mc, mr/ + | /4 width=5 by seq_sym, me, mr/ + ] +]