update in functional

+ support for multiple filling

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma
index edc607bbc63f58a01b5e8f7837756266bb97ef26..30b8b65170937fda18daec0d02b4fd0f9e335ae7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma
@@ -36,6 +36,17 @@ interpretation "generic functional relocation (term)"
 interpretation "uniform functional relocation (term)"
    'UpArrow i T = (flifts (uni i) T).
 
 interpretation "uniform functional relocation (term)"
    'UpArrow i T = (flifts (uni i) T).
 

+(* Basic properties *********************************************************)
+
+lemma flifts_lref (f) (i): ↑*[f](#i) = #(f@❴i❵).
+// qed.
+
+lemma flifts_bind (f) (p) (I) (V) (T): ↑*[f](ⓑ{p,I}V.T) = ⓑ{p,I}↑*[f]V.↑*[⫯f]T.
+// qed.
+
+lemma flifts_flat (f) (I) (V) (T): ↑*[f](ⓕ{I}V.T) = ⓕ{I}↑*[f]V.↑*[f]T.
+// qed.
+

 (* Main properties **********************************************************)
 
 theorem flifts_lifts: ∀T,f. ⬆*[f]T ≘ ↑*[f]T.
 (* Main properties **********************************************************)
 
 theorem flifts_lifts: ∀T,f. ⬆*[f]T ≘ ↑*[f]T.


@@ -55,13 +66,10 @@ qed-.
 
 (* Derived properties *******************************************************)
 
 
 (* Derived properties *******************************************************)
 

+lemma flifts_comp: ∀f1,f2. f1 ≡ f2 → ∀T. ↑*[f1]T = ↑*[f2]T.
+/3 width=3 by flifts_inv_lifts, lifts_eq_repl_fwd/ qed.
+
+(* Derived properties with uniform relocation *******************************)
+

 lemma flifts_lref_uni: ∀l,i. ↑[l](#i) = #(l+i).
 /3 width=1 by flifts_inv_lifts, lifts_lref_uni/ qed.
 lemma flifts_lref_uni: ∀l,i. ↑[l](#i) = #(l+i).
 /3 width=1 by flifts_inv_lifts, lifts_lref_uni/ qed.

-(*
-lemma flift_join: ∀e1,e2,T. ⬆[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
-#e1 #e2 #T
-lapply (flift_lift T 0 (e1+e2)) #H
-elim (lift_split … H e1 e1) -H // #U #H
->(flift_inv_lift … H) -H //
-qed.
-*)

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_basic.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_basic.ma
index f3e6c31ddf06fb6bc345dc409d5b1d442eb5d971..5c50fb1af74a17fe5745b0f02ce822d7e95724b1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_basic.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_basic.ma
@@ -12,11 +12,21 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-include "ground_2/relocation/rtmap_basic.ma".
+include "ground_2/relocation/nstream_basic.ma".

 include "apps_2/functional/flifts.ma".
 include "apps_2/notation/functional/uparrow_3.ma".
 
 include "apps_2/functional/flifts.ma".
 include "apps_2/notation/functional/uparrow_3.ma".
 

-(* GENERIC FUNCTIONAL RELOCATION ********************************************)
+(* BASIC FUNCTIONAL RELOCATION **********************************************)

 
 interpretation "basic functional relocation (term)"
    'UpArrow d h T = (flifts (basic d h) T).
 
 interpretation "basic functional relocation (term)"
    'UpArrow d h T = (flifts (basic d h) T).

+
+(* Basic properties *********************************************************)
+
+lemma flifts_basic_lref_ge (i) (d) (h): d ≤ i → ↑[d,h](#i) = #(h+i).
+#i #d #h #Hdi
+/4 width=1 by apply_basic_ge, (* 2x *) eq_f/
+qed-.
+
+lemma flifts_basic_bind (p) (I) (V) (T) (d) (h): ↑[d,h](ⓑ{p,I}V.T) = ⓑ{p,I}(↑[d,h]V).(↑[↑d,h]T).
+// qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts.ma
new file mode 100644 (file)
index 0000000..de4b424
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/relocation/lifts_lifts.ma".
+include "apps_2/functional/flifts.ma".
+
+(* GENERIC FUNCTIONAL RELOCATION ********************************************)
+
+(* Main derived properties **************************************************)
+
+theorem flifts_compose (f2) (f1) (T): ↑*[f2]↑*[f1]T = ↑*[f2∘f1]T.
+#f2 #f1 #T
+elim (lifts_total T f1) #U #HTU
+>(flifts_inv_lifts … HTU)
+/4 width=6 by flifts_inv_lifts, lifts_trans, sym_eq/
+qed.
+
+(* Main derived properties with uniform relocation **************************)
+
+theorem flifts_compose_uni (l2) (l1) (T): ↑[l2]↑[l1]T = ↑[l2+l1]T.
+#l2 #l1 #T >flifts_compose
+/4 width=1 by flifts_inv_lifts, lifts_uni, sym_eq/ qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts_basic.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts_basic.ma
new file mode 100644 (file)
index 0000000..9b7f6fa
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts_basic.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 "apps_2/functional/flifts_flifts.ma".
+include "apps_2/functional/flifts_basic.ma".
+
+(* BASIC FUNCTIONAL RELOCATION **********************************************)
+
+(* Main properties **********************************************************)
+
+theorem flifts_basic_swap (T) (d1) (d2) (h1) (h2):
+                          d2 ≤ d1 → ↑[d2,h2]↑[d1,h1]T = ↑[h2+d1,h1]↑[d2,h2]T.
+/3 width=1 by flifts_comp, basic_swap/ qed-.
+(*
+lemma flift_join: ∀e1,e2,T. ⬆[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
+#e1 #e2 #T
+lapply (flift_lift T 0 (e1+e2)) #H
+elim (lift_split … H e1 e1) -H // #U #H
+>(flift_inv_lift … H) -H //
+qed.
+*)

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
new file mode 100644 (file)
index 0000000..6f2074d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "apps_2/notation/functional/blackcircle_3.ma".
+include "apps_2/functional/mf_vlift.ma".
+include "apps_2/functional/mf_vpush.ma".
+
+(* MULTIPLE FILLING FOR TERMS ***********************************************)
+
+rec definition mf gv lv T on T ≝ match T with
+[ TAtom I     ⇒ match I with
+  [ Sort _ ⇒ T
+  | LRef i ⇒ lv i
+  | GRef l ⇒ gv l
+  ]
+| TPair I V T ⇒ match I with
+  [ Bind2 _ _ ⇒ TPair I (mf gv lv V) (mf (⇡[0]gv) (⇡[0←#0]lv) T)
+  | Flat2 _   ⇒ TPair I (mf gv lv V) (mf gv lv T)
+  ]
+].
+
+interpretation "term filling (multiple filling)"
+  'BlackCircle gv lv T = (mf gv lv T).
+
+(* Basic Properties *********************************************************)
+
+lemma mf_sort: ∀gv,lv,s. ●[gv,lv]⋆s = ⋆s.
+// qed.
+
+lemma mf_lref: ∀gv,lv,i. ●[gv,lv]#i = lv i.
+// qed.
+
+lemma mf_gref: ∀gv,lv,l. ●[gv,lv]§l = gv l.
+// qed.
+
+lemma mf_bind (p) (I): ∀gv,lv,V,T.
+                       ●[gv,lv]ⓑ{p,I}V.T = ⓑ{p,I}●[gv,lv]V.●[⇡[0]gv,⇡[0←#0]lv]T.
+// qed.
+
+lemma mf_flat (I): ∀gv,lv,V,T.
+                   ●[gv,lv]ⓕ{I}V.T = ⓕ{I}●[gv,lv]V.●[gv,lv]T.
+// qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma
new file mode 100644 (file)
index 0000000..2e7f3d5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.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/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/cpr.ma".
+include "apps_2/functional/mf_exteq.ma".
+
+(* MULTIPLE FILLING FOR TERMS ***********************************************)
+
+(* Properties with relocation ***********************************************)
+
+lemma mf_delta_drops (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 →
+                              ∀T,L,l. ⬇*[l] L ≘ K.ⓓV1 →
+                              ∀gv,lv. ⦃G, L⦄ ⊢ ●[gv,⇡[l←#l]lv]T ➡[h] ●[gv,⇡[l←↑[↑l]V2]lv]T.
+#h #G #K #V1 #V2 #HV #T elim T -T * //
+[ #i #L #l #HKL #gv #lv
+  >mf_lref >mf_lref
+  elim (lt_or_eq_or_gt i l) #Hl destruct
+  [ >(mf_vpush_lt … Hl) >(mf_vpush_lt … Hl) //
+  | >mf_vpush_eq >mf_vpush_eq
+    /2 width=6 by cpm_delta_drops/
+  | >(mf_vpush_gt … Hl) >(mf_vpush_gt … Hl) //
+  ]
+| #p #I #V #T #IHV #IHT #L #l #HLK #gv #lv
+  >mf_bind >mf_bind
+  >(mf_comp … T) in ⊢ (?????%?);
+  [2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
+  >(mf_comp … T) in ⊢ (??????%);
+  [2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
+  >(flifts_lref_uni 1 l) >(flifts_compose_uni 1 (↑l))
+  /4 width=1 by cpm_bind, drops_drop/
+| #I #V #T #IHV #IHT #L #l #HLK #gv #lv
+  >mf_flat >mf_flat /3 width=1 by cpr_flat/
+]
+qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma
new file mode 100644 (file)
index 0000000..0f6975a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "apps_2/functional/mf_vlift_exteq.ma".
+include "apps_2/functional/mf_vpush_exteq.ma".
+include "apps_2/functional/mf.ma".
+
+(* MULTIPLE FILLING FOR TERMS ***********************************************)
+
+(* Properties with extensional equivalence **********************************)
+
+lemma mf_comp (T): compatible_3 … (λgv,lv.●[gv,lv]T) (exteq …) (exteq …) (eq …).
+#T elim T -T *
+[ //
+| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+  whd in ⊢ (??%%); //
+| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+  whd in ⊢ (??%%); //
+| #p #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+  whd in ⊢ (??%%); /4 width=1 by mf_vlift_comp, mf_vpush_comp, eq_f3/
+| #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+  whd in ⊢ (??%%); /3 width=1 by eq_f3/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma mf_id (T): ●[mf_gi,mf_li]T = T.
+#T elim T -T * //
+[ #p #I #V #T #IHV #IHT
+  <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
+  whd in ⊢ (??%?); /3 width=1 by mf_comp, eq_f3/
+| #I #V #T #IHV #IHT
+  <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT //
+]
+qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_lifts.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_lifts.ma
new file mode 100644 (file)
index 0000000..2509377
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_lifts.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "apps_2/functional/mf_vpush_vlift.ma".
+include "apps_2/functional/mf_exteq.ma".
+
+(* MULTIPLE FILLING FOR TERMS ***********************************************)
+
+(* Properties with relocation ***********************************************)
+
+lemma mf_lifts_basic_SO_dx (T) (j): ∀gv,lv. ↑[j,1]●[gv,lv]T = ●[⇡[j]gv,⇡[j]lv]T.
+#T elim T -T * //
+[ #p #I #V #T #IHV #IHT #j #gv #lv
+  >mf_bind >mf_bind >flifts_basic_bind
+  /4 width=1 by mf_comp, mf_vlift_swap, eq_f2/
+| #I #V #T #IHV #IHT #j #gv #lv
+  >mf_flat >mf_flat >flifts_flat
+  //
+]
+qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_v.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_v.ma
new file mode 100644 (file)
index 0000000..fbe6c55
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_v.ma
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/syntax/term.ma".
+
+(* MULTIPLE FILLING EVALUATION **********************************************)
+
+definition mf_evaluation ≝ nat → term.
+
+definition mf_li: mf_evaluation ≝ λi.#i.
+
+definition mf_gi: mf_evaluation ≝ λl.§l.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift.ma
new file mode 100644 (file)
index 0000000..d6b3e51
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift.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 "apps_2/notation/functional/dotteduparrow_2.ma".
+include "apps_2/functional/flifts_basic.ma".
+include "apps_2/functional/mf_v.ma".
+
+(* MULTIPLE EVALUATION LIFT *************************************************)
+
+definition mf_vlift (j) (gv): mf_evaluation ≝ λi. ↑[j,1](gv i).
+
+interpretation "lift (multiple_filling)"
+  'DottedUpArrow i gv = (mf_vlift i gv).
+
+(* Basic properties *********************************************************)
+
+lemma mf_vlift_rw (j) (gv): ∀i. (⇡[j]gv) i = ↑[j,1](gv i).
+// qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
new file mode 100644 (file)
index 0000000..79a5bbf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lib/functions.ma".
+include "ground_2/lib/exteq.ma".
+include "apps_2/functional/flifts_flifts_basic.ma".
+include "apps_2/functional/mf_vlift.ma".
+
+(* MULTIPLE EVALUATION LIFT *************************************************)
+
+(* Properties with extensional equivalence **********************************)
+
+lemma mf_gc_id: ∀j. ⇡[j]mf_gi ≐ mf_gi.
+// qed.
+
+lemma mf_vlift_comp (l): compatible_2 … (mf_vlift l) (exteq …) (exteq …).
+#l #gv1 #gv2 #Hgv #i
+>mf_vlift_rw >mf_vlift_rw //
+qed.
+
+(* Main properties with extensional equivalence *****************************)
+
+theorem mf_vlift_swap: ∀l1,l2. l2 ≤ l1 → ∀v. ⇡[l2]⇡[l1]v ≐ ⇡[↑l1]⇡[l2]v.
+/2 width=1 by flifts_basic_swap/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush.ma
new file mode 100644 (file)
index 0000000..0a76650
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "apps_2/notation/functional/dotteduparrow_3.ma".
+include "apps_2/functional/flifts_basic.ma".
+include "apps_2/functional/mf_v.ma".
+
+(* MULTIPLE FILLING PUSH ****************************************************)
+
+definition mf_vpush (j) (T) (lv): mf_evaluation ≝
+                    λi. tri … i j (lv i) T (↑[j,1](lv (↓i))).
+
+interpretation "push (multiple filling)"
+  'DottedUpArrow i d lv = (mf_vpush i d lv).
+
+(* Basic properties *********************************************************)
+
+lemma mf_vpush_lt (lv) (j) (T): ∀i. i < j → (⇡[j←T]lv) i = lv i.
+/2 width=1 by tri_lt/ qed-.
+
+lemma mf_vpush_eq: ∀lv,T,i. (⇡[i←T]lv) i = T.
+/2 width=1 by tri_eq/ qed.
+
+lemma mf_vpush_gt: ∀lv,T,j,i. j < i → (⇡[j←T]lv) i = ↑[j,1](lv (↓i)).
+/2 width=1 by tri_gt/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
new file mode 100644 (file)
index 0000000..a36a122
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lib/functions.ma".
+include "ground_2/lib/exteq.ma".
+include "apps_2/functional/flifts_flifts_basic.ma".
+include "apps_2/functional/mf_vpush.ma".
+
+(* MULTIPLE FILLING PUSH ****************************************************)
+
+(* Properties with extensional equivalence **********************************)
+
+lemma mf_lc_id: ⇡[0←#0]mf_li ≐ mf_li.
+#i elim (eq_or_gt i) #Hi destruct //
+>mf_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
+qed.
+
+lemma mf_vpush_comp (i): compatible_3 … (mf_vpush i) (eq …) (exteq …) (exteq …).
+#i #T1 #T2 #HT12 #lv1 #lv2 #Hlv #j
+elim (lt_or_eq_or_gt j i) #Hij destruct
+[ >mf_vpush_lt // >mf_vpush_lt //
+| >mf_vpush_eq >mf_vpush_eq //
+| >mf_vpush_gt // >mf_vpush_gt //
+]
+qed-.
+
+(* Main properties with extensional equivalence *****************************)
+
+theorem mf_vpush_swap: ∀l1,l2. l2 ≤ l1 →
+                       ∀v,T1,T2. ⇡[l2←T2]⇡[l1←T1]v ≐ ⇡[↑l1←↑[l2,1]T1]⇡[l2←T2]v.
+#l1 #l2 #Hl21 #v #T1 #T2 #i
+elim (lt_or_eq_or_gt i l2) #Hl2 destruct
+[ lapply (lt_to_le_to_lt … Hl2 Hl21) #Hl1
+  >mf_vpush_lt // >mf_vpush_lt // >mf_vpush_lt /2 width=1 by lt_S/ >mf_vpush_lt //
+| >mf_vpush_eq >mf_vpush_lt /2 width=1 by monotonic_le_plus_l/
+| >mf_vpush_gt // elim (lt_or_eq_or_gt (↓i) l1) #Hl1 destruct
+  [ >mf_vpush_lt // >mf_vpush_lt /2 width=1 by lt_minus_to_plus/ >mf_vpush_gt //
+  | >mf_vpush_eq <(lt_succ_pred … Hl2) >mf_vpush_eq //
+  | lapply (le_to_lt_to_lt … Hl21 Hl1) -Hl2 #Hl2
+    >mf_vpush_gt // >mf_vpush_gt /2 width=1 by lt_minus_to_plus_r/ >mf_vpush_gt //
+    /2 width=1 by flifts_basic_swap/
+  ]
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
new file mode 100644 (file)
index 0000000..c1f6e76
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "apps_2/functional/mf_vlift_exteq.ma".
+include "apps_2/functional/mf_vpush.ma".
+
+(* MULTIPLE FILLING PUSH ****************************************************)
+
+(* Properties with multiple filling lift ************************************)
+
+lemma mf_vpush_vlift_swap_O (v) (T) (l): ⇡[0←↑[↑l,1]T]⇡[l]v ≐⇡[↑l]⇡[0←T]v.
+#v #T #l #i
+elim (eq_or_gt i) #Hi destruct
+[ >mf_vpush_eq >mf_vlift_rw >mf_vpush_eq //
+| >(mf_vpush_gt … Hi) >mf_vlift_rw >mf_vlift_rw >(mf_vpush_gt … Hi)
+  @mf_vlift_swap //
+]
+qed.
+
+lemma mf_vpush_vlift_swap_O_lref_O (v) (l): ⇡[0←#0]⇡[l]v ≐⇡[↑l]⇡[0←#0]v.
+#v #l @(mf_vpush_vlift_swap_O … (#0))
+qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.ma
deleted file mode 100644 (file)
index 0047ad2..0000000
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.ma
+++ /dev/null
@@ -1,67 +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 "ground_2/lib/functions.ma".
-include "ground_2/lib/exteq.ma".
-include "apps_2/models/tm.ma".
-
-(* TERM MODEL ***************************************************************)
-
-(* Properties with extensional equivalencs of evaluations *******************) 
-
-lemma tm_gc_id: ∀j. ⇡[j]tm_gc ≐ tm_gc.
-// qed.
-
-lemma tm_lc_id: ⇡[0←#0]tm_lc ≐ tm_lc.
-#i elim (eq_or_gt i) #Hi destruct //
->tm_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
-qed.
-
-lemma tm_vlift_comp (l): compatible_2 … (tm_vlift l) (exteq …) (exteq …).
-#l #gv1 #gv2 #Hgv #i
->tm_vlift_rw >tm_vlift_rw //
-qed.
-
-lemma tm_vpush_comp (i): compatible_3 … (tm_vpush i) (eq …) (exteq …) (exteq …).
-#i #T1 #T2 #HT12 #lv1 #lv2 #Hlv #j
-elim (lt_or_eq_or_gt j i) #Hij destruct
-[ >tm_vpush_lt // >tm_vpush_lt //
-| >tm_vpush_eq >tm_vpush_eq //
-| >tm_vpush_gt // >tm_vpush_gt //
-]
-qed-.
-
-lemma tm_ti_comp (T): compatible_3 … (λgv,lv.tm_ti gv lv T) (exteq …) (exteq …) (eq …).
-#T elim T -T *
-[ //
-| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
-  whd in ⊢ (??%%); //
-| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
-  whd in ⊢ (??%%); //
-| #p #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
-  whd in ⊢ (??%%); /4 width=1 by tm_vlift_comp, tm_vpush_comp, eq_f3/
-| #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
-  whd in ⊢ (??%%); /3 width=1 by eq_f3/
-]
-qed-.
-
-lemma tm_ti_eq (T): tm_ti tm_gc tm_lc T = T.
-#T elim T -T * //
-[ #p #I #V #T #IHV #IHT
-  <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
-  whd in ⊢ (??%?); /3 width=1 by tm_ti_comp, eq_f3/
-| #I #V #T #IHV #IHT
-  <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT //
-]
-qed.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/functional/blackcircle_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/blackcircle_3.ma
new file mode 100644 (file)
index 0000000..899b0f6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/blackcircle_3.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation "hvbox( ●[ term 46 gv, break term 46 lv ] break term 46 T )"
+   non associative with precedence 46
+   for @{ 'BlackCircle $gv $lv $T }.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_2.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_2.ma
new file mode 100644 (file)
index 0000000..20d2d6e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation "hvbox( ⇡[ term 46 i ] break term 46 gv )"
+   non associative with precedence 46
+   for @{ 'DottedUpArrow $i $gv }.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_3.ma
new file mode 100644 (file)
index 0000000..3ffe16f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_3.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation "hvbox( ⇡[ term 46 i ← break term 46 d ] break term 46 lv )"
+   non associative with precedence 46
+   for @{ 'DottedUpArrow $i $d $lv }.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_2.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_2.ma
deleted file mode 100644 (file)
index 20d2d6e..0000000
--- a/matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE "models" COMPONENT **************************************)
-
-notation "hvbox( ⇡[ term 46 i ] break term 46 gv )"
-   non associative with precedence 46
-   for @{ 'DottedUpArrow $i $gv }.

diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_3.ma
deleted file mode 100644 (file)
index 3ffe16f..0000000
--- a/matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_3.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE "models" COMPONENT **************************************)
-
-notation "hvbox( ⇡[ term 46 i ← break term 46 d ] break term 46 lv )"
-   non associative with precedence 46
-   for @{ 'DottedUpArrow $i $d $lv }.

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 747b554ad7fa1cd4c3e8e349b9e84746b11197d7..6010578f44c5715bbc2bc0ff5eafc16cf1bb3c2e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
@@ -12,9 +12,7 @@ table {
    class "yellow"
    [ { "models" * } {
         [ { "term model" * } {
    class "yellow"
    [ { "models" * } {
         [ { "term model" * } {

-             [ "tm" + "( ⇡[?]? )" + "( ⇡[?←?]? )"
-               "tm_exteq"
-             * ]
+             [ "tm" * ]

           }
         ]
         [ { "denotational equivalence" * } {
           }
         ]
         [ { "denotational equivalence" * } {


@@ -54,16 +52,16 @@ table {
 *)
    class "orange"
    [ { "functional" * } {
 *)
    class "orange"
    [ { "functional" * } {

-(*
-        [ { "reduction and type machine" * } {
-             [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+        [ { "multiple filling" * } {
+             [ "mf" + "( ●[?,?]? )" "mf_exeq" "mf_lifts" "mf_cpr" *]
+             [ "mf_vpush" + "( ⇡[?←?]? )" "mf_vpush_exteq" "mf_vpush_vlift" * ]
+             [ "mf_vlift" + "( ⇡[?]? )" "mf_vlift_exteq" * ]
+             [ "mf_v" * ]

           }
         ]
           }
         ]

-*)

         [ { "relocation" * } {
         [ { "relocation" * } {

-             [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )"
-               "flifts_basic" + "( ↑[?,?]? )"
-             * ]
+             [ "flifts_basic" + "( ↑[?,?]? )" "flifts_flifts_basic" * ]
+             [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )" "flifts_flifts" * ]

           }
         ]
      }
           }
         ]
      }


@@ -88,4 +86,8 @@ class "italic"            { 1 }
              [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
           }
         ]
              [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
           }
         ]

+        [ { "reduction and type machine" * } {
+             [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+          }
+        ]        

 *)
 *)

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 6dd729c310f5a8453e6dec587a97736424387ea6..9efd9a61b908171086989a4ad2ae3a15214f34cd 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1562,7 +1562,7 @@ let predefined_classes = [
  ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
  ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
  ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ;
  ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
  ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
  ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ;

- ["o"; "θ"; "ϑ"; "𝕠"; "∘";  "⊚"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ;
+ ["o"; "θ"; "ϑ"; "𝕠"; "∘";  "⊚"; "ø"; "○"; "●"; "𝐨"; "𝛉"; "ⓞ"; ] ;

  ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ;
  ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ;
  ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ;
  ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ;
  ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ;
  ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ;