From fdf7649cd98c08e6153f08ae5831191d9cbf1574 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 7 May 2018 21:59:37 +0200 Subject: [PATCH] update in apps_2 + update to web site --- helm/www/lambdadelta/web/home/home.ldw.xml | 20 ++++---- .../contribs/lambdadelta/apps_2/models/veq.ma | 28 +++++++++-- .../lambdadelta/apps_2/models/veq_lifts.ma | 46 +++++++++++++++++++ 3 files changed, 79 insertions(+), 15 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma 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/ + ] +] -- 2.39.2