--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
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
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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 <IHV <IHT -V2 -T2 //
+| #f #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT <IHV <IHT -V2 -T2 //
+]
+qed-.
+
+(* Derived properties *******************************************************)
+
+lemma flifts_lref_uni: ∀l,i. ↑[l](#i) = #(l+i).
+/3 width=1 by flifts_inv_lifts, lifts_lref_uni/ qed.
+(*
+lemma flift_join: ∀e1,e2,T. ⬆[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
+#e1 #e2 #T
+lapply (flift_lift T 0 (e1+e2)) #H
+elim (lift_split … H e1 e1) -H // #U #H
+>(flift_inv_lift … H) -H //
+qed.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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
- ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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).
@(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
@(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/
[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-.
| #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
(* *)
(**************************************************************************)
-include "apps_2/models/model_vlift.ma".
+include "apps_2/models/model_vpush.ma".
(* MODEL ********************************************************************)
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 *****************************************************)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/lib/functions.ma".
+include "ground_2/lib/exteq.ma".
+include "apps_2/models/tm.ma".
+
+(* TERM MODEL ***************************************************************)
+
+(* Properties with extensional equivalencs of evaluations *******************)
+
+lemma tm_gc_id: ∀j. ⇡[j]tm_gc ≐ tm_gc.
+// qed.
+
+lemma tm_lc_id: ⇡[0←#0]tm_lc ≐ tm_lc.
+#i elim (eq_or_gt i) #Hi destruct //
+>tm_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
+qed.
+
+lemma tm_vlift_comp (l): compatible_2 … (tm_vlift l) (exteq …) (exteq …).
+#l #gv1 #gv2 #Hgv #i
+>tm_vlift_rw >tm_vlift_rw //
+qed.
+
+lemma tm_vpush_comp (i): compatible_3 … (tm_vpush i) (eq …) (exteq …) (exteq …).
+#i #T1 #T2 #HT12 #lv1 #lv2 #Hlv #j
+elim (lt_or_eq_or_gt j i) #Hij destruct
+[ >tm_vpush_lt // >tm_vpush_lt //
+| >tm_vpush_eq >tm_vpush_eq //
+| >tm_vpush_gt // >tm_vpush_gt //
+]
+qed-.
+
+lemma tm_ti_comp (T): compatible_3 … (λgv,lv.tm_ti gv lv T) (exteq …) (exteq …) (eq …).
+#T elim T -T *
+[ //
+| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+ whd in ⊢ (??%%); //
+| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+ whd in ⊢ (??%%); //
+| #p #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+ whd in ⊢ (??%%); /4 width=1 by tm_vlift_comp, tm_vpush_comp, eq_f3/
+| #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+ whd in ⊢ (??%%); /3 width=1 by eq_f3/
+]
+qed-.
+
+lemma tm_ti_eq (T): tm_ti tm_gc tm_lc T = T.
+#T elim T -T * //
+[ #p #I #V #T #IHV #IHT
+ <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
+ whd in ⊢ (??%?); /3 width=1 by tm_ti_comp, eq_f3/
+| #I #V #T #IHV #IHT
+ <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT //
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_cpcs.ma".
+include "apps_2/models/model_props.ma".
+include "apps_2/models/tm.ma".
+
+(* TERM MODEL ***************************************************************)
+
+lemma tm_md (h): ∀T,V,gv,lv. ⟦+ⓓV.T⟧[gv,lv] ≗{TM h} ⟦T⟧[gv,⫯[O←⟦V⟧[gv,lv]]lv].
+#h #T elim T *
+[ /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/
+| #i #V #gv #lv
+ elim (eq_or_gt i) #Hi destruct
+ [ elim (lifts_total (⟦V⟧[gv,lv]) (𝐔❴1❵)) #W #HVW
+ >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 ]
+*)
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-.
[ /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/
]
(* 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
@(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 ]
@(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
]
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-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
]
}
]
- 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" * } {
]
[ { "model declaration" * } {
[ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
- "model_vlift" + "( ⫯{?}[?←?]? )"
+ "model_vpush" + "( ⫯{?}[?←?]? )"
"model_props"
* ]
}
]
}
]
+*)
class "orange"
[ { "functional" * } {
+(*
[ { "reduction and type machine" * } {
[ "rtm" "rtm_step ( ? ⇨ ? )" * ]
}
]
+*)
[ { "relocation" * } {
- [ "lift ( ↑[?,?] ? )" * ]
+ [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )"
+ "flifts_basic" + "( ↑[?,?]? )"
+ * ]
}
]
}
]
-*)
class "red"
[ { "examples" * } {
[ { "terms with special features" * } {
basic_2/rt_conversion
basic_2/rt_equivalence
apps_2/examples/ex_cpr_omega.ma
+apps_2/functional/
apps_2/models/
-
(**************************************************************************)
(* ___ *)
(* ||M|| *)
]
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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
}
]
[ { "append" * } {
- [ [ "for restricted closures" ] "shift" + "( ? + ? )" "shift_append" * ]
+ [ [ "for restricted closures" ] "fold" + "( ? + ? )" "fold_append" * ]
[ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ]
}
]
projects / helm.git / commitdiff