]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 4f9165b)
update in apps_2
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 7 May 2018 19:59:37 +0000 (21:59 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 7 May 2018 19:59:37 +0000 (21:59 +0200)
+ update to web site

helm/www/lambdadelta/web/home/home.ldw.xml patch | blob | history
matita/matita/contribs/lambdadelta/apps_2/models/veq.ma patch | blob | history
matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma [new file with mode: 0644] patch | blob

diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml
index e1b5eb42564e1f7ca01c3ffd5430e5ec12c94f65..8e6135836d861a64fffbbf64e845257b950916ab 100644 (file)
--- a/helm/www/lambdadelta/web/home/home.ldw.xml
+++ b/helm/www/lambdadelta/web/home/home.ldw.xml
@@ -11,13 +11,14 @@
    <section9 name="foreword">Foreword</section9>
    <body>
       The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support
    <section9 name="foreword">Foreword</section9>
    <body>
       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 <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation</link>
-       and its predecessors).
+      the foundational frameworks for Mathematics that require an underlying specification language,
+      for example the
+      <link to="http://www.math.unipd.it/~maietti/">Minimalist Foundation (MF)</link>
+      and its predecessors.
    </body>
    <body>
       The λδ family is developed within the
    </body>
    <body>
       The λδ family is developed within the
-      <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
+      <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics (HELM)</link>
       as a set of machine-checked digital specifications.
    </body>
    <body>
       as a set of machine-checked digital specifications.
    </body>
    <body>
@@ -25,12 +26,9 @@
       (revised <notice class="alpha" text="2012-09"/>).
    </body>
    <body>
       (revised <notice class="alpha" text="2012-09"/>).
    </body>
    <body>
-      <notice class="alpha" text="Notice for the user of Internet Explorer."/>
-      To view this site correctly, please select a font
+      <notice class="alpha" text="Notice:"/>
+      to view this site correctly, please select a font
       with <link to="http://www.unicode.org/">Unicode</link> support.
       with <link to="http://www.unicode.org/">Unicode</link> 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.
    </body>
 
 <!-- ===================================================================== -->
    </body>
 
 <!-- ===================================================================== -->
@@ -41,13 +39,13 @@
    </body>
 
    <topitem name="C10">
    </body>
 
    <topitem name="C10">
-      Matthias Weber:
+      M. Weber:
       <notice class="alpha">An extended type system with lambda-typed lambda-expressions</notice>
       (2018). Technical report. Faculty of Computer Science, Technical University of Berlin.
    </topitem>
 
    <topitem name="C9">
       <notice class="alpha">An extended type system with lambda-typed lambda-expressions</notice>
       (2018). Technical report. Faculty of Computer Science, Technical University of Berlin.
    </topitem>
 
    <topitem name="C9">
-      Matthias Weber:
+      M. Weber:
       <notice class="alpha">An extended type system with lambda-typed lambda-expressions (extended version)</notice>
       (2018). Technical report. Faculty of Computer Science, Technical University of Berlin.
    </topitem>
       <notice class="alpha">An extended type system with lambda-typed lambda-expressions (extended version)</notice>
       (2018). Technical report. Faculty of Computer Science, Technical University of Berlin.
    </topitem>
diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
index 47d4a1b74a4238e3898c2e0ac4ff4a0469f4ab3a..87a0800e75746a5481bc7e83207c9f159a64bed0 100644 (file)
--- 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 *******************************)
 
 
 (* 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
 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 ***************************************) 
 
 
 (* 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.
 | /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 (file)
index 0000000..fce7d42
--- /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/
+  ]
+]  
Unnamed repository; edit this file 'description' to name the repository.