From: Ferruccio Guidi Date: Thu, 19 Jul 2018 15:00:59 +0000 (+0200) Subject: update in functional X-Git-Tag: make_still_working~296 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea918ec7701db4458c5ca25885e80abc6fed1be7;p=helm.git 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 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/functional/mf_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma new file mode 100644 index 000000000..0f6975a73 --- /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 + 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/models/tm_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.ma deleted file mode 100644 index 0047ad29f..000000000 --- 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 -