From cc6fcb70ca4f3cf01205ed722d75a2fdb2aaf779 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 13 Jul 2018 17:34:46 +0200 Subject: [PATCH] update in static_2 and app_2 + term model started + functional relocation reactivated + some renaming --- .../functional/notation.etc} | 4 - .../rtm.ma => etc/functional/rtm.etc} | 0 .../functional/rtm_step.etc} | 0 .../apps_2/etc/models/model_ext.etc | 18 ---- .../apps_2/functional/{lift.ma => flifts.ma} | 51 +++++------ .../apps_2/functional/flifts_basic.ma | 22 +++++ .../lambdadelta/apps_2/models/deq_cpr.ma | 18 ++-- .../contribs/lambdadelta/apps_2/models/li.ma | 2 +- .../lambdadelta/apps_2/models/model_props.ma | 10 +- .../models/{model_vlift.ma => model_vpush.ma} | 12 +-- .../contribs/lambdadelta/apps_2/models/tm.ma | 91 +++++++++++++++++++ .../lambdadelta/apps_2/models/tm_exteq.ma | 67 ++++++++++++++ .../lambdadelta/apps_2/models/tm_props.ma | 54 +++++++++++ .../contribs/lambdadelta/apps_2/models/veq.ma | 30 +++--- .../lambdadelta/apps_2/models/veq_lifts.ma | 16 ++-- .../apps_2/models/{vlifts.ma => vpushs.ma} | 50 +++++----- .../{vlifts_shift.ma => vpushs_fold.ma} | 46 +++++----- .../apps_2/notation/functional/uparrow_2.ma | 19 ++++ .../apps_2/notation/functional/uparrow_3.ma | 19 ++++ .../apps_2/notation/models/dotteduparrow_2.ma | 19 ++++ .../apps_2/notation/models/dotteduparrow_3.ma | 19 ++++ .../lambdadelta/apps_2/web/apps_2_src.tbl | 24 +++-- .../matita/contribs/lambdadelta/partial.txt | 1 + .../lambdadelta/static_2/relocation/lifts.ma | 3 +- .../static_2/syntax/{shift.ma => fold.ma} | 16 ++-- .../lambdadelta/static_2/web/static_2_src.tbl | 2 +- 26 files changed, 455 insertions(+), 158 deletions(-) rename matita/matita/contribs/lambdadelta/apps_2/{functional/notation.ma => etc/functional/notation.etc} (91%) rename matita/matita/contribs/lambdadelta/apps_2/{functional/rtm.ma => etc/functional/rtm.etc} (100%) rename matita/matita/contribs/lambdadelta/apps_2/{functional/rtm_step.ma => etc/functional/rtm_step.etc} (100%) rename matita/matita/contribs/lambdadelta/apps_2/functional/{lift.ma => flifts.ma} (58%) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/functional/flifts_basic.ma rename matita/matita/contribs/lambdadelta/apps_2/models/{model_vlift.ma => model_vpush.ma} (81%) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/tm.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma rename matita/matita/contribs/lambdadelta/apps_2/models/{vlifts.ma => vpushs.ma} (76%) rename matita/matita/contribs/lambdadelta/apps_2/models/{vlifts_shift.ma => vpushs_fold.ma} (69%) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/functional/uparrow_2.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/functional/uparrow_3.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_2.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_3.ma rename matita/matita/contribs/lambdadelta/static_2/syntax/{shift.ma => fold.ma} (74%) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/notation.etc similarity index 91% rename from matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma rename to matita/matita/contribs/lambdadelta/apps_2/etc/functional/notation.etc index 172f475fa..800038120 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/notation.etc @@ -18,10 +18,6 @@ notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 non associative with precedence 50 for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. -notation "hvbox( ↑* [ term 46 f ] break term 46 T )" - non associative with precedence 46 - for @{ 'LiftStar $f $T }. - notation "hvbox( T1 ⇨ break term 46 T2 )" non associative with precedence 45 for @{ 'SRed $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma rename to matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm.etc diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm_step.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma rename to matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm_step.etc diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_ext.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_ext.etc index 8c6e9d7c8..ea34bcfb7 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_ext.etc +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_ext.etc @@ -3,14 +3,6 @@ include "ground_2/lib/exteq.ma". include "apps_2/models/model_li.ma". include "apps_2/models/vdrop.ma". -lemma vlift_ext (M): ∀i. compatible_3 … (vlift M i) (eq …) (exteq …) (exteq …). -#M #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j -elim (lt_or_eq_or_gt j i) #Hij destruct -[ >vlift_lt // >vlift_lt // -| >vlift_eq >vlift_eq // -| >vlift_gt // >vlift_gt // -] -qed. lemma vdrop_ext (M): ∀i. compatible_2 … (vdrop M i) (exteq …) (exteq …). #M #i #lv1 #lv2 #Hlv12 #j elim (lt_or_ge j i) #Hji @@ -66,13 +58,3 @@ lemma veq_repl_exteq (M): is_model M → lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv → ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2. // qed-. - -lemma ti_ext_l (M): is_model M → - ∀T,gv,lv1,lv2. lv1 ≐ lv2 → - ⟦T⟧[gv, lv1] ≗{M} ⟦T⟧[gv, lv2]. -/3 width=1 by ti_comp_l, ext_veq/ qed. - -lemma valign_ext (M) (l): compatible_2 … (valign M l) (exteq …) (exteq …). -#M #l #lv1 #lv2 #HLv12 #i ->valign_rw >valign_rw // -qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma similarity index 58% rename from matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma rename to matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma index ea7409060..edc607bbc 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma @@ -12,57 +12,56 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lift.ma". -include "apps_2/functional/notation.ma". +include "ground_2/notation/functions/uparrowstar_2.ma". +include "apps_2/notation/functional/uparrow_2.ma". +include "static_2/relocation/lifts.ma". -(* FUNCTIONAL RELOCATION ****************************************************) +(* GENERIC FUNCTIONAL RELOCATION ********************************************) -let rec flift d e U on U ≝ match U with +rec definition flifts f U on U ≝ match U with [ TAtom I ⇒ match I with [ Sort _ ⇒ U - | LRef i ⇒ #(tri … i d i (i + e) (i + e)) + | LRef i ⇒ #(f@❴i❵) | GRef _ ⇒ U ] | TPair I V T ⇒ match I with - [ Bind2 a I ⇒ ⓑ{a,I} (flift d e V). (flift (d+1) e T) - | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T) + [ Bind2 p I ⇒ ⓑ{p,I}(flifts f V).(flifts (⫯f) T) + | Flat2 I ⇒ ⓕ{I}(flifts f V).(flifts f T) ] ]. -interpretation "functional relocation" 'Lift d e T = (flift d e T). +interpretation "generic functional relocation (term)" + 'UpArrowStar f T = (flifts f T). + +interpretation "uniform functional relocation (term)" + 'UpArrow i T = (flifts (uni i) T). (* Main properties **********************************************************) -theorem flift_lift: ∀T,d,e. ⬆[d, e] T ≡ ↑[d, e] T. -#T elim T -T -[ * #i #d #e // - elim (lt_or_eq_or_gt i d) #Hid normalize - [ >(tri_lt ?????? Hid) /2 width=1/ - | /2 width=1/ - | >(tri_gt ?????? Hid) /3 width=2/ - ] -| * /2/ -] +theorem flifts_lifts: ∀T,f. ⬆*[f]T ≘ ↑*[f]T. +#T elim T -T * +/2 width=1 by lifts_sort, lifts_lref, lifts_gref, lifts_bind, lifts_flat/ qed. (* Main inversion properties ************************************************) -theorem flift_inv_lift: ∀d,e,T1,T2. ⬆[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2. -#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // -[ #i #d #e #Hid >(tri_lt ?????? Hid) // -| #i #d #e #Hid - elim (le_to_or_lt_eq … Hid) -Hid #Hid - [ >(tri_gt ?????? Hid) // - | destruct // - ] +theorem flifts_inv_lifts: ∀f,T1,T2. ⬆*[f]T1 ≘ T2 → ↑*[f]T1 = T2. +#f #T1 #T2 #H elim H -f -T1 -T2 // +[ #f #i1 #i2 #H <(at_inv_total … H) // +| #f #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT (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 new file mode 100644 index 000000000..f3e6c31dd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts_basic.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/rtmap_basic.ma". +include "apps_2/functional/flifts.ma". +include "apps_2/notation/functional/uparrow_3.ma". + +(* GENERIC FUNCTIONAL RELOCATION ********************************************) + +interpretation "basic functional relocation (term)" + 'UpArrow d h T = (flifts (basic d h) T). diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma b/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma index 6acf720cb..c0d19aefc 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/deq_cpr.ma @@ -29,19 +29,19 @@ lemma cpr_fwd_deq (h) (M): is_model M → is_extensional M → @(mq … H1M) [4,5: @(ti_comp … H) /2 width=2 by veq_refl/ |1,2: skip ] -v @(mq … H1M) [4: /3 width=1 by seq_sym, ml/ | skip - |5: /2 width=2 by lifts_SO_fwd_vlift/ | skip ] -W2 - >vlift_eq /2 width=1 by/ + |5: /2 width=2 by lifts_SO_fwd_vpush/ | skip ] -W2 + >vpush_eq /2 width=1 by/ | #I #G #K #T #U #i #_ #IH #HTU #gv #v #H elim (li_fwd_bind … H) // -H #lv #d #HK #H @(mq … H1M) [4,5: @(ti_comp … H) /2 width=2 by veq_refl/ |1,2: skip ] -v @(mq … H1M) [4: /3 width=1 by seq_sym, ml/ | skip - |5: /2 width=2 by lifts_SO_fwd_vlift/ | skip ] -U - >vlift_gt /3 width=5 by ml, mq, mr/ + |5: /2 width=2 by lifts_SO_fwd_vpush/ | skip ] -U + >vpush_gt /3 width=5 by ml, mq, mr/ | #p * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv [ @(mq … H1M) [4,5: /3 width=2 by seq_sym, md/ |1,2: skip ] -p @(seq_trans … H1M) [2: @IHT /2 width=1 by li_abbr/ | skip ] -T1 - /4 width=1 by ti_comp, vlift_comp, (* 2x *) veq_refl/ + /4 width=1 by ti_comp, vpush_comp, (* 2x *) veq_refl/ | /4 width=1 by li_abst, mx/ ] | * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv @@ -54,7 +54,7 @@ lemma cpr_fwd_deq (h) (M): is_model M → is_extensional M → @(mq … H1M) [4: /3 width=2 by seq_sym, md/ | skip |3: /3 width=1 by li_abbr/ | skip ] -L -U1 - /3 width=1 by lifts_SO_fwd_vlift, seq_sym/ + /3 width=1 by lifts_SO_fwd_vpush, seq_sym/ | #G #L #V #T1 #T2 #_ #IH #gv #lv #Hlv @(seq_trans … H1M) [2: @(me … H1M) | skip ] /2 width=1 by/ @@ -64,16 +64,16 @@ lemma cpr_fwd_deq (h) (M): is_model M → is_extensional M → [4: /3 width=2 by seq_sym, mb/ | skip |5: @IHT /2 width=1 by li_abst/ | skip ] -T2 @ti_comp /2 width=1 by veq_refl/ - @vlift_comp /2 width=1 by veq_refl/ + @vpush_comp /2 width=1 by veq_refl/ @(mq … H1M) [4,5: /3 width=2 by seq_sym, me/ |1,2: skip ] -L -V1 /2 width=1 by mr/ | #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #IHW #IHT #HV2 #gv #lv #Hlv @(mq … H1M) [4,5: /3 width=2 by seq_sym, ma, md/ |1,2: skip ] @(seq_trans … H1M) [3: /3 width=1 by seq_sym, ma/ | skip ] - @mp // [ @(seq_trans … H1M) /3 width=3 by lifts_SO_fwd_vlift/ ] -V1 -V -V2 + @mp // [ @(seq_trans … H1M) /3 width=3 by lifts_SO_fwd_vpush/ ] -V1 -V -V2 @(mq … H1M) [4: /3 width=2 by seq_sym, md/ | skip |3: @IHT /2 width=1 by li_abbr/ | skip ] -T1 - /4 width=1 by ti_comp, vlift_comp, (* 2x *) veq_refl/ + /4 width=1 by ti_comp, vpush_comp, (* 2x *) veq_refl/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma index f0f2c0f63..4d36f1427 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma @@ -113,7 +113,7 @@ lemma li_repl (M) (L): is_model M -> | #lv1 #d #K #V #_ #Hd #IH #gv2 #Hgv #lv2 #Hlv destruct @li_veq [2: /4 width=4 by li_abbr, veq_refl/ | skip ] -IH @(veq_canc_sn … Hlv) -Hlv // - /4 width=1 by ti_comp, vlift_comp, (* 2x *) veq_refl/ + /4 width=1 by ti_comp, vpush_comp, (* 2x *) veq_refl/ | #lv1 #d #K #W #_ #IH #gv2 #Hgv #lv2 #Hlv @li_veq /4 width=3 by li_abst, veq_refl/ | #lv1 #d #I #K #_ #IH #gv2 #Hgv #lv2 #Hlv diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma index 26a347832..346917ff8 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "apps_2/models/model_vlift.ma". +include "apps_2/models/model_vpush.ma". (* MODEL ********************************************************************) @@ -64,18 +64,18 @@ lemma seq_canc_sn (M): is_model M → left_cancellable … (sq M). lemma seq_canc_dx (M): is_model M → right_cancellable … (sq M). /3 width=3 by seq_trans, seq_sym/ qed-. -lemma ti_lref_vlift_eq (M): is_model M → +lemma ti_lref_vpush_eq (M): is_model M → ∀gv,lv,d,i. ⟦#i⟧[gv,⫯[i←d]lv] ≗{M} d. #M #HM #gv #lv #d #i @(seq_trans … HM) [2: @ml // | skip ] ->vlift_eq /2 width=1 by mr/ +>vpush_eq /2 width=1 by mr/ qed. -lemma ti_lref_vlift_gt (M): is_model M → +lemma ti_lref_vpush_gt (M): is_model M → ∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[0←d]lv] ≗{M} ⟦#i⟧[gv,lv]. #M #HM #gv #lv #d #i @(mq … HM) [4,5: @(seq_sym … HM) /2 width=2 by ml/ |1,2: skip ] ->vlift_gt /2 width=1 by mr/ +>vpush_gt /2 width=1 by mr/ qed. (* Basic Forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_vpush.ma similarity index 81% rename from matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma rename to matita/matita/contribs/lambdadelta/apps_2/models/model_vpush.ma index bb2d5c7c9..ccf633e6e 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_vpush.ma @@ -18,19 +18,19 @@ include "apps_2/models/model.ma". (* MODEL ********************************************************************) -definition vlift (M): nat → dd M → evaluation M → evaluation M ≝ +definition vpush (M): nat → dd M → evaluation M → evaluation M ≝ λj,d,lv,i. tri … i j (lv i) d (lv (↓i)). -interpretation "lift (model evaluation)" - 'UpSpoon M i d lv = (vlift M i d lv). +interpretation "push (model evaluation)" + 'UpSpoon M i d lv = (vpush M i d lv). (* Basic properties *********************************************************) -lemma vlift_lt (M): ∀lv,d,j,i. i < j → (⫯{M}[j←d] lv) i = lv i. +lemma vpush_lt (M): ∀lv,d,j,i. i < j → (⫯{M}[j←d] lv) i = lv i. /2 width=1 by tri_lt/ qed-. -lemma vlift_eq (M): ∀lv,d,i. (⫯{M}[i←d] lv) i = d. +lemma vpush_eq (M): ∀lv,d,i. (⫯{M}[i←d] lv) i = d. /2 width=1 by tri_eq/ qed-. -lemma vlift_gt (M): ∀lv,d,j,i. j < i → (⫯{M}[j←d] lv) i = lv (↓i). +lemma vpush_gt (M): ∀lv,d,j,i. j < i → (⫯{M}[j←d] lv) i = lv (↓i). /2 width=1 by tri_gt/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma new file mode 100644 index 000000000..2a630c592 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma @@ -0,0 +1,91 @@ +(**************************************************************************) +(* ___ *) +(* ||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_equivalence/cpcs.ma". +include "apps_2/functional/flifts_basic.ma". +include "apps_2/models/model.ma". +include "apps_2/notation/models/dotteduparrow_2.ma". +include "apps_2/notation/models/dotteduparrow_3.ma". + +(* TERM MODEL ***************************************************************) + +definition tm_dd ≝ term. + +definition tm_evaluation ≝ nat → tm_dd. + +definition tm_sq (h) (T1) (T2) ≝ ⦃⋆, ⋆⦄ ⊢ T1 ⬌*[h] T2. + +definition tm_sv (s) ≝ ⋆s. + +definition tm_ap (V) (T) ≝ ⓐV.T. + +definition tm_vlift (j) (gv): tm_evaluation ≝ λi. ↑[j,1](gv i). + +interpretation "lift (term model evaluation)" + 'DottedUpArrow i gv = (tm_vlift i gv). + +definition tm_vpush (j) (T) (lv): tm_evaluation ≝ + λi. tri … i j (lv i) T (↑[j,1](lv (↓i))). + +interpretation "push (term model evaluation)" + 'DottedUpArrow i d lv = (tm_vpush i d lv). + +rec definition tm_ti 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 (tm_ti gv lv V) (tm_ti (⇡[0]gv) (⇡[0←#0]lv) T) + | Flat2 _ ⇒ TPair I (tm_ti gv lv V) (tm_ti gv lv T) + ] +]. + +definition tm_lc: tm_evaluation ≝ λi.#i. + +definition tm_gc: tm_evaluation ≝ λl.§l. + +definition TM (h): model ≝ mk_model … . +[ @tm_dd +| @(tm_sq h) |6,7: skip +| @tm_sv +| @tm_ap +| @tm_ti +]. +defined-. + +(* Basic properties *********************************************************) + +lemma tm_vlift_rw (j) (gv): ∀i. (⇡[j]gv) i = ↑[j,1](gv i). +// qed. + +lemma tm_vpush_lt (lv) (j) (T): ∀i. i < j → (⇡[j←T]lv) i = lv i. +/2 width=1 by tri_lt/ qed-. + +lemma tm_vpush_eq: ∀lv,T,i. (⇡[i←T]lv) i = T. +/2 width=1 by tri_eq/ qed. + +lemma tm_vpush_gt: ∀lv,T,j,i. j < i → (⇡[j←T]lv) i = ↑[j,1](lv (↓i)). +/2 width=1 by tri_gt/ qed-. + +lemma tm_ti_lref (h): ∀gv,lv,i. ⟦#i⟧{TM h}[gv,lv] = lv i. +// qed. + +lemma tm_ti_gref (h): ∀gv,lv,l. ⟦§l⟧{TM h}[gv,lv] = gv l. +// qed. + +lemma tm_ti_bind (h) (p) (I): ∀gv,lv,V,T. + ⟦ⓑ{p,I}V.T⟧{TM h}[gv,lv] = ⓑ{p,I}⟦V⟧[gv,lv].⟦T⟧{TM h}[⇡[0]gv,⇡[0←#0]lv]. +// 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 new file mode 100644 index 000000000..0047ad29f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_exteq.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* ___ *) +(* ||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 + tm_ti_lref >vpush_eq + >tm_ti_bind >tm_ti_lref >tm_vpush_eq + /5 width=3 by cpc_cpcs, cpm_zeta, cpm_delta, or_introl/ + | >tm_ti_lref >vpush_gt // + >tm_ti_bind >tm_ti_lref >tm_vpush_gt // + /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ + ] +| #l #V #gv #lv + >tm_ti_bind >tm_ti_gref >tm_ti_gref + /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ +| #p #I #W #T #IHW #IHT #V #gv #lv + >tm_ti_bind in ⊢ (???%); +(* + + >tm_ti_bind >tm_ti_bind + @cpc_cpcs @or_introl + @cpm_bind + + /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ + +definition is_tm (h): is_model (TM h) ≝ mk_is_model …. // +[ +| +| #gv #lv #p #V #T + @cpcs_cprs_dx + @cprs_step_sn + [2: @cpm_bind // | skip ] +*) diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma index 7f6e8b789..a351e2003 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -44,37 +44,37 @@ lemma veq_canc_sn (M): is_model M → left_cancellable … (veq M). lemma veq_canc_dx (M): is_model M → right_cancellable … (veq M). /3 width=3 by veq_trans, veq_sym/ qed-. -(* Properties with evaluation lift ******************************************) +(* Properties with evaluation push ******************************************) -theorem vlift_swap (M): is_model M → +theorem vpush_swap (M): is_model M → ∀i1,i2. i1 ≤ i2 → ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≗{M} ⫯[↑i2←d2] ⫯[i1←d1] lv. #M #HM #i1 #i2 #Hi12 #lv #d1 #d2 #j elim (lt_or_eq_or_gt j i1) #Hji1 destruct [ lapply (lt_to_le_to_lt … Hji1 Hi12) #Hji2 - >vlift_lt // >vlift_lt // >vlift_lt /2 width=1 by lt_S/ >vlift_lt // + >vpush_lt // >vpush_lt // >vpush_lt /2 width=1 by lt_S/ >vpush_lt // /2 width=1 by veq_refl/ -| >vlift_eq >vlift_lt /2 width=1 by monotonic_le_plus_l/ >vlift_eq +| >vpush_eq >vpush_lt /2 width=1 by monotonic_le_plus_l/ >vpush_eq /2 width=1 by mr/ -| >vlift_gt // elim (lt_or_eq_or_gt (↓j) i2) #Hji2 destruct - [ >vlift_lt // >vlift_lt /2 width=1 by lt_minus_to_plus/ >vlift_gt // +| >vpush_gt // elim (lt_or_eq_or_gt (↓j) i2) #Hji2 destruct + [ >vpush_lt // >vpush_lt /2 width=1 by lt_minus_to_plus/ >vpush_gt // /2 width=1 by veq_refl/ - | >vlift_eq <(lt_succ_pred … Hji1) >vlift_eq + | >vpush_eq <(lt_succ_pred … Hji1) >vpush_eq /2 width=1 by mr/ | lapply (le_to_lt_to_lt … Hi12 Hji2) #Hi1j - >vlift_gt // >vlift_gt /2 width=1 by lt_minus_to_plus_r/ >vlift_gt // + >vpush_gt // >vpush_gt /2 width=1 by lt_minus_to_plus_r/ >vpush_gt // /2 width=1 by veq_refl/ ] ] qed. -lemma vlift_comp (M): is_model M → - ∀i. compatible_3 … (vlift M i) (sq M) (veq M) (veq M). +lemma vpush_comp (M): is_model M → + ∀i. compatible_3 … (vpush M i) (sq M) (veq M) (veq M). #M #HM #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j elim (lt_or_eq_or_gt j i) #Hij destruct -[ >vlift_lt // >vlift_lt // -| >vlift_eq >vlift_eq // -| >vlift_gt // >vlift_gt // +[ >vpush_lt // >vpush_lt // +| >vpush_eq >vpush_eq // +| >vpush_gt // >vpush_gt // ] qed-. @@ -87,8 +87,8 @@ lemma ti_comp (M): is_model M → [ /4 width=5 by seq_trans, seq_sym, ms/ | /4 width=5 by seq_sym, ml, mq/ | /4 width=3 by seq_trans, seq_sym, mg/ -| /5 width=5 by vlift_comp, seq_sym, md, mq/ -| /5 width=1 by vlift_comp, mi, mr/ +| /5 width=5 by vpush_comp, seq_sym, md, mq/ +| /5 width=1 by vpush_comp, mi, mr/ | /4 width=5 by seq_sym, ma, mp, mq/ | /4 width=5 by seq_sym, me, mq/ ] diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma index dc83b79b1..943f8f5af 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq_lifts.ma @@ -20,7 +20,7 @@ include "apps_2/models/veq.ma". (* Forward lemmas with generic relocation ***********************************) -fact lifts_fwd_vlift_aux (M): is_model M → is_extensional M → +fact lifts_fwd_vpush_aux (M): is_model M → is_extensional M → ∀f,T1,T2. ⬆*[f] T1 ≘ T2 → ∀m. 𝐁❴m,1❵ = f → ∀gv,lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[m←d]lv]. #M #H1M #H2M #f #T1 #T2 #H elim H -f -T1 -T2 @@ -31,9 +31,9 @@ fact lifts_fwd_vlift_aux (M): is_model M → is_extensional M → @(mq … H1M) [4,5: /3 width=2 by seq_sym, ml/ |1,2: skip ] elim (lt_or_ge i1 m) #Hi1 [ lapply (at_basic_inv_lt … Hi12) -Hi12 // #H destruct - >vlift_lt /2 width=1 by mr/ + >vpush_lt /2 width=1 by mr/ | lapply (at_basic_inv_ge … Hi12) -Hi12 // #H destruct - >vlift_gt /2 width=1 by mr, le_S_S/ + >vpush_gt /2 width=1 by mr, le_S_S/ ] | #f #l #m #Hf #gv #lv #d @(mq … H1M) [4,5: /3 width=2 by seq_sym, mg/ |1,2: skip ] @@ -43,18 +43,18 @@ fact lifts_fwd_vlift_aux (M): is_model M → is_extensional M → @(seq_trans … H1M) [3: @ti_comp // | skip ] [1,2: /2 width=2 by veq_refl/ ] - [2: @(vlift_comp … H1M) | skip ] + [2: @(vpush_comp … H1M) | skip ] [1,2: /2 width=2 by/ |3,4: /2 width=2 by veq_refl/ ] -IHV @(seq_trans … H1M) [3: @ti_comp // | skip ] [1,2: /2 width=2 by veq_refl/ ] - [2: @veq_sym // @vlift_swap // | skip ] + [2: @veq_sym // @vpush_swap // | skip ] /2 width=1 by/ | @mx // [ /2 width=1 by/ ] -IHV #d0 @(seq_trans … H1M) [3: @ti_comp // | skip ] [1,2: /2 width=2 by veq_refl/ ] - [2: @veq_sym // @vlift_swap // | skip ] + [2: @veq_sym // @vpush_swap // | skip ] /2 width=1 by/ ] | #f * #V1 #v2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #gv #lv #d @@ -64,7 +64,7 @@ fact lifts_fwd_vlift_aux (M): is_model M → is_extensional M → ] qed-. -lemma lifts_SO_fwd_vlift (M) (gv): is_model M → is_extensional M → +lemma lifts_SO_fwd_vpush (M) (gv): is_model M → is_extensional M → ∀T1,T2. ⬆*[1] T1 ≘ T2 → ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[0←d]lv]. -/2 width=3 by lifts_fwd_vlift_aux/ qed-. +/2 width=3 by lifts_fwd_vpush_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma similarity index 76% rename from matita/matita/contribs/lambdadelta/apps_2/models/vlifts.ma rename to matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma index 81321cdac..dabd2c431 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma @@ -16,22 +16,22 @@ include "apps_2/notation/models/roplus_5.ma". include "static_2/syntax/lenv.ma". include "apps_2/models/veq.ma". -(* MULTIPLE LIFT FOR MODEL EVALUATIONS **************************************) +(* MULTIPLE PUSH FOR MODEL EVALUATIONS **************************************) -inductive vlifts (M) (gv) (lv): relation2 lenv (evaluation M) ≝ -| vlifts_atom: vlifts M gv lv (⋆) lv -| vlifts_abbr: ∀v,d,K,V. vlifts M gv lv K v → ⟦V⟧[gv, v] = d → vlifts M gv lv (K.ⓓV) (⫯[0←d]v) -| vlifts_abst: ∀v,d,K,V. vlifts M gv lv K v → vlifts M gv lv (K.ⓛV) (⫯[0←d]v) -| vlifts_unit: ∀v,d,I,K. vlifts M gv lv K v → vlifts M gv lv (K.ⓤ{I}) (⫯[0←d]v) -| vlifts_repl: ∀v1,v2,L. vlifts M gv lv L v1 → v1 ≗ v2 → vlifts M gv lv L v2 +inductive vpushs (M) (gv) (lv): relation2 lenv (evaluation M) ≝ +| vpushs_atom: vpushs M gv lv (⋆) lv +| vpushs_abbr: ∀v,d,K,V. vpushs M gv lv K v → ⟦V⟧[gv, v] = d → vpushs M gv lv (K.ⓓV) (⫯[0←d]v) +| vpushs_abst: ∀v,d,K,V. vpushs M gv lv K v → vpushs M gv lv (K.ⓛV) (⫯[0←d]v) +| vpushs_unit: ∀v,d,I,K. vpushs M gv lv K v → vpushs M gv lv (K.ⓤ{I}) (⫯[0←d]v) +| vpushs_repl: ∀v1,v2,L. vpushs M gv lv L v1 → v1 ≗ v2 → vpushs M gv lv L v2 . -interpretation "multiple lift (model evaluation)" - 'ROPlus M gv L lv v = (vlifts M gv lv L v). +interpretation "multiple push (model evaluation)" + 'ROPlus M gv L lv v = (vpushs M gv lv L v). (* Basic inversion lemmas ***************************************************) -fact vlifts_inv_atom_aux (M) (gv) (lv): is_model M → +fact vpushs_inv_atom_aux (M) (gv) (lv): is_model M → ∀v,L. L ⨁{M}[gv] lv ≘ v → ⋆ = L → lv ≗ v. #M #gv #lv #HM #v #L #H elim H -v -L @@ -44,11 +44,11 @@ fact vlifts_inv_atom_aux (M) (gv) (lv): is_model M → ] qed-. -lemma vlifts_inv_atom (M) (gv) (lv): is_model M → +lemma vpushs_inv_atom (M) (gv) (lv): is_model M → ∀v. ⋆ ⨁{M}[gv] lv ≘ v → lv ≗ v. -/2 width=4 by vlifts_inv_atom_aux/ qed-. +/2 width=4 by vpushs_inv_atom_aux/ qed-. -fact vlifts_inv_abbr_aux (M) (gv) (lv): is_model M → +fact vpushs_inv_abbr_aux (M) (gv) (lv): is_model M → ∀y,L. L ⨁{M}[gv] lv ≘ y → ∀K,V. K.ⓓV = L → ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv, v]]v ≗ y. @@ -64,12 +64,12 @@ fact vlifts_inv_abbr_aux (M) (gv) (lv): is_model M → ] qed-. -lemma vlifts_inv_abbr (M) (gv) (lv): is_model M → +lemma vpushs_inv_abbr (M) (gv) (lv): is_model M → ∀y,K,V. K.ⓓV ⨁{M}[gv] lv ≘ y → ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv, v]]v ≗ y. -/2 width=3 by vlifts_inv_abbr_aux/ qed-. +/2 width=3 by vpushs_inv_abbr_aux/ qed-. -fact vlifts_inv_abst_aux (M) (gv) (lv): is_model M → +fact vpushs_inv_abst_aux (M) (gv) (lv): is_model M → ∀y,L. L ⨁{M}[gv] lv ≘ y → ∀K,W. K.ⓛW = L → ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. @@ -85,12 +85,12 @@ fact vlifts_inv_abst_aux (M) (gv) (lv): is_model M → ] qed-. -lemma vlifts_inv_abst (M) (gv) (lv): is_model M → +lemma vpushs_inv_abst (M) (gv) (lv): is_model M → ∀y,K,W. K.ⓛW ⨁{M}[gv] lv ≘ y → ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. -/2 width=4 by vlifts_inv_abst_aux/ qed-. +/2 width=4 by vpushs_inv_abst_aux/ qed-. -fact vlifts_inv_unit_aux (M) (gv) (lv): is_model M → +fact vpushs_inv_unit_aux (M) (gv) (lv): is_model M → ∀y,L. L ⨁{M}[gv] lv ≘ y → ∀I,K. K.ⓤ{I} = L → ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. @@ -106,20 +106,20 @@ fact vlifts_inv_unit_aux (M) (gv) (lv): is_model M → ] qed-. -lemma vlifts_inv_unit (M) (gv) (lv): is_model M → +lemma vpushs_inv_unit (M) (gv) (lv): is_model M → ∀y,I,K. K.ⓤ{I} ⨁{M}[gv] lv ≘ y → ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. -/2 width=4 by vlifts_inv_unit_aux/ qed-. +/2 width=4 by vpushs_inv_unit_aux/ qed-. (* Basic forward lemmas *****************************************************) -lemma vlifts_fwd_bind (M) (gv) (lv): is_model M → +lemma vpushs_fwd_bind (M) (gv) (lv): is_model M → ∀y,I,K. K.ⓘ{I} ⨁{M}[gv] lv ≘ y → ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y. #M #gv #lv #HM #y * [ #I | * #V ] #L #H -[ /2 width=2 by vlifts_inv_unit/ -| elim (vlifts_inv_abbr … H) // -H #v #HL #Hv +[ /2 width=2 by vpushs_inv_unit/ +| elim (vpushs_inv_abbr … H) // -H #v #HL #Hv /2 width=4 by ex2_2_intro/ -| /2 width=2 by vlifts_inv_abst/ +| /2 width=2 by vpushs_inv_abst/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma similarity index 69% rename from matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma rename to matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma index a324d3cf4..7f5eacc47 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma @@ -12,58 +12,58 @@ (* *) (**************************************************************************) -include "static_2/syntax/shift.ma". -include "apps_2/models/vlifts.ma". +include "static_2/syntax/fold.ma". +include "apps_2/models/vpushs.ma". -(* MULTIPLE LIFT FOR MODEL EVALUATIONS **************************************) +(* MULTIPLE PUSH FOR MODEL EVALUATIONS **************************************) -(* Properties with shift for restricted closures ****************************) +(* Properties with fold for restricted closures *****************************) -lemma vlifts_shift (M): is_model M → is_extensional M → +lemma vpushs_fold (M): is_model M → is_extensional M → ∀L,T1,T2,gv,lv. (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]) → ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv]. #M #H1M #H2M #L elim L -L [| #K * [| * ]] [ #T1 #T2 #gv #lv #H12 - >shift_atom >shift_atom - /4 width=1 by vlifts_atom, veq_refl/ + >fold_atom >fold_atom + /4 width=1 by vpushs_atom, veq_refl/ | #I #IH #T1 #T2 #gv #lv #H12 - >shift_unit >shift_unit - /5 width=1 by vlifts_unit, mx, mr/ + >fold_unit >fold_unit + /5 width=1 by vpushs_unit, mx, mr/ | #V #IH #T1 #T2 #gv #lv #H12 - >shift_pair >shift_pair + >fold_pair >fold_pair @IH -IH #v #Hv @(mq … H1M) [3:|*: /3 width=2 by seq_sym, md/ ] - /4 width=1 by vlifts_abbr, mr/ + /4 width=1 by vpushs_abbr, mr/ | #W #IH #T1 #T2 #gv #lv #H12 - >shift_pair >shift_pair - /5 width=1 by vlifts_abst, mx, mr/ + >fold_pair >fold_pair + /5 width=1 by vpushs_abst, mx, mr/ ] qed. -(* Inversion lemmas with shift for restricted closures **********************) +(* Inversion lemmas with fold for restricted closures ***********************) -lemma vlifts_inv_shift (M): is_model M → +lemma vpushs_inv_fold (M): is_model M → ∀L,T1,T2,gv,lv. ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv] → ∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]. #M #HM #L elim L -L [| #K * [| * ]] [ #T1 #T2 #gv #lv - >shift_atom >shift_atom #H12 #v #H - lapply (vlifts_inv_atom … H) -H // #Hv + >fold_atom >fold_atom #H12 #v #H + lapply (vpushs_inv_atom … H) -H // #Hv /4 width=7 by ti_comp, veq_refl, mq/ | #I #IH #T1 #T2 #gv #lv - >shift_unit >shift_unit #H12 #y #H - elim (vlifts_inv_unit … H) -H // #v #d #Hlv #Hv + >fold_unit >fold_unit #H12 #y #H + elim (vpushs_inv_unit … H) -H // #v #d #Hlv #Hv lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12 /4 width=7 by ti_comp, ti_fwd_mx_dx, veq_refl, mq/ | #V #IH #T1 #T2 #gv #lv - >shift_pair >shift_pair #H12 #y #H - elim (vlifts_inv_abbr … H) -H // #v #Hlv #Hv + >fold_pair >fold_pair #H12 #y #H + elim (vpushs_inv_abbr … H) -H // #v #Hlv #Hv lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12 /4 width=7 by ti_comp, veq_refl, md, mq/ | #W #IH #T1 #T2 #gv #lv - >shift_pair >shift_pair #H12 #y #H - elim (vlifts_inv_abst … H) -H // #v #d #Hlv #Hv + >fold_pair >fold_pair #H12 #y #H + elim (vpushs_inv_abst … H) -H // #v #d #Hlv #Hv lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12 /4 width=7 by ti_comp, ti_fwd_mx_dx, veq_refl, mq/ ] diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/functional/uparrow_2.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/uparrow_2.ma new file mode 100644 index 000000000..627c0995e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/uparrow_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 "functional" COMPONENT **************************************) + +notation "hvbox( ↑[ term 46 h ] break term 46 T )" + non associative with precedence 46 + for @{ 'UpArrow $h $T }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/functional/uparrow_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/uparrow_3.ma new file mode 100644 index 000000000..17d967860 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/functional/uparrow_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 "functional" COMPONENT **************************************) + +notation "hvbox( ↑[ term 46 d, break term 46 h ] break term 46 T )" + non associative with precedence 46 + for @{ 'UpArrow $d $h $T }. 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 new file mode 100644 index 000000000..20d2d6e33 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/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/models/dotteduparrow_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/dotteduparrow_3.ma new file mode 100644 index 000000000..3ffe16ffa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/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/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 236ec0c5c..747b554ad 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 @@ -9,18 +9,24 @@ table { ] } ] - class "orange" + class "yellow" [ { "models" * } { + [ { "term model" * } { + [ "tm" + "( ⇡[?]? )" + "( ⇡[?←?]? )" + "tm_exteq" + * ] + } + ] [ { "denotational equivalence" * } { [ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ] } ] [ { "local environment interpretation" * } { - [ "li" + "( ? ϵ ⟦?⟧{?}[?] )" "li_vlifts" * ] + [ "li" + "( ? ϵ ⟦?⟧{?}[?] )" "li_vpushs" * ] } ] - [ { "multiple evaluation lift" * } { - [ "vlifts" + "( ?⨁{?}[?]? ≘ ? )" "vlifts_shift" * ] + [ { "multiple evaluation push" * } { + [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpush_fold" * ] } ] [ { "evaluation equivalence" * } { @@ -29,7 +35,7 @@ table { ] [ { "model declaration" * } { [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )" - "model_vlift" + "( ⫯{?}[?←?]? )" + "model_vpush" + "( ⫯{?}[?←?]? )" "model_props" * ] } @@ -45,19 +51,23 @@ table { ] } ] +*) class "orange" [ { "functional" * } { +(* [ { "reduction and type machine" * } { [ "rtm" "rtm_step ( ? ⇨ ? )" * ] } ] +*) [ { "relocation" * } { - [ "lift ( ↑[?,?] ? )" * ] + [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )" + "flifts_basic" + "( ↑[?,?]? )" + * ] } ] } ] -*) class "red" [ { "examples" * } { [ { "terms with special features" * } { diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 9ab2c9283..e1ac851a2 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -5,4 +5,5 @@ basic_2/rt_computation basic_2/rt_conversion basic_2/rt_equivalence apps_2/examples/ex_cpr_omega.ma +apps_2/functional/ apps_2/models/ diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma index 56f69a641..54372cf8f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma @@ -1,4 +1,3 @@ - (**************************************************************************) (* ___ *) (* ||M|| *) @@ -357,7 +356,7 @@ elim (IHV1 f) -IHV1 #V2 #HV12 ] qed-. -lemma lift_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i). +lemma lifts_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i). #l elim l -l /2 width=1 by lifts_lref/ qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma similarity index 74% rename from matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma rename to matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma index 0c40a310b..67bfbf7ff 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma @@ -14,25 +14,25 @@ include "static_2/syntax/lenv.ma". -(* SHIFT FOR RESTRICTED CLOSURES ********************************************) +(* FOLD FOR RESTRICTED CLOSURES *********************************************) -rec definition shift L T on L ≝ match L with +rec definition fold L T on L ≝ match L with [ LAtom ⇒ T | LBind L I ⇒ match I with - [ BUnit _ ⇒ shift L (-ⓛ⋆0.T) - | BPair I V ⇒ shift L (-ⓑ{I}V.T) + [ BUnit _ ⇒ fold L (-ⓛ⋆0.T) + | BPair I V ⇒ fold L (-ⓑ{I}V.T) ] ]. -interpretation "shift (restricted closure)" 'plus L T = (shift L T). +interpretation "fold (restricted closure)" 'plus L T = (fold L T). (* Basic properties *********************************************************) -lemma shift_atom: ∀T. ⋆ + T = T. +lemma fold_atom: ∀T. ⋆ + T = T. // qed. -lemma shift_unit: ∀I,L,T. L.ⓤ{I}+T = L+(-ⓛ⋆0.T). +lemma fold_unit: ∀I,L,T. L.ⓤ{I}+T = L+(-ⓛ⋆0.T). // qed. -lemma shift_pair: ∀I,L,V,T. (L.ⓑ{I}V)+T = L+(-ⓑ{I}V.T). +lemma fold_pair: ∀I,L,V,T. (L.ⓑ{I}V)+T = L+(-ⓑ{I}V.T). // qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index 6a2e3859e..6a7a09101 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -103,7 +103,7 @@ table { } ] [ { "append" * } { - [ [ "for restricted closures" ] "shift" + "( ? + ? )" "shift_append" * ] + [ [ "for restricted closures" ] "fold" + "( ? + ? )" "fold_append" * ] [ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ] } ] -- 2.39.2