From: Ferruccio Guidi Date: Fri, 13 Jul 2018 15:34:46 +0000 (+0200) Subject: update in static_2 and app_2 X-Git-Tag: make_still_working~299 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=cc6fcb70ca4f3cf01205ed722d75a2fdb2aaf779 update in static_2 and app_2 + term model started + functional relocation reactivated + some renaming --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/functional/notation.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/notation.etc new file mode 100644 index 000000000..800038120 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/notation.etc @@ -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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE "functional" COMPONENT ********************************) + +notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )" + non associative with precedence 50 + for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. + +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/etc/functional/rtm.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm.etc new file mode 100644 index 000000000..e8ac12370 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm.etc @@ -0,0 +1,86 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/term_vector.ma". +include "basic_2/syntax/genv.ma". +include "apps_2/functional/notation.ma". + +(* REDUCTION AND TYPE MACHINE ***********************************************) + +(* machine local environment *) +inductive xenv: Type[0] ≝ +| XAtom: xenv (* empty *) +| XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *) +. + +interpretation "atom (ext. local environment)" + 'Star = XAtom. + +interpretation "environment construction (quad)" + 'DxItem4 L I u K V = (XQuad L I u K V). + +(* machine stack *) +definition stack: Type[0] ≝ list2 xenv term. + +(* machine status *) +record rtm: Type[0] ≝ +{ rg: genv; (* global environment *) + ru: nat; (* current de Bruijn's level *) + re: xenv; (* extended local environment *) + rs: stack; (* application stack *) + rt: term (* code *) +}. + +(* initial state *) +definition rtm_i: genv → term → rtm ≝ + λG,T. mk_rtm G 0 (⋆) (Ⓔ) T. + +(* update code *) +definition rtm_t: rtm → term → rtm ≝ + λM,T. match M with + [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (Ⓔ) T + ]. + +(* update closure *) +definition rtm_u: rtm → xenv → term → rtm ≝ + λM,E,T. match M with + [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (Ⓔ) T + ]. + +(* get global environment *) +definition rtm_g: rtm → genv ≝ + λM. match M with + [ mk_rtm G _ _ _ _ ⇒ G + ]. + +(* get local reference level *) +definition rtm_l: rtm → nat ≝ + λM. match M with + [ mk_rtm _ u E _ _ ⇒ match E with + [ XAtom ⇒ u + | XQuad _ _ u _ _ ⇒ u + ] + ]. + +(* get stack *) +definition rtm_s: rtm → stack ≝ + λM. match M with + [ mk_rtm _ _ _ S _ ⇒ S + ]. + +(* get code *) +definition rtm_c: rtm → term ≝ + λM. match M with + [ mk_rtm _ _ _ _ T ⇒ T + ]. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm_step.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm_step.etc new file mode 100644 index 000000000..1b456b521 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/functional/rtm_step.etc @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rtm.ma". + +(* REDUCTION AND TYPE MACHINE ***********************************************) + +(* transitions *) +inductive rtm_step: relation rtm ≝ +| rtm_drop : ∀G,u,E,I,t,D,V,S,i. + rtm_step (mk_rtm G u (E. ④{I} {t, D, V}) S (#(i + 1))) + (mk_rtm G u E S (#i)) +| rtm_ldelta: ∀G,u,E,t,D,V,S. + rtm_step (mk_rtm G u (E. ④{Abbr} {t, D, V}) S (#0)) + (mk_rtm G u D S V) +| rtm_ltype : ∀G,u,E,t,D,V,S. + rtm_step (mk_rtm G u (E. ④{Abst} {t, D, V}) S (#0)) + (mk_rtm G u D S V) +| rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| → + rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p)) + (mk_rtm G u E S (§p)) +| rtm_gdelta: ∀G,V,u,E,S,p. p = |G| → + rtm_step (mk_rtm (G. ⓓV) u E S (§p)) + (mk_rtm G u E S V) +| rtm_gtype : ∀G,V,u,E,S,p. p = |G| → + rtm_step (mk_rtm (G. ⓛV) u E S (§p)) + (mk_rtm G u E S V) +| rtm_eps : ∀G,u,E,S,W,T. + rtm_step (mk_rtm G u E S (ⓝW. T)) + (mk_rtm G u E S T) +| rtm_appl : ∀G,u,E,S,V,T. + rtm_step (mk_rtm G u E S (ⓐV. T)) + (mk_rtm G u E ({E, V} @ S) T) +| rtm_beta : ∀G,u,E,D,V,S,W,T. + rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T)) + (mk_rtm G u (E. ④{Abbr} {u, D, V}) S T) +| rtm_push : ∀G,u,E,W,T. + rtm_step (mk_rtm G u E (Ⓔ) (+ⓛW. T)) + (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (Ⓔ) T) +| rtm_theta : ∀G,u,E,S,V,T. + rtm_step (mk_rtm G u E S (+ⓓV. T)) + (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) +. + +interpretation "sequential reduction (RTM)" + 'SRed O1 O2 = (rtm_step O1 O2). 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/flifts.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma new file mode 100644 index 000000000..edc607bbc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.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/notation/functions/uparrowstar_2.ma". +include "apps_2/notation/functional/uparrow_2.ma". +include "static_2/relocation/lifts.ma". + +(* GENERIC FUNCTIONAL RELOCATION ********************************************) + +rec definition flifts f U on U ≝ match U with +[ TAtom I ⇒ match I with + [ Sort _ ⇒ U + | LRef i ⇒ #(f@❴i❵) + | GRef _ ⇒ U + ] +| TPair I V T ⇒ match I with + [ Bind2 p I ⇒ ⓑ{p,I}(flifts f V).(flifts (⫯f) T) + | Flat2 I ⇒ ⓕ{I}(flifts f V).(flifts f 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 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 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/functional/lift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma deleted file mode 100644 index ea7409060..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma +++ /dev/null @@ -1,68 +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 "basic_2/substitution/lift.ma". -include "apps_2/functional/notation.ma". - -(* FUNCTIONAL RELOCATION ****************************************************) - -let rec flift d e U on U ≝ match U with -[ TAtom I ⇒ match I with - [ Sort _ ⇒ U - | LRef i ⇒ #(tri … i d i (i + e) (i + e)) - | 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) - ] -]. - -interpretation "functional relocation" 'Lift d e T = (flift d e 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/ -] -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 // - ] -] -qed-. - -(* Derived properties *******************************************************) - -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/notation.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma deleted file mode 100644 index 172f475fa..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE "functional" COMPONENT ********************************) - -notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )" - 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/functional/rtm.ma deleted file mode 100644 index e8ac12370..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma +++ /dev/null @@ -1,86 +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 "basic_2/syntax/term_vector.ma". -include "basic_2/syntax/genv.ma". -include "apps_2/functional/notation.ma". - -(* REDUCTION AND TYPE MACHINE ***********************************************) - -(* machine local environment *) -inductive xenv: Type[0] ≝ -| XAtom: xenv (* empty *) -| XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *) -. - -interpretation "atom (ext. local environment)" - 'Star = XAtom. - -interpretation "environment construction (quad)" - 'DxItem4 L I u K V = (XQuad L I u K V). - -(* machine stack *) -definition stack: Type[0] ≝ list2 xenv term. - -(* machine status *) -record rtm: Type[0] ≝ -{ rg: genv; (* global environment *) - ru: nat; (* current de Bruijn's level *) - re: xenv; (* extended local environment *) - rs: stack; (* application stack *) - rt: term (* code *) -}. - -(* initial state *) -definition rtm_i: genv → term → rtm ≝ - λG,T. mk_rtm G 0 (⋆) (Ⓔ) T. - -(* update code *) -definition rtm_t: rtm → term → rtm ≝ - λM,T. match M with - [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (Ⓔ) T - ]. - -(* update closure *) -definition rtm_u: rtm → xenv → term → rtm ≝ - λM,E,T. match M with - [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (Ⓔ) T - ]. - -(* get global environment *) -definition rtm_g: rtm → genv ≝ - λM. match M with - [ mk_rtm G _ _ _ _ ⇒ G - ]. - -(* get local reference level *) -definition rtm_l: rtm → nat ≝ - λM. match M with - [ mk_rtm _ u E _ _ ⇒ match E with - [ XAtom ⇒ u - | XQuad _ _ u _ _ ⇒ u - ] - ]. - -(* get stack *) -definition rtm_s: rtm → stack ≝ - λM. match M with - [ mk_rtm _ _ _ S _ ⇒ S - ]. - -(* get code *) -definition rtm_c: rtm → term ≝ - λM. match M with - [ mk_rtm _ _ _ _ T ⇒ T - ]. diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma deleted file mode 100644 index 1b456b521..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma +++ /dev/null @@ -1,57 +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 "apps_2/functional/rtm.ma". - -(* REDUCTION AND TYPE MACHINE ***********************************************) - -(* transitions *) -inductive rtm_step: relation rtm ≝ -| rtm_drop : ∀G,u,E,I,t,D,V,S,i. - rtm_step (mk_rtm G u (E. ④{I} {t, D, V}) S (#(i + 1))) - (mk_rtm G u E S (#i)) -| rtm_ldelta: ∀G,u,E,t,D,V,S. - rtm_step (mk_rtm G u (E. ④{Abbr} {t, D, V}) S (#0)) - (mk_rtm G u D S V) -| rtm_ltype : ∀G,u,E,t,D,V,S. - rtm_step (mk_rtm G u (E. ④{Abst} {t, D, V}) S (#0)) - (mk_rtm G u D S V) -| rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| → - rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p)) - (mk_rtm G u E S (§p)) -| rtm_gdelta: ∀G,V,u,E,S,p. p = |G| → - rtm_step (mk_rtm (G. ⓓV) u E S (§p)) - (mk_rtm G u E S V) -| rtm_gtype : ∀G,V,u,E,S,p. p = |G| → - rtm_step (mk_rtm (G. ⓛV) u E S (§p)) - (mk_rtm G u E S V) -| rtm_eps : ∀G,u,E,S,W,T. - rtm_step (mk_rtm G u E S (ⓝW. T)) - (mk_rtm G u E S T) -| rtm_appl : ∀G,u,E,S,V,T. - rtm_step (mk_rtm G u E S (ⓐV. T)) - (mk_rtm G u E ({E, V} @ S) T) -| rtm_beta : ∀G,u,E,D,V,S,W,T. - rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T)) - (mk_rtm G u (E. ④{Abbr} {u, D, V}) S T) -| rtm_push : ∀G,u,E,W,T. - rtm_step (mk_rtm G u E (Ⓔ) (+ⓛW. T)) - (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (Ⓔ) T) -| rtm_theta : ∀G,u,E,S,V,T. - rtm_step (mk_rtm G u E S (+ⓓV. T)) - (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) -. - -interpretation "sequential reduction (RTM)" - 'SRed O1 O2 = (rtm_step O1 O2). 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_vlift.ma deleted file mode 100644 index bb2d5c7c9..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/model_vlift.ma +++ /dev/null @@ -1,36 +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 "apps_2/notation/models/upspoon_4.ma". -include "apps_2/models/model.ma". - -(* MODEL ********************************************************************) - -definition vlift (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). - -(* Basic properties *********************************************************) - -lemma vlift_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. -/2 width=1 by tri_eq/ qed-. - -lemma vlift_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/model_vpush.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_vpush.ma new file mode 100644 index 000000000..ccf633e6e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_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 "ground_2/lib/functions.ma". +include "apps_2/notation/models/upspoon_4.ma". +include "apps_2/models/model.ma". + +(* MODEL ********************************************************************) + +definition vpush (M): nat → dd M → evaluation M → evaluation M ≝ + λj,d,lv,i. tri … i j (lv i) d (lv (↓i)). + +interpretation "push (model evaluation)" + 'UpSpoon M i d lv = (vpush M i d lv). + +(* Basic properties *********************************************************) + +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 vpush_eq (M): ∀lv,d,i. (⫯{M}[i←d] lv) i = d. +/2 width=1 by tri_eq/ qed-. + +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/vlifts.ma deleted file mode 100644 index 81321cdac..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts.ma +++ /dev/null @@ -1,125 +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 "apps_2/notation/models/roplus_5.ma". -include "static_2/syntax/lenv.ma". -include "apps_2/models/veq.ma". - -(* MULTIPLE LIFT 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 -. - -interpretation "multiple lift (model evaluation)" - 'ROPlus M gv L lv v = (vlifts M gv lv L v). - -(* Basic inversion lemmas ***************************************************) - -fact vlifts_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 -[ #_ /2 width=1 by veq_refl/ -| #v #d #K #V #_ #_ #_ #H destruct -| #v #d #K #V #_ #_ #H destruct -| #v #d #I #K #_ #_ #H destruct -| #v1 #v2 #L #_ #Hv12 #IH #H destruct - /3 width=3 by veq_trans/ -] -qed-. - -lemma vlifts_inv_atom (M) (gv) (lv): is_model M → - ∀v. ⋆ ⨁{M}[gv] lv ≘ v → lv ≗ v. -/2 width=4 by vlifts_inv_atom_aux/ qed-. - -fact vlifts_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. -#M #gv #lv #HM #y #L #H elim H -y -L -[ #Y #X #H destruct -| #v #d #K #V #Hv #Hd #_ #Y #X #H destruct - /3 width=3 by veq_refl, ex2_intro/ -| #v #d #K #V #_ #_ #Y #X #H destruct -| #v #d #I #K #_ #_ #Y #X #H destruct -| #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct - elim IH -IH [|*: // ] #v #Hv #Hv1 - /3 width=5 by veq_trans, ex2_intro/ -] -qed-. - -lemma vlifts_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-. - -fact vlifts_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. -#M #gv #lv #HM #y #L #H elim H -y -L -[ #Y #X #H destruct -| #v #d #K #V #_ #_ #_ #Y #X #H destruct -| #v #d #K #V #Hv #_ #Y #X #H destruct - /3 width=4 by veq_refl, ex2_2_intro/ -| #v #d #I #K #_ #_ #Y #X #H destruct -| #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct - elim IH -IH [|*: // ] #v #d #Hv #Hv1 - /3 width=6 by veq_trans, ex2_2_intro/ -] -qed-. - -lemma vlifts_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-. - -fact vlifts_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. -#M #gv #lv #HM #y #L #H elim H -y -L -[ #Z #Y #H destruct -| #v #d #K #V #_ #_ #_ #Z #Y #H destruct -| #v #d #K #V #_ #_ #Z #Y #H destruct -| #v #d #I #K #Hv #_ #Z #Y #H destruct - /3 width=4 by veq_refl, ex2_2_intro/ -| #v1 #v2 #L #_ #Hv12 #IH #Z #Y #H destruct - elim IH -IH [|*: // ] #v #d #Hv #Hv1 - /3 width=6 by veq_trans, ex2_2_intro/ -] -qed-. - -lemma vlifts_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-. - -(* Basic forward lemmas *****************************************************) - -lemma vlifts_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=4 by ex2_2_intro/ -| /2 width=2 by vlifts_inv_abst/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma deleted file mode 100644 index a324d3cf4..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vlifts_shift.ma +++ /dev/null @@ -1,70 +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 "static_2/syntax/shift.ma". -include "apps_2/models/vlifts.ma". - -(* MULTIPLE LIFT FOR MODEL EVALUATIONS **************************************) - -(* Properties with shift for restricted closures ****************************) - -lemma vlifts_shift (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/ -| #I #IH #T1 #T2 #gv #lv #H12 - >shift_unit >shift_unit - /5 width=1 by vlifts_unit, mx, mr/ -| #V #IH #T1 #T2 #gv #lv #H12 - >shift_pair >shift_pair - @IH -IH #v #Hv - @(mq … H1M) [3:|*: /3 width=2 by seq_sym, md/ ] - /4 width=1 by vlifts_abbr, mr/ -| #W #IH #T1 #T2 #gv #lv #H12 - >shift_pair >shift_pair - /5 width=1 by vlifts_abst, mx, mr/ -] -qed. - -(* Inversion lemmas with shift for restricted closures **********************) - -lemma vlifts_inv_shift (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 - /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 - 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 - 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 - lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12 - /4 width=7 by ti_comp, ti_fwd_mx_dx, veq_refl, mq/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma new file mode 100644 index 000000000..dabd2c431 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma @@ -0,0 +1,125 @@ +(**************************************************************************) +(* ___ *) +(* ||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/models/roplus_5.ma". +include "static_2/syntax/lenv.ma". +include "apps_2/models/veq.ma". + +(* MULTIPLE PUSH FOR MODEL EVALUATIONS **************************************) + +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 push (model evaluation)" + 'ROPlus M gv L lv v = (vpushs M gv lv L v). + +(* Basic inversion lemmas ***************************************************) + +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 +[ #_ /2 width=1 by veq_refl/ +| #v #d #K #V #_ #_ #_ #H destruct +| #v #d #K #V #_ #_ #H destruct +| #v #d #I #K #_ #_ #H destruct +| #v1 #v2 #L #_ #Hv12 #IH #H destruct + /3 width=3 by veq_trans/ +] +qed-. + +lemma vpushs_inv_atom (M) (gv) (lv): is_model M → + ∀v. ⋆ ⨁{M}[gv] lv ≘ v → lv ≗ v. +/2 width=4 by vpushs_inv_atom_aux/ qed-. + +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. +#M #gv #lv #HM #y #L #H elim H -y -L +[ #Y #X #H destruct +| #v #d #K #V #Hv #Hd #_ #Y #X #H destruct + /3 width=3 by veq_refl, ex2_intro/ +| #v #d #K #V #_ #_ #Y #X #H destruct +| #v #d #I #K #_ #_ #Y #X #H destruct +| #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct + elim IH -IH [|*: // ] #v #Hv #Hv1 + /3 width=5 by veq_trans, ex2_intro/ +] +qed-. + +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 vpushs_inv_abbr_aux/ qed-. + +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. +#M #gv #lv #HM #y #L #H elim H -y -L +[ #Y #X #H destruct +| #v #d #K #V #_ #_ #_ #Y #X #H destruct +| #v #d #K #V #Hv #_ #Y #X #H destruct + /3 width=4 by veq_refl, ex2_2_intro/ +| #v #d #I #K #_ #_ #Y #X #H destruct +| #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct + elim IH -IH [|*: // ] #v #d #Hv #Hv1 + /3 width=6 by veq_trans, ex2_2_intro/ +] +qed-. + +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 vpushs_inv_abst_aux/ qed-. + +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. +#M #gv #lv #HM #y #L #H elim H -y -L +[ #Z #Y #H destruct +| #v #d #K #V #_ #_ #_ #Z #Y #H destruct +| #v #d #K #V #_ #_ #Z #Y #H destruct +| #v #d #I #K #Hv #_ #Z #Y #H destruct + /3 width=4 by veq_refl, ex2_2_intro/ +| #v1 #v2 #L #_ #Hv12 #IH #Z #Y #H destruct + elim IH -IH [|*: // ] #v #d #Hv #Hv1 + /3 width=6 by veq_trans, ex2_2_intro/ +] +qed-. + +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 vpushs_inv_unit_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +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 vpushs_inv_unit/ +| elim (vpushs_inv_abbr … H) // -H #v #HL #Hv + /2 width=4 by ex2_2_intro/ +| /2 width=2 by vpushs_inv_abst/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma new file mode 100644 index 000000000..7f5eacc47 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fold.ma". +include "apps_2/models/vpushs.ma". + +(* MULTIPLE PUSH FOR MODEL EVALUATIONS **************************************) + +(* Properties with fold for restricted closures *****************************) + +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 + >fold_atom >fold_atom + /4 width=1 by vpushs_atom, veq_refl/ +| #I #IH #T1 #T2 #gv #lv #H12 + >fold_unit >fold_unit + /5 width=1 by vpushs_unit, mx, mr/ +| #V #IH #T1 #T2 #gv #lv #H12 + >fold_pair >fold_pair + @IH -IH #v #Hv + @(mq … H1M) [3:|*: /3 width=2 by seq_sym, md/ ] + /4 width=1 by vpushs_abbr, mr/ +| #W #IH #T1 #T2 #gv #lv #H12 + >fold_pair >fold_pair + /5 width=1 by vpushs_abst, mx, mr/ +] +qed. + +(* Inversion lemmas with fold for restricted closures ***********************) + +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 + >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 + >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 + >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 + >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/ +] +qed-. 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/fold.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma new file mode 100644 index 000000000..67bfbf7ff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lenv.ma". + +(* FOLD FOR RESTRICTED CLOSURES *********************************************) + +rec definition fold L T on L ≝ match L with +[ LAtom ⇒ T +| LBind L I ⇒ match I with + [ BUnit _ ⇒ fold L (-ⓛ⋆0.T) + | BPair I V ⇒ fold L (-ⓑ{I}V.T) + ] +]. + +interpretation "fold (restricted closure)" 'plus L T = (fold L T). + +(* Basic properties *********************************************************) + +lemma fold_atom: ∀T. ⋆ + T = T. +// qed. + +lemma fold_unit: ∀I,L,T. L.ⓤ{I}+T = L+(-ⓛ⋆0.T). +// qed. + +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/syntax/shift.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma deleted file mode 100644 index 0c40a310b..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/shift.ma +++ /dev/null @@ -1,38 +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 "static_2/syntax/lenv.ma". - -(* SHIFT FOR RESTRICTED CLOSURES ********************************************) - -rec definition shift 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) - ] -]. - -interpretation "shift (restricted closure)" 'plus L T = (shift L T). - -(* Basic properties *********************************************************) - -lemma shift_atom: ∀T. ⋆ + T = T. -// qed. - -lemma shift_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). -// 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" * ] } ]