From ea918ec7701db4458c5ca25885e80abc6fed1be7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 19 Jul 2018 17:00:59 +0200 Subject: [PATCH] update in functional + support for multiple filling --- .../lambdadelta/apps_2/functional/flifts.ma | 24 +++++--- .../apps_2/functional/flifts_basic.ma | 14 ++++- .../apps_2/functional/flifts_flifts.ma | 33 +++++++++++ .../apps_2/functional/flifts_flifts_basic.ma | 32 +++++++++++ .../lambdadelta/apps_2/functional/mf.ma | 53 ++++++++++++++++++ .../lambdadelta/apps_2/functional/mf_cpr.ma | 46 ++++++++++++++++ .../tm_exteq.ma => functional/mf_exteq.ma} | 42 ++++---------- .../lambdadelta/apps_2/functional/mf_lifts.ma | 31 +++++++++++ .../lambdadelta/apps_2/functional/mf_v.ma | 23 ++++++++ .../lambdadelta/apps_2/functional/mf_vlift.ma | 29 ++++++++++ .../apps_2/functional/mf_vlift_exteq.ma | 35 ++++++++++++ .../lambdadelta/apps_2/functional/mf_vpush.ma | 36 ++++++++++++ .../apps_2/functional/mf_vpush_exteq.ma | 55 +++++++++++++++++++ .../apps_2/functional/mf_vpush_vlift.ma | 33 +++++++++++ .../notation/functional/blackcircle_3.ma | 19 +++++++ .../{models => functional}/dotteduparrow_2.ma | 0 .../{models => functional}/dotteduparrow_3.ma | 0 .../lambdadelta/apps_2/web/apps_2_src.tbl | 22 ++++---- matita/matita/predefined_virtuals.ml | 2 +- 19 files changed, 477 insertions(+), 52 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts_basic.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma rename matita/matita/contribs/lambdadelta/apps_2/{models/tm_exteq.ma => functional/mf_exteq.ma} (57%) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf_lifts.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf_v.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/functional/blackcircle_3.ma rename matita/matita/contribs/lambdadelta/apps_2/notation/{models => functional}/dotteduparrow_2.ma (100%) rename matita/matita/contribs/lambdadelta/apps_2/notation/{models => functional}/dotteduparrow_3.ma (100%) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma index edc607bbc..30b8b6517 100644 --- 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). +(* 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. @@ -55,13 +66,10 @@ qed-. (* 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 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 f3e6c31dd..5c50fb1af 100644 --- 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". -(* GENERIC FUNCTIONAL RELOCATION ********************************************) +(* BASIC FUNCTIONAL RELOCATION **********************************************) 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 index 000000000..de4b424e9 --- /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 index 000000000..9b7f6fa2b --- /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 index 000000000..6f2074db5 --- /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 index 000000000..2e7f3d5ef --- /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/models/tm_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma similarity index 57% rename from matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.ma rename to matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma index 0047ad29f..0f6975a73 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma @@ -12,37 +12,15 @@ (* *) (**************************************************************************) -include "ground_2/lib/functions.ma". -include "ground_2/lib/exteq.ma". -include "apps_2/models/tm.ma". +include "apps_2/functional/mf_vlift_exteq.ma". +include "apps_2/functional/mf_vpush_exteq.ma". +include "apps_2/functional/mf.ma". -(* TERM MODEL ***************************************************************) +(* MULTIPLE FILLING FOR TERMS ***********************************************) -(* Properties with extensional equivalencs of evaluations *******************) +(* Properties with extensional equivalence **********************************) -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 …). +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 @@ -50,17 +28,19 @@ lemma tm_ti_comp (T): compatible_3 … (λgv,lv.tm_ti gv lv T) (exteq …) (exte | #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/ + 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-. -lemma tm_ti_eq (T): tm_ti tm_gc tm_lc T = T. +(* Advanced properties ******************************************************) + +lemma mf_id (T): ●[mf_gi,mf_li]T = T. #T elim T -T * // [ #p #I #V #T #IHV #IHT 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 index 000000000..fbe6c5507 --- /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 index 000000000..d6b3e51d1 --- /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 index 000000000..79a5bbf37 --- /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 index 000000000..0a766506e --- /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 index 000000000..a36a12292 --- /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 index 000000000..c1f6e76ce --- /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/notation/functional/blackcircle_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/blackcircle_3.ma new file mode 100644 index 000000000..899b0f68f --- /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/models/dotteduparrow_2.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_2.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_2.ma rename to matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_2.ma diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_3.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_3.ma rename to matita/matita/contribs/lambdadelta/apps_2/notation/functional/dotteduparrow_3.ma 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 747b554ad..6010578f4 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 @@ -12,9 +12,7 @@ table { class "yellow" [ { "models" * } { [ { "term model" * } { - [ "tm" + "( ⇡[?]? )" + "( ⇡[?←?]? )" - "tm_exteq" - * ] + [ "tm" * ] } ] [ { "denotational equivalence" * } { @@ -54,16 +52,16 @@ table { *) 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" * } { - [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )" - "flifts_basic" + "( ↑[?,?]? )" - * ] + [ "flifts_basic" + "( ↑[?,?]? )" "flifts_flifts_basic" * ] + [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )" "flifts_flifts" * ] } ] } @@ -88,4 +86,8 @@ class "italic" { 1 } [ "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 6dd729c31..9efd9a61b 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1562,7 +1562,7 @@ let predefined_classes = [ ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ; ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ; ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ; - ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ; + ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "●"; "𝐨"; "𝛉"; "ⓞ"; ] ; ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ; ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ; ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ; -- 2.39.2