TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib clean \
www up-html
-PACKAGES := ground_2 basic_2 static_2 apps_2 alpha_1
-XPACKAGES := ground_2 basic_2
+PACKAGES := ground_2 static_2 basic_2 apps_2 alpha_1
+XPACKAGES := ground_2 static_2 basic_2
LDWS := $(shell find -name "*.ldw.xml")
TBLS := $(shell find -name "*.tbl")
--- /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( ⫰[ break term 46 i ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'DownSpoon $M $i $lv }.
+
+notation > "hvbox( ⫰[ break term 46 i ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'DownSpoon ? $i $lv }.
+
+notation > "hvbox( ⫰{ term 46 M }[ break term 46 i ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'DownSpoon $M $i $lv }.
--- /dev/null
+
+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
+[ >vdrop_lt // >vdrop_lt //
+| >vdrop_ge // >vdrop_ge //
+]
+qed.
+
+lemma vlift_vdrop_eq (M): ∀lv,i. lv ≐{?,dd M} ⫯[i←lv i]⫰[i]lv.
+#M #lv #i #j elim (lt_or_eq_or_gt j i) #Hji destruct
+[ >vlift_lt // >vdrop_lt //
+| >vlift_eq //
+| >vlift_gt // >vdrop_ge /2 width=1 by monotonic_pred/
+ <(lt_succ_pred … Hji) //
+]
+qed.
+
+axiom vdrop_vlift_eq: ∀M,lv,d,i. lv ≐{?,dd M} ⫰[i]⫯[i←d]lv.
+(*
+#M #lv #d #i #j elim (lt_or_eq_or_gt j i) #Hji destruct
+*)
+
+lemma ext_inv_vlift_sn (M): ∀lv1,y,i,d. ⫯[i←d]lv1 ≐{?,dd M} y →
+ ∧∧ d = y i & lv1 ≐ ⫰[i]y.
+#M #lv1 #y #i #d #H @conj
+[ lapply (H i) -H >vlift_eq //
+| @exteq_trans [2: @(vdrop_vlift_eq … d i) | skip ]
+ @vdrop_ext //
+]
+qed-.
+
+lemma ext_inv_vlift_sn (M): ∀lv1,y,i,d. ⫯[i←d]lv1 ≐{?,dd M} y →
+ ∃∃lv2. lv1 ≐ lv2 & ⫯[i←d]lv2 = y.
+
+lemma li_repl (M) (gv): ∀lv1,L. lv1 ϵ ⟦L⟧{M}[gv] →
+ ∀lv2. lv1 ≐ lv2 → lv2 ϵ ⟦L⟧{M}[gv].
+#M #gv #lv1 #L #H elim H -lv1 -L
+[ //
+|
+| #lv1 #d #K #W #_ #IH #y #H
+
+
+
+
+lemma ext_veq (M): is_model M →
+ ∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2.
+/2 width=1 by mr/ qed.
+
+lemma veq_repl_exteq (M): is_model M →
+ replace_2 … (veq M) (exteq …) (exteq …).
+/2 width=5 by mq/ qed-.
+
+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 "static_2/syntax/genv.ma".
+
+(* GLOBAL ENVIRONMENT INTERPRETATION ***************************************)
--- /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/model.ma".
+
+(* MODEL ********************************************************************)
+
+definition valign (M) (l): evaluation M → evaluation M ≝
+ λlv,i. ⫯[l](lv i).
+
+interpretation "alignment (model evaluation)"
+ 'UpSpoon M l lv = (valign M l lv).
+
+(* Basic properties *********************************************************)
+
+lemma valign_rw (M) (l) (lv): ∀i. (⫯{M}[l]lv) i = ⫯[l](lv i).
+// 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 "models" COMPONENT **************************************)
+
+notation < "hvbox( ↑[ term 46 f ] break term 70 d )"
+ non associative with precedence 70
+ for @{ 'UpArrow $M $f $d }.
+
+notation > "hvbox( ↑[ term 46 f ] break term 70 d )"
+ non associative with precedence 70
+ for @{ 'UpArrow ? $f $d }.
+
+notation > "hvbox( ↑{ term 46 M }[ break term 46 f ] break term 70 d )"
+ non associative with precedence 70
+ for @{ 'UpArrow $M $f $d }.
--- /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( ⫯[ break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon $M $d $lv }.
+
+notation > "hvbox( ⫯[ break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon ? $d $lv }.
+
+notation > "hvbox( ⫯{ term 46 M }[ break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'UpSpoon $M $d $lv }.
--- /dev/null
+include "apps_2/notation/models/upspoon_3.ma".
+
+ al: nat → dd → dd; (* alignment *)
+
+interpretation "alignment (model)"
+ 'UpSpoon M i d = (al M i d).
+
+(* Note: lift: compatibility *)
+ mf: compatible_3 … (al M) (eq …) (sq M) (sq M);
+(* Note: lift: swap *)
+ mw: ∀l1,l2,d. l2 ≤ l1 → ⫯[l2]⫯[l1]d ≗{M} ⫯[↑l1]⫯[l2]d;
+(* Note: lift: sort evaluation *)
+ mv: ∀l,s. ⫯[l](sv M s) ≗ sv M s;
+
+theorem valign_swap (M): is_model M →
+ ∀l1,l2. l2 ≤ l1 →
+ ∀lv:evaluation …. ⫯[l2]⫯[l1]lv ≗{M} ⫯[↑l1]⫯[l2]lv.
+/2 width=1 by mw/ qed.
+
+lemma valign_comp (M): is_model M →
+ ∀l. compatible_2 … (valign M l) (veq M) (veq M).
+/2 width=1 by mf/ qed-.
-
-
-lemma vdrop_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v.
-#M #v #l #i elim (lt_or_ge … i l) #Hil
-[ >vdrop_lt //
-| >vdrop_ge //
-]
-qed.
-
-(* Main properties **********************************************************)
-
-theorem vdrop_vdrop_le_sym: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 →
- ↓[l1, m1] ↓[l2+m1, m2] v ≐⦋M⦌ ↓[l2, m2] ↓[l1, m1] v.
-#M #v #l1 #l2 #m1 #m2 #Hl12 #j elim (lt_or_ge … j l1) #Hjl1
-[ lapply (lt_to_le_to_lt … Hjl1 Hl12) -Hl12 #Hjl2
- >vdrop_lt // >vdrop_lt /2 width=3 by lt_to_le_to_lt/
- >vdrop_lt // >vdrop_lt //
-| >vdrop_ge // elim (lt_or_ge … j l2) #Hjl2 -Hl12
- [ >vdrop_lt /2 width=1 by lt_minus_to_plus/
- >vdrop_lt // >vdrop_ge //
- | >vdrop_ge /2 width=1 by monotonic_le_plus_l/
- >vdrop_ge // >vdrop_ge /2 width=1 by le_plus/
- ]
-]
-qed.
-
-lemma vdrop_vdrop_le: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 →
- ↓[l2, m2] ↓[l1, m1] v ≐⦋M⦌ ↓[l1, m1] ↓[l2+m1, m2] v.
-/3 width=1 by vdrop_vdrop_le_sym, veq_sym/ qed-.
-
-(* Properties on raise ******************************************************)
-
-lemma vdrop_raise_lt: ∀M,v,d,l,m,i. i ≤ l → ↓[l+1, m] [i⬐d] v ≐⦋M⦌ [i⬐d] ↓[l, m] v.
-#M #v #d #l #m #i #Hil #j elim (lt_or_eq_or_gt … j i) #Hij destruct
-[ lapply (lt_to_le_to_lt … Hij Hil) -Hil #Hjl
- >vdrop_lt /2 width=1 by le_S/ >raise_lt // >raise_lt // >vdrop_lt //
-| >vdrop_lt /2 width=1 by le_S_S/ >raise_eq >raise_eq //
-| lapply (ltn_to_ltO … Hij) #Hj
- >raise_gt // elim (lt_or_ge … j (l+1)) #Hlj
- [ -Hil >vdrop_lt // >vdrop_lt /2 width=2 by lt_plus_to_minus/ >raise_gt //
- | >vdrop_ge // >vdrop_ge /2 width=1 by le_plus_to_minus_r/
- >raise_gt /2 width=1 by le_plus/ >plus_minus //
- ]
-]
-qed.
-
-lemma raise_vdrop_lt: ∀M,v,d,l,m,i. i ≤ l → [i⬐d] ↓[l, m] v ≐⦋M⦌ ↓[l+1, m] [i⬐d] v.
-/3 width=1 by vdrop_raise_lt, veq_sym/ qed.
-
-lemma vdrop_raise_be: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m+1] [i⬐d] v ≐⦋M⦌ ↓[l, m] v.
-#M #v #d #l #m #i #Hli #Hilm #j elim (lt_or_ge … j l) #Hlj
-[ lapply (lt_to_le_to_lt … Hlj Hli) -Hli -Hilm #Hij
- >vdrop_lt // >vdrop_lt // >raise_lt //
-| lapply (transitive_le … (j+m) Hilm ?) -Hli -Hilm /2 width=1 by monotonic_le_plus_l/ #Hijm
- >vdrop_ge // >vdrop_ge // >raise_gt /2 width=1 by le_S_S/
-]
-qed.
-
-lemma vdrop_raise_be_sym: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m] v ≐⦋M⦌ ↓[l, m+1] [i⬐d] v.
-/3 width=1 by vdrop_raise_be, veq_sym/ qed.
-
-lemma vdrop_raise: ∀M,v,d,l. ↓[l, 1] [l⬐d] v ≐⦋M⦌ v.
-/3 width=3 by vdrop_raise_be, veq_trans/ qed.
-
-lemma vdrop_raise_sym: ∀M,v,d,l. v ≐⦋M⦌ ↓[l, 1] [l⬐d] v.
-/2 width=1 by veq_sym/ qed.
-
-lemma raise_vdrop: ∀M,v,i. [i⬐v i] ↓[i,1] v ≐⦋M⦌ v.
-#M #V #i #j elim (lt_or_eq_or_gt j i) #Hij destruct
-[ >raise_lt // >vdrop_lt //
-| >raise_eq //
-| >raise_gt // >vdrop_ge /2 width=1 by monotonic_pred/
- <plus_minus_m_m /2 width=2 by ltn_to_ltO/
-]
-qed.
-
-lemma raise_vdrop_sym: ∀M,v,i. v ≐⦋M⦌ [i⬐v i] ↓[i,1] v.
-/3 width=1 by raise_vdrop, veq_sym/ qed.
-
-lemma raise_vdrop_be: ∀M,v,l,m. ↓[l, m] v ≐⦋M⦌ [l⬐v (l+m)] ↓[l, m+1] v.
-#M #v #l #m #j elim (lt_or_eq_or_gt j l) #Hlj destruct
-[ >vdrop_lt // >raise_lt // >vdrop_lt //
-| >vdrop_ge // >raise_eq //
-| lapply (ltn_to_ltO … Hlj) #Hj
- >vdrop_ge /2 width=1 by lt_to_le/ >raise_gt //
- >vdrop_ge /4 width=1 by plus_minus, monotonic_pred, eq_f/
-]
-qed.
-
-lemma raise_vdrop_be_sym: ∀M,v,l,m. [l⬐v (l+m)] ↓[l, m+1] v ≐⦋M⦌ ↓[l, m] v.
-/3 width=1 by raise_vdrop_be, veq_sym/ qed.
-
-(* Forward lemmas on raise **************************************************)
-
-lemma vdrop_fwd_raise_be_S: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 →
- ↓[l, m+1] v1 ≐ v2.
-#M #v1 #v2 #d #l #m #Hv12 #j elim (lt_or_ge j l) #Hlj
-[ lapply (Hv12 j) -Hv12
- >vdrop_lt // >vdrop_lt // >raise_lt //
-| lapply (Hv12 (j+1))
- >vdrop_ge /2 width=1 by le_S/ >vdrop_ge // >raise_gt /2 width=1 by le_S_S/
+(**************************************************************************)
+(* ___ *)
+(* ||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/downspoon_3.ma".
+include "apps_2/models/model.ma".
+
+(* EVALUATION DROP **********************************************************)
+
+definition vdrop (M): nat → evaluation M → evaluation M ≝
+ λj,lv,i. tri … i j (lv i) (lv (↑i)) (lv (↑i)).
+
+interpretation "drop (model evaluation)"
+ 'DownSpoon M i lv = (vdrop M i lv).
+
+(* Basic properties *********************************************************)
+
+lemma vdrop_lt (M): ∀lv,j,i. i < j → (⫰{M}[j] lv) i = lv i.
+/2 width=1 by tri_lt/ qed-.
+
+lemma vdrop_ge (M): ∀lv,j,i. j ≤ i → (⫰{M}[j] lv) i = lv (↑i).
+#M #lv #j #i #Hji elim (le_to_or_lt_eq … Hji) -Hji #Hji destruct
+[ /2 width=1 by tri_gt/
+| /2 width=1 by tri_eq/
]
qed-.
-
-lemma raise_fwd_vdrop_be_S: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
- v2 ≐ ↓[l, m+1] v1.
-/3 width=2 by vdrop_fwd_raise_be_S, veq_sym/ qed-.
-
-lemma vdrop_fwd_raise_be_O: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 → v1 (l+m) = d.
-#M #v1 #v2 #d #l #m #Hv12 lapply (Hv12 l)
->vdrop_ge // >raise_eq //
-qed-.
-
-lemma raise_fwd_vdrop_be_O: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → d = v1 (l+m).
-/4 width=7 by vdrop_fwd_raise_be_O, veq_sym, sym_eq/ qed-.
-
-(* Inversion lemmas on raise ************************************************)
-
-lemma raise_inv_vdrop_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → [i⬐d] v1 ≐⦋M⦌ ↓[l+1, m] v2 →
- ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v.
-#M #v1 #v2 #d #l #m #i #Hil #Hv12
-lapply (Hv12 i) >raise_eq >vdrop_lt /2 width=1 by le_S_S/ #H destruct
-@(ex2_intro … (↓[i, 1] v2)) //
-@(veq_trans … (↓[i, 1] ↓[l+1, m] v2))
-/3 width=3 by vdrop_vdrop_le_sym, vdrop_veq, veq_trans/
-qed-.
-
-lemma vdrop_inv_raise_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → ↓[l+1, m] v2 ≐⦋M⦌ [i⬐d] v1 →
- ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v.
-/3 width=1 by raise_inv_vdrop_lt, veq_sym/ qed-.
-
-lemma vdrop_inv_raise_be: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 →
- v1 (l+m) = d ∧ ↓[l, m+1] v1 ≐ v2.
-/3 width=2 by vdrop_fwd_raise_be_O, vdrop_fwd_raise_be_S, conj/ qed-.
-
-lemma raise_inv_vdrop_be: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
- d = v1 (l+m) ∧ v2 ≐ ↓[l, m+1] v1.
-/3 width=2 by raise_fwd_vdrop_be_O, raise_fwd_vdrop_be_S, conj/ qed-.
--- /dev/null
+
+
+lemma vdrop_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v.
+#M #v #l #i elim (lt_or_ge … i l) #Hil
+[ >vdrop_lt //
+| >vdrop_ge //
+]
+qed.
+
+(* Main properties **********************************************************)
+
+theorem vdrop_vdrop_le_sym: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 →
+ ↓[l1, m1] ↓[l2+m1, m2] v ≐⦋M⦌ ↓[l2, m2] ↓[l1, m1] v.
+#M #v #l1 #l2 #m1 #m2 #Hl12 #j elim (lt_or_ge … j l1) #Hjl1
+[ lapply (lt_to_le_to_lt … Hjl1 Hl12) -Hl12 #Hjl2
+ >vdrop_lt // >vdrop_lt /2 width=3 by lt_to_le_to_lt/
+ >vdrop_lt // >vdrop_lt //
+| >vdrop_ge // elim (lt_or_ge … j l2) #Hjl2 -Hl12
+ [ >vdrop_lt /2 width=1 by lt_minus_to_plus/
+ >vdrop_lt // >vdrop_ge //
+ | >vdrop_ge /2 width=1 by monotonic_le_plus_l/
+ >vdrop_ge // >vdrop_ge /2 width=1 by le_plus/
+ ]
+]
+qed.
+
+lemma vdrop_vdrop_le: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 →
+ ↓[l2, m2] ↓[l1, m1] v ≐⦋M⦌ ↓[l1, m1] ↓[l2+m1, m2] v.
+/3 width=1 by vdrop_vdrop_le_sym, veq_sym/ qed-.
+
+(* Properties on raise ******************************************************)
+
+lemma vdrop_raise_lt: ∀M,v,d,l,m,i. i ≤ l → ↓[l+1, m] [i⬐d] v ≐⦋M⦌ [i⬐d] ↓[l, m] v.
+#M #v #d #l #m #i #Hil #j elim (lt_or_eq_or_gt … j i) #Hij destruct
+[ lapply (lt_to_le_to_lt … Hij Hil) -Hil #Hjl
+ >vdrop_lt /2 width=1 by le_S/ >raise_lt // >raise_lt // >vdrop_lt //
+| >vdrop_lt /2 width=1 by le_S_S/ >raise_eq >raise_eq //
+| lapply (ltn_to_ltO … Hij) #Hj
+ >raise_gt // elim (lt_or_ge … j (l+1)) #Hlj
+ [ -Hil >vdrop_lt // >vdrop_lt /2 width=2 by lt_plus_to_minus/ >raise_gt //
+ | >vdrop_ge // >vdrop_ge /2 width=1 by le_plus_to_minus_r/
+ >raise_gt /2 width=1 by le_plus/ >plus_minus //
+ ]
+]
+qed.
+
+lemma raise_vdrop_lt: ∀M,v,d,l,m,i. i ≤ l → [i⬐d] ↓[l, m] v ≐⦋M⦌ ↓[l+1, m] [i⬐d] v.
+/3 width=1 by vdrop_raise_lt, veq_sym/ qed.
+
+lemma vdrop_raise_be: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m+1] [i⬐d] v ≐⦋M⦌ ↓[l, m] v.
+#M #v #d #l #m #i #Hli #Hilm #j elim (lt_or_ge … j l) #Hlj
+[ lapply (lt_to_le_to_lt … Hlj Hli) -Hli -Hilm #Hij
+ >vdrop_lt // >vdrop_lt // >raise_lt //
+| lapply (transitive_le … (j+m) Hilm ?) -Hli -Hilm /2 width=1 by monotonic_le_plus_l/ #Hijm
+ >vdrop_ge // >vdrop_ge // >raise_gt /2 width=1 by le_S_S/
+]
+qed.
+
+lemma vdrop_raise_be_sym: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m] v ≐⦋M⦌ ↓[l, m+1] [i⬐d] v.
+/3 width=1 by vdrop_raise_be, veq_sym/ qed.
+
+lemma vdrop_raise: ∀M,v,d,l. ↓[l, 1] [l⬐d] v ≐⦋M⦌ v.
+/3 width=3 by vdrop_raise_be, veq_trans/ qed.
+
+lemma vdrop_raise_sym: ∀M,v,d,l. v ≐⦋M⦌ ↓[l, 1] [l⬐d] v.
+/2 width=1 by veq_sym/ qed.
+
+lemma raise_vdrop: ∀M,v,i. [i⬐v i] ↓[i,1] v ≐⦋M⦌ v.
+#M #V #i #j elim (lt_or_eq_or_gt j i) #Hij destruct
+[ >raise_lt // >vdrop_lt //
+| >raise_eq //
+| >raise_gt // >vdrop_ge /2 width=1 by monotonic_pred/
+ <plus_minus_m_m /2 width=2 by ltn_to_ltO/
+]
+qed.
+
+lemma raise_vdrop_sym: ∀M,v,i. v ≐⦋M⦌ [i⬐v i] ↓[i,1] v.
+/3 width=1 by raise_vdrop, veq_sym/ qed.
+
+lemma raise_vdrop_be: ∀M,v,l,m. ↓[l, m] v ≐⦋M⦌ [l⬐v (l+m)] ↓[l, m+1] v.
+#M #v #l #m #j elim (lt_or_eq_or_gt j l) #Hlj destruct
+[ >vdrop_lt // >raise_lt // >vdrop_lt //
+| >vdrop_ge // >raise_eq //
+| lapply (ltn_to_ltO … Hlj) #Hj
+ >vdrop_ge /2 width=1 by lt_to_le/ >raise_gt //
+ >vdrop_ge /4 width=1 by plus_minus, monotonic_pred, eq_f/
+]
+qed.
+
+lemma raise_vdrop_be_sym: ∀M,v,l,m. [l⬐v (l+m)] ↓[l, m+1] v ≐⦋M⦌ ↓[l, m] v.
+/3 width=1 by raise_vdrop_be, veq_sym/ qed.
+
+(* Forward lemmas on raise **************************************************)
+
+lemma vdrop_fwd_raise_be_S: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 →
+ ↓[l, m+1] v1 ≐ v2.
+#M #v1 #v2 #d #l #m #Hv12 #j elim (lt_or_ge j l) #Hlj
+[ lapply (Hv12 j) -Hv12
+ >vdrop_lt // >vdrop_lt // >raise_lt //
+| lapply (Hv12 (j+1))
+ >vdrop_ge /2 width=1 by le_S/ >vdrop_ge // >raise_gt /2 width=1 by le_S_S/
+]
+qed-.
+
+lemma raise_fwd_vdrop_be_S: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
+ v2 ≐ ↓[l, m+1] v1.
+/3 width=2 by vdrop_fwd_raise_be_S, veq_sym/ qed-.
+
+lemma vdrop_fwd_raise_be_O: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 → v1 (l+m) = d.
+#M #v1 #v2 #d #l #m #Hv12 lapply (Hv12 l)
+>vdrop_ge // >raise_eq //
+qed-.
+
+lemma raise_fwd_vdrop_be_O: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → d = v1 (l+m).
+/4 width=7 by vdrop_fwd_raise_be_O, veq_sym, sym_eq/ qed-.
+
+(* Inversion lemmas on raise ************************************************)
+
+lemma raise_inv_vdrop_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → [i⬐d] v1 ≐⦋M⦌ ↓[l+1, m] v2 →
+ ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v.
+#M #v1 #v2 #d #l #m #i #Hil #Hv12
+lapply (Hv12 i) >raise_eq >vdrop_lt /2 width=1 by le_S_S/ #H destruct
+@(ex2_intro … (↓[i, 1] v2)) //
+@(veq_trans … (↓[i, 1] ↓[l+1, m] v2))
+/3 width=3 by vdrop_vdrop_le_sym, vdrop_veq, veq_trans/
+qed-.
+
+lemma vdrop_inv_raise_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → ↓[l+1, m] v2 ≐⦋M⦌ [i⬐d] v1 →
+ ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v.
+/3 width=1 by raise_inv_vdrop_lt, veq_sym/ qed-.
+
+lemma vdrop_inv_raise_be: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 →
+ v1 (l+m) = d ∧ ↓[l, m+1] v1 ≐ v2.
+/3 width=2 by vdrop_fwd_raise_be_O, vdrop_fwd_raise_be_S, conj/ qed-.
+
+lemma raise_inv_vdrop_be: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
+ d = v1 (l+m) ∧ v2 ≐ ↓[l, m+1] v1.
+/3 width=2 by raise_fwd_vdrop_be_O, raise_fwd_vdrop_be_S, conj/ 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/models/model_vlift.ma".
+include "apps_2/models/vdrop.ma".
+
+(* EVALUATION DROP **********************************************************)
+
+(* Advanced properties with evaluation evaluation lift **********************)
+
+lemma vlift_vdrop_eq (M): ∀lv,i. lv ≐{?,dd M} ⫯[i←lv i]⫰[i]lv.
+#M #lv #i #j elim (lt_or_eq_or_gt j i) #Hji destruct
+[ >vlift_lt // >vdrop_lt //
+| >vlift_eq //
+| >vlift_gt // >vdrop_ge /2 width=1 by monotonic_pred/
+ <(lt_succ_pred … Hji) //
+]
+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/models/model_li.ma".
+include "apps_2/models/veq_vdrop.ma".
+
+(* EVALUATION EQUIVALENCE ***************************************************)
+
+(* Properties with local environment interpretation *************************)
+
+lemma li_repl_back (M) (gv): is_model M →
+ ∀L,lv1. lv1 ϵ ⟦L⟧[gv] →
+ ∀lv2. lv1 ≗{M} lv2 → lv2 ϵ ⟦L⟧[gv].
+#M #gv #HM #L #lv1 #H elim H -L -lv1 //
+[ #lv1 #d1 #K #V #_ #Hd #IH #y #H
+ elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #Hd12 #Hy
+ /5 width=5 by li_repl, li_abbr, ti_comp_l, mq/
+| #lv1 #d1 #K #W #_ #IH #y #H
+ elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #_ #Hy
+ /4 width=3 by li_repl, li_abst/
+| #lv1 #d1 #I #K #_ #IH #y #H
+ elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #_ #Hy
+ /4 width=3 by li_repl, li_unit/
+| #lv1 #lv #L #_ #Hlv1 #IH #lv2 #Hlv2
+ @IH /2 width=3 by exteq_veq_trans/
+]
+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/models/vdrop_vlift.ma".
+include "apps_2/models/veq.ma".
+
+(* EVALUATION EQUIVALENCE ***************************************************)
+
+(* Properties with evaluation drop ******************************************)
+
+lemma vdrop_comp (M): ∀i. compatible_2 … (vdrop M i) (veq M) (veq M).
+#M #i #lv1 #lv2 #Hlv12 #j elim (lt_or_ge j i) #Hji
+[ >vdrop_lt // >vdrop_lt //
+| >vdrop_ge // >vdrop_ge //
+]
+qed.
+
+(* Advanced inversion lemmas with evaluation evaluation lift ****************)
+
+lemma veq_inv_vlift_sn (M): ∀lv1,y2,d1,i. ⫯[i←d1]lv1 ≗{M} y2 →
+ ∃∃lv2,d2. lv1 ≗ lv2 & d1 ≗ d2 & ⫯[i←d2]lv2 ≐ y2.
+#M #lv1 #y2 #d1 #i #H
+@(ex3_2_intro)
+[5: @exteq_sym @vlift_vdrop_eq |1,2: skip
+| #j elim (lt_or_ge j i) #Hji
+ [ lapply (H j) -H >vlift_lt // >vdrop_lt //
+ | lapply (H (↑j)) -H >vlift_gt /2 width=1 by monotonic_le_plus_l/ >vdrop_ge //
+ ]
+| lapply (H i) >vlift_eq //
+]
+qed-.
(**************************************************************************)
include "apps_2/notation/models/ringeq_5.ma".
-include "apps_2/models/model_gi.ma".
-include "apps_2/models/model_li.ma".
-include "apps_2/models/model_props.ma".
+include "apps_2/models/li.ma".
+include "static_2/syntax/genv.ma".
(* DENOTATIONAL EQUIVALENCE ************************************************)
lemma deq_refl (M): is_model M →
∀G,L. reflexive … (deq M G L).
-/2 width=1 by mq/ qed.
+/2 width=1 by mr/ qed.
(*
lemma veq_sym: ∀M. symmetric … (veq M).
// qed-.
#h #M #H1M #H2M #G #L #T1 #T2 #H @(cpr_ind … H) -G -L -T1 -T2
[ /2 width=2 by deq_refl/
| #G #K #V1 #V2 #W2 #_ #IH #HVW2 #gv #v #H
- elim (li_inv_abbr … H) -H #lv #d #HK #Hd #H
- @(mr … H1M) [4,5: @(ti_ext_l … H1M … H) |1,2: skip ] -v
- lapply (lifts_SO_fwd_vlift … gv H1M H2M … HVW2 lv d) -HVW2 #HVW2
- @(seq_trans … H1M … HVW2) -W2
- @(seq_trans … H1M) [3: @IH // | skip ] -G -K -V2
- @(seq_canc_dx … H1M … Hd) -V1 /2 width=1 by ti_lref_vlift_eq/
+ elim (li_inv_abbr … H) -H // #lv #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 ] -W2
+ >vlift_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
- @(mr … H1M) [4,5: @(ti_ext_l … H1M … H) |1,2: skip ] -v
- lapply (lifts_SO_fwd_vlift … gv H1M H2M … HTU lv d) -HTU #HTU
- @(seq_trans … H1M … HTU) -U
- @(seq_trans … H1M) [3: @IH // | skip ] -G -K -T
- /2 width=1 by ti_lref_vlift_gt/
+ 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/
| #p * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv
- [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(md … H1M) |1,2: skip ] -p
- @(seq_trans … H1M) [3: @IHT /3 width=1 by li_abbr/ | skip ] -T2
- /4 width=1 by ti_comp_l, veq_refl, vlift_comp/
- | @(mx … H2M) /3 width=1 by li_abst/
+ [ @(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 li_abst, mx/
]
| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #gv #lv #Hlv
- [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(ma … H1M) |1,2: skip ]
- /3 width=1 by mc/
- | @(mr … H1M) [4,5: @(seq_sym … H1M) @(me … H1M) |1,2: skip ]
+ [ @(mq … H1M) [4,5: /3 width=2 by seq_sym, ma/ |1,2: skip ]
+ /3 width=1 by mp/
+ | @(mq … H1M) [4,5: /3 width=2 by seq_sym, me/ |1,2: skip ]
/2 width=1 by/
]
| #G #L #V #U1 #U2 #T2 #_ #IH #HTU2 #gv #lv #Hlv
- @(seq_trans … H1M) [2: @(md … H1M) | skip ]
- @(seq_trans … H1M) [2: @IH /3 width=1 by li_abbr, veq_refl/ | skip ] -G -L -U1
+ @(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/
| #G #L #V #T1 #T2 #_ #IH #gv #lv #Hlv
@(seq_trans … H1M) [2: @(me … H1M) | skip ]
/2 width=1 by/
| #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #_ #IHT #gv #lv #Hlv
- @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(ma … H1M) | @(md … H1M) ] |1,2: skip ]
- @(seq_trans … H1M) [3: @IHT /2 width=1 by li_abst/ | skip ] -T2
- @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(mb … H1M) | @(ti_comp_l … H1M) ] |1,2: skip ]
- [2: @vlift_comp [2: @(me … H1M) |4: @(veq_refl … H1M) |1,3: skip ] | skip ]
- /4 width=1 by ti_comp_l, veq_refl, vlift_comp/
+ @(mq … H1M) [4,5: /3 width=2 by seq_sym, ma, md/ |1,2: skip ]
+ @(mq … H1M)
+ [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/
+ @(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
- @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(ma … H1M) | @(md … H1M) ] |1,2: skip ]
- @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(mc … H1M) | @(ma … H1M) ] |1,2: skip ]
- [2: @IHV // |4: @(md … H1M) |1,3: skip ] -p -V1
- @(mc … H1M) [ /2 width=1 by lifts_SO_fwd_vlift/ ] -V -V2
- @(seq_trans … H1M) [2: @IHT /3 width=1 by li_abbr, veq_refl/ | skip ] -T1
- /4 width=1 by ti_comp_l, veq_refl, vlift_comp/
+ @(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
+ @(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/
]
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".
+include "apps_2/models/veq.ma".
+include "apps_2/notation/models/inwbrackets_4.ma".
+
+(* LOCAL ENVIRONMENT INTERPRETATION ****************************************)
+
+inductive li (M) (gv): relation2 lenv (evaluation M) ≝
+| li_atom: ∀lv. li M gv (⋆) lv
+| li_abbr: ∀lv,d,L,V. li M gv L lv → ⟦V⟧[gv, lv] = d → li M gv (L.ⓓV) (⫯[0←d]lv)
+| li_abst: ∀lv,d,L,W. li M gv L lv → li M gv (L.ⓛW) (⫯[0←d]lv)
+| li_unit: ∀lv,d,I,L. li M gv L lv → li M gv (L.ⓤ{I}) (⫯[0←d]lv)
+| li_veq : ∀lv1,lv2,L. li M gv L lv1 → lv1 ≗ lv2 → li M gv L lv2
+.
+
+interpretation "local environment interpretation (model)"
+ 'InWBrackets M gv L lv = (li M gv L lv).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact li_inv_abbr_aux (M) (gv): is_model M →
+ ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,V. Y = L.ⓓV →
+ ∃∃lv. lv ϵ ⟦L⟧[gv] & ⫯[0←⟦V⟧[gv,lv]]lv ≗ v.
+#M #gv #HM #v #Y #H elim H -v -Y
+[ #lv #K #W #H destruct
+| #lv #d #L #V #HL #HV #_ #K #W #H destruct
+ /3 width=3 by veq_refl, ex2_intro/
+| #lv #d #L #V #_ #_ #K #W #H destruct
+| #lv #d #I #L #_ #_ #K #W #H destruct
+| #lv1 #lv2 #L #_ #Hlv12 #IH #K #W #H destruct
+ elim IH -IH [|*: // ] #lv #HK #HW
+ /3 width=5 by veq_trans, ex2_intro/
+]
+qed-.
+
+lemma li_inv_abbr (M) (gv): is_model M →
+ ∀v,L,V. v ϵ ⟦L.ⓓV⟧{M}[gv] →
+ ∃∃lv. lv ϵ ⟦L⟧[gv] & ⫯[0←⟦V⟧[gv,lv]]lv ≗ v.
+/2 width=3 by li_inv_abbr_aux/ qed-.
+
+fact li_inv_abst_aux (M) (gv): is_model M →
+ ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,W. Y = L.ⓛW →
+ ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v.
+#M #gv #HM #v #Y #H elim H -v -Y
+[ #lv #K #U #H destruct
+| #lv #d #L #V #_ #_ #_ #K #U #H destruct
+| #lv #d #L #V #HL #_ #K #U #H destruct
+ /3 width=4 by veq_refl, ex2_2_intro/
+| #lv #d #I #L #_ #_ #K #U #H destruct
+| #lv1 #lv2 #L #_ #Hlv12 #IH #K #U #H destruct
+ elim IH -IH [|*: // ] #lv #d #HK #Hlv
+ /3 width=6 by veq_trans, ex2_2_intro/
+]
+qed-.
+
+lemma li_inv_abst (M) (gv): is_model M →
+ ∀v,L,W. v ϵ ⟦L.ⓛW⟧{M}[gv] →
+ ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v.
+/2 width=4 by li_inv_abst_aux/ qed-.
+
+fact li_inv_unit_aux (M) (gv): is_model M →
+ ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀I,L. Y = L.ⓤ{I} →
+ ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v.
+#M #gv #HM #v #Y #H elim H -v -Y
+[ #lv #J #K #H destruct
+| #lv #d #L #V #_ #_ #_ #J #K #H destruct
+| #lv #d #L #V #_ #_ #J #K #H destruct
+| #lv #d #I #L #HL #_ #J #K #H destruct
+ /3 width=4 by veq_refl, ex2_2_intro/
+| #lv1 #lv2 #L #_ #Hlv12 #IH #J #K #H destruct
+ elim IH -IH [|*: // ] #lv #d #HK #Hlv
+ /3 width=6 by veq_trans, ex2_2_intro/
+]
+qed-.
+
+lemma li_inv_unit (M) (gv): is_model M →
+ ∀v,I,L. v ϵ ⟦L.ⓤ{I}⟧{M}[gv] →
+ ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v.
+/2 width=4 by li_inv_unit_aux/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma li_fwd_bind (M) (gv): is_model M →
+ ∀v,I,L. v ϵ ⟦L.ⓘ{I}⟧{M}[gv] →
+ ∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v.
+#M #gv #HM #v * [ #I | * #V ] #L #H
+[ /2 width=2 by li_inv_unit/
+| elim (li_inv_abbr … H) // -H #lv #HL #Hv
+ /2 width=4 by ex2_2_intro/
+| /2 width=2 by li_inv_abst/
+]
+qed-.
+
+(* Basic_properties *********************************************************)
+
+lemma li_repl (M) (L): is_model M ->
+ replace_2 … (λgv.li M gv L) (veq …) (veq …).
+#M #L #HM #gv1 #lv1 #H elim H -L -lv1
+[ #lv1 #gv2 #Hgv #lv2 #Hlv /2 width=1 by li_atom/
+| #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/
+| #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
+ @li_veq /4 width=3 by li_unit, veq_refl/
+| #lv1 #lv #L #_ #Hlv1 #IH #gv2 #Hgv #lv2 #Hlv
+ /3 width=3 by veq_trans/
+]
+qed.
(* MODEL ********************************************************************)
record model: Type[1] ≝ {
- dd: Type[0]; (* denotations domain *)
- sq: relation2 dd dd; (* structural equivalence *)
- sv: nat → dd; (* sort evaluation *)
- ap: dd → dd → dd; (* application *)
- ti: (nat → dd) → (nat → dd) → term → dd (* term interperpretation *)
+(* Note: denotations domain *)
+ dd: Type[0];
+(* Note: structural equivalence *)
+ sq: relation2 dd dd;
+(* Note: sort evaluation *)
+ sv: nat → dd;
+(* Note: application *)
+ ap: dd → dd → dd;
+(* Note: term interperpretation *)
+ ti: (nat → dd) → (nat → dd) → term → dd
}.
interpretation "structural equivalence (model)"
+++ /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/genv.ma".
-
-(* GLOBAL ENVIRONMENT INTERPRETATION ***************************************)
+++ /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".
-include "apps_2/models/model_vlift.ma".
-include "apps_2/notation/models/inwbrackets_4.ma".
-
-(* LOCAL ENVIRONMENT INTERPRETATION ****************************************)
-
-inductive li (M) (gv): relation2 lenv (evaluation M) ≝
-| li_atom: ∀lv. li M gv (⋆) lv
-| li_abbr: ∀lv,d,L,V. li M gv L lv → ⟦V⟧[gv, lv] ≗ d → li M gv (L.ⓓV) (⫯[d]lv)
-| li_abst: ∀lv,d,L,W. li M gv L lv → li M gv (L.ⓛW) (⫯[d]lv)
-| li_unit: ∀lv,d,I,L. li M gv L lv → li M gv (L.ⓤ{I}) (⫯[d]lv)
-| li_repl: ∀lv1,lv2,L. li M gv L lv1 → lv1 ≐ lv2 → li M gv L lv2
-.
-
-interpretation "local environment interpretation (model)"
- 'InWBrackets M gv L lv = (li M gv L lv).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact li_inv_abbr_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,V. Y = L.ⓓV →
- ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⟦V⟧{M}[gv, lv] ≗ d & ⫯{M}[d]lv ≐ v.
-#M #gv #v #Y #H elim H -v -Y
-[ #lv #K #W #H destruct
-| #lv #d #L #V #HL #HV #_ #K #W #H destruct /2 width=5 by ex3_2_intro/
-| #lv #d #L #V #_ #_ #K #W #H destruct
-| #lv #d #I #L #_ #_ #K #W #H destruct
-| #lv1 #lv2 #L #_ #Hlv12 #IH #K #W #H destruct
- elim IH -IH [|*: // ] #lv #d #HK #HW #Hlv
- /3 width=5 by exteq_trans, ex3_2_intro/
-]
-qed-.
-
-lemma li_inv_abbr (M) (gv): ∀v,L,V. v ϵ ⟦L.ⓓV⟧{M}[gv] →
- ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⟦V⟧{M}[gv, lv] ≗ d & ⫯{M}[d]lv ≐ v.
-/2 width=3 by li_inv_abbr_aux/ qed-.
-
-fact li_inv_abst_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,W. Y = L.ⓛW →
- ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
-#M #gv #v #Y #H elim H -v -Y
-[ #lv #K #U #H destruct
-| #lv #d #L #V #_ #_ #_ #K #U #H destruct
-| #lv #d #L #V #HL #_ #K #U #H destruct /2 width=4 by ex2_2_intro/
-| #lv #d #I #L #_ #_ #K #U #H destruct
-| #lv1 #lv2 #L #_ #Hlv12 #IH #K #U #H destruct
- elim IH -IH [|*: // ] #lv #d #HK #Hlv
- /3 width=4 by exteq_trans, ex2_2_intro/
-]
-qed-.
-
-lemma li_inv_abst (M) (gv): ∀v,L,W. v ϵ ⟦L.ⓛW⟧{M}[gv] →
- ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
-/2 width=4 by li_inv_abst_aux/ qed-.
-
-fact li_inv_unit_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀I,L. Y = L.ⓤ{I} →
- ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
-#M #gv #v #Y #H elim H -v -Y
-[ #lv #J #K #H destruct
-| #lv #d #L #V #_ #_ #_ #J #K #H destruct
-| #lv #d #L #V #_ #_ #J #K #H destruct
-| #lv #d #I #L #HL #_ #J #K #H destruct /2 width=4 by ex2_2_intro/
-| #lv1 #lv2 #L #_ #Hlv12 #IH #J #K #H destruct
- elim IH -IH [|*: // ] #lv #d #HK #Hlv
- /3 width=4 by exteq_trans, ex2_2_intro/
-]
-qed-.
-
-lemma li_inv_unit (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓤ{I}⟧{M}[gv] →
- ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
-/2 width=4 by li_inv_unit_aux/ qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma li_fwd_bind (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓘ{I}⟧{M}[gv] →
- ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
-#m #gv #v * [ #I | * #V ] #L #H
-[ @(li_inv_unit … H)
-| elim (li_inv_abbr … H) -H #lv #d #Hl #_ #Hv
- /2 width=4 by ex2_2_intro/
-| @(li_inv_abst … H)
-]
-qed-.
(* MODEL ********************************************************************)
record is_model (M): Prop ≝ {
- mq: reflexive … (sq M);
- mr: replace_2 … (sq M) (sq M) (sq M);
- mc: compatible_3 … (ap M) (sq M) (sq M) (sq M);
+(* Note: equivalence: reflexivity *)
+ mr: reflexive … (sq M);
+(* Note: equivalence: compatibility *)
+ mq: replace_2 … (sq M) (sq M) (sq M);
+(* Note: application: compatibility *)
+ mp: compatible_3 … (ap M) (sq M) (sq M) (sq M);
+(* Note: interpretation: sort *)
ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s;
+(* Note: interpretation: local reference *)
ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i;
+(* Note: interpretation: global reference *)
mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l;
- md: ∀gv,lv,p,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[⟦V⟧[gv, lv]]lv];
- mi: ∀gv,lv1,lv2,p,W,T. ⟦W⟧{M}[gv, lv1] ≗ ⟦W⟧{M}[gv, lv2] →
- (∀d. ⟦T⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T⟧{M}[gv, ⫯[d]lv2]) →
- ⟦ⓛ{p}W.T⟧[gv, lv1] ≗ ⟦ⓛ{p}W.T⟧[gv, lv2];
+(* Note: interpretation: local δ-equivalence *)
+ md: ∀gv,lv,p,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[0←⟦V⟧[gv, lv]]lv];
+(* Note: interpretation: intensional abstraction *)
+ mi: ∀gv1,gv2,lv1,lv2,p,W,T. ⟦W⟧{M}[gv1, lv1] ≗ ⟦W⟧{M}[gv2, lv2] →
+ (∀d. ⟦T⟧{M}[gv1, ⫯[0←d]lv1] ≗ ⟦T⟧{M}[gv2, ⫯[0←d]lv2]) →
+ ⟦ⓛ{p}W.T⟧[gv1, lv1] ≗ ⟦ⓛ{p}W.T⟧[gv2, lv2];
+(* Note: interpretation: application *)
ma: ∀gv,lv,V,T. ⟦ⓐV.T⟧{M}[gv, lv] ≗ ⟦V⟧[gv, lv] @ ⟦T⟧[gv, lv];
+(* Note: interpretation: ϵ-equivalence *)
me: ∀gv,lv,W,T. ⟦ⓝW.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, lv];
- mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[d]lv]
+(* Note: interpretation: β-requivalence *)
+ mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[0←d]lv]
}.
record is_extensional (M): Prop ≝ {
- mx: ∀gv,lv1,lv2,p,W1,W2,T1,T2. ⟦W1⟧{M}[gv, lv1] ≗ ⟦W2⟧{M}[gv, lv2] →
- (∀d. ⟦T1⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T2⟧{M}[gv, ⫯[d]lv2]) →
- ⟦ⓛ{p}W1.T1⟧[gv, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv, lv2]
+(* Note: interpretation: extensional abstraction *)
+ mx: ∀gv1,gv2,lv1,lv2,p,W1,W2,T1,T2. ⟦W1⟧{M}[gv1, lv1] ≗ ⟦W2⟧{M}[gv2, lv2] →
+ (∀d. ⟦T1⟧{M}[gv1, ⫯[0←d]lv1] ≗ ⟦T2⟧{M}[gv2, ⫯[0←d]lv2]) →
+ ⟦ⓛ{p}W1.T1⟧[gv1, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv2, lv2]
}.
(* Basic properties *********************************************************)
lemma seq_sym (M): is_model M → symmetric … (sq M).
-/3 width=5 by mr, mq/ qed-.
+/3 width=5 by mq, mr/ qed-.
lemma seq_trans (M): is_model M → Transitive … (sq M).
-/3 width=5 by mr, mq/ qed-.
+/3 width=5 by mq, mr/ qed-.
lemma seq_canc_sn (M): is_model M → left_cancellable … (sq M).
/3 width=3 by seq_trans, seq_sym/ qed-.
∀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 mq/
+>vlift_eq /2 width=1 by mr/
qed.
lemma ti_lref_vlift_gt (M): is_model M →
- ∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[d]lv] ≗{M} ⟦#i⟧[gv,lv].
+ ∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[0←d]lv] ≗{M} ⟦#i⟧[gv,lv].
#M #HM #gv #lv #d #i
-@(mr … HM) [4,5: @(seq_sym … HM) @(ml … HM) |1,2: skip ]
->vlift_gt /2 width=1 by mq/
+@(mq … HM) [4,5: @(seq_sym … HM) /2 width=2 by ml/ |1,2: skip ]
+>vlift_gt /2 width=1 by mr/
qed.
+
+(* Basic Forward lemmas *****************************************************)
+
+lemma ti_fwd_mx_dx (M): is_model M →
+ ∀gv1,gv2,lv1,lv2,p,W1,W2,T1,T2.
+ ⟦ⓛ{p}W1.T1⟧[gv1, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv2, lv2] →
+ ∀d. ⟦T1⟧{M}[gv1, ⫯[0←d]lv1] ≗ ⟦T2⟧{M}[gv2, ⫯[0←d]lv2].
+#M #HM #gv1 #gv2 #lv1 #lv2 #p #W1 #W2 #T1 #T2 #H12 #d
+@(mq … HM) /3 width=5 by mb, mp, mr/
+qed-.
(**************************************************************************)
include "ground_2/lib/functions.ma".
-include "ground_2/lib/exteq.ma".
include "apps_2/notation/models/upspoon_4.ma".
-include "apps_2/notation/models/upspoon_3.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 "generic lift (model evaluation)"
- 'UpSpoon M i d lv = (vlift M i d lv).
-
interpretation "lift (model evaluation)"
- 'UpSpoon M d lv = (vlift M O d lv).
+ 'UpSpoon M i d lv = (vlift M i d lv).
(* Basic properties *********************************************************)
lemma vlift_gt (M): ∀lv,d,j,i. j < i → (⫯{M}[j←d] lv) i = lv (↓i).
/2 width=1 by tri_gt/ qed-.
-
-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.
+++ /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 "ground_2/notation/functions/downspoon_2.ma".
-include "apps_2/notation/models/downspoon_3.ma".
-include "apps_2/models/model.ma".
-
-(* EVALUATION DROP **********************************************************)
-
-definition vdrop (M): nat → evaluation M → evaluation M ≝
- λj,lv,i. tri … i j (lv i) (lv (↑i)) (lv (↑i)).
-
-interpretation "generic drop (model evaluation)"
- 'DownSpoon M i lv = (vdrop M i lv).
-
-interpretation "drop (model evaluation)"
- 'DownSpoon M lv = (vdrop M O lv).
-
-(* Basic properties *********************************************************)
-
-lemma vdrop_lt (M): ∀lv,j,i. i < j → (⫰{M}[j] lv) i = lv i.
-/2 width=1 by tri_lt/ qed-.
-
-lemma vdrop_ge (M): ∀lv,j,i. j ≤ i → (⫰{M}[j] lv) i = lv (↑i).
-#M #lv #j #i #Hji elim (le_to_or_lt_eq … Hji) -Hji #Hji destruct
-[ /2 width=1 by tri_gt/
-| /2 width=1 by tri_eq/
-]
-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
-[ >vdrop_lt // >vdrop_lt //
-| >vdrop_ge // >vdrop_ge //
-]
-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/models/model_vlift.ma".
-include "apps_2/models/vdrop.ma".
-
-(* EVALUATION DROP **********************************************************)
-
-(* Advanced properties with evaluation evaluation lift **********************)
-
-lemma vlift_vdrop_eq (M): ∀lv,i. lv ≐{?,dd M} ⫯[i←lv i]⫰[i]lv.
-#M #lv #i #j elim (lt_or_eq_or_gt j i) #Hji destruct
-[ >vlift_lt // >vdrop_lt //
-| >vlift_eq //
-| >vlift_gt // >vdrop_ge /2 width=1 by monotonic_pred/
- <(lt_succ_pred … Hji) //
-]
-qed.
include "apps_2/models/model_props.ma".
-(* EVALUATION EQUIVALENCE **************************************************)
+(* EVALUATION EQUIVALENCE ***************************************************)
definition veq (M): relation (evaluation M) ≝
λv1,v2. ∀d. v1 d ≗ v2 d.
lemma veq_refl (M): is_model M →
reflexive … (veq M).
-/2 width=1 by mq/ qed.
+/2 width=1 by mr/ qed.
lemma veq_repl (M): is_model M →
replace_2 … (veq M) (veq M) (veq M).
-/2 width=5 by mr/ qed-.
+/2 width=5 by mq/ qed-.
lemma veq_sym (M): is_model M → symmetric … (veq M).
/3 width=5 by veq_repl, veq_refl/ qed-.
lemma veq_trans (M): is_model M → Transitive … (veq M).
/3 width=5 by veq_repl, veq_refl/ qed-.
-(* Properties with extebsional equivalence **********************************)
+lemma veq_canc_sn (M): is_model M → left_cancellable … (veq M).
+/3 width=3 by veq_trans, veq_sym/ qed-.
-lemma ext_veq (M): is_model M →
- ∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2.
-/2 width=1 by mq/ qed.
+lemma veq_canc_dx (M): is_model M → right_cancellable … (veq M).
+/3 width=3 by veq_trans, veq_sym/ qed-.
-lemma veq_repl_exteq (M): is_model M →
- replace_2 … (veq M) (exteq …) (exteq …).
-/2 width=5 by mr/ qed-.
+(* Properties with evaluation lift ******************************************)
-lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv →
- ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2.
-// qed-.
-
-(* Properties with evaluation evaluation lift *******************************)
-
-theorem vlift_swap (M): ∀i1,i2. i1 ≤ i2 →
- ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≐{?,dd M} ⫯[↑i2←d2] ⫯[i1←d1] lv.
-#M #i1 #i2 #Hi12 #lv #d1 #d2 #j
+theorem vlift_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
-[ >vlift_lt // >vlift_lt /2 width=3 by lt_to_le_to_lt/
- >vlift_lt /3 width=3 by lt_S, lt_to_le_to_lt/ >vlift_lt //
-| >vlift_eq >vlift_lt /2 width=1 by monotonic_le_plus_l/ >vlift_eq //
+[ lapply (lt_to_le_to_lt … Hji1 Hi12) #Hji2
+ >vlift_lt // >vlift_lt // >vlift_lt /2 width=1 by lt_S/ >vlift_lt //
+ /2 width=1 by veq_refl/
+| >vlift_eq >vlift_lt /2 width=1 by monotonic_le_plus_l/ >vlift_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 //
- | >vlift_eq <(lt_succ_pred … Hji1) >vlift_eq //
- | >vlift_gt // >vlift_gt /2 width=1 by lt_minus_to_plus_r/ >vlift_gt /2 width=3 by le_to_lt_to_lt/
+ /2 width=1 by veq_refl/
+ | >vlift_eq <(lt_succ_pred … Hji1) >vlift_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 //
+ /2 width=1 by veq_refl/
]
]
-qed-.
+qed.
-lemma vlift_comp (M): ∀i. compatible_3 … (vlift M i) (sq M) (veq M) (veq M).
-#m #i #d1 #d2 #Hd12 #lv1 #lv2 #HLv12 #j
+lemma vlift_comp (M): is_model M →
+ ∀i. compatible_3 … (vlift 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 //
(* Properies with term interpretation ***************************************)
-lemma ti_comp_l (M): is_model M →
- ∀T,gv,lv1,lv2. lv1 ≗{M} lv2 →
- ⟦T⟧[gv, lv1] ≗ ⟦T⟧[gv, lv2].
+lemma ti_comp (M): is_model M →
+ ∀T,gv1,gv2. gv1 ≗ gv2 → ∀lv1,lv2. lv1 ≗ lv2 →
+ ⟦T⟧[gv1, lv1] ≗{M} ⟦T⟧[gv2, lv2].
#M #HM #T elim T -T * [||| #p * | * ]
-[ /4 width=3 by seq_trans, seq_sym, ms/
-| /4 width=5 by seq_sym, ml, mr/
+[ /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, mr/
-| /5 width=1 by vlift_comp, mi, mq/
-| /4 width=5 by seq_sym, ma, mc, mr/
-| /4 width=5 by seq_sym, me, mr/
+| /5 width=5 by vlift_comp, seq_sym, md, mq/
+| /5 width=1 by vlift_comp, mi, mr/
+| /4 width=5 by seq_sym, ma, mp, mq/
+| /4 width=5 by seq_sym, me, mq/
]
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.
+++ /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/models/model_li.ma".
-include "apps_2/models/veq_vdrop.ma".
-
-(* EVALUATION EQUIVALENCE **************************************************)
-
-(* Properties with local environment interpretation *************************)
-
-lemma li_repl_back (M) (gv): is_model M →
- ∀L,lv1. lv1 ϵ ⟦L⟧[gv] →
- ∀lv2. lv1 ≗{M} lv2 → lv2 ϵ ⟦L⟧[gv].
-#M #gv #HM #L #lv1 #H elim H -L -lv1 //
-[ #lv1 #d1 #K #V #_ #Hd #IH #y #H
- elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #Hd12 #Hy
- /5 width=5 by li_repl, li_abbr, ti_comp_l, mr/
-| #lv1 #d1 #K #W #_ #IH #y #H
- elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #_ #Hy
- /4 width=3 by li_repl, li_abst/
-| #lv1 #d1 #I #K #_ #IH #y #H
- elim (veq_inv_vlift_sn … H) -H #lv2 #d2 #Hlv12 #_ #Hy
- /4 width=3 by li_repl, li_unit/
-| #lv1 #lv #L #_ #Hlv1 #IH #lv2 #Hlv2
- @IH /2 width=3 by exteq_veq_trans/
-]
-qed-.
(* Forward lemmas with generic relocation ***********************************)
-fact lifts_fwd_vlift_aux (M) (gv): is_model M → is_extensional M →
- ∀f,T1,T2. ⬆*[f] T1 ≘ T2 → ∀m. 𝐁❴m,1❵ = f →
- ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[m←d]lv].
-#M #gv #H1M #H2M #f #T1 #T2 #H elim H -f -T1 -T2
-[ /4 width=3 by seq_trans, seq_sym, ms/
-| #f #i1 #i2 #Hi12 #m #Hm #lv #d destruct
- @(mr … H1M) [4,5: @(seq_sym … H1M) @(ml … H1M) |1,2: skip ]
+fact lifts_fwd_vlift_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
+[ #f #s #m #Hf #gv #lv #d
+ @(mq … H1M) [4,5: /3 width=2 by seq_sym, ms/ |1,2: skip ]
+ /2 width=1 by mr/
+| #f #i1 #i2 #Hi12 #m #Hm #gv #lv #d destruct
+ @(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 mq/
+ >vlift_lt /2 width=1 by mr/
| lapply (at_basic_inv_ge … Hi12) -Hi12 // #H destruct
- >vlift_gt /2 width=1 by mq, le_S_S/
+ >vlift_gt /2 width=1 by mr, le_S_S/
]
-| /4 width=3 by seq_trans, seq_sym, mg/
-| #f #p * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #lv #d destruct
- [ @(mr … H1M) [4,5: @(seq_sym … H1M) @(md … H1M) |1,2: skip ]
+| #f #l #m #Hf #gv #lv #d
+ @(mq … H1M) [4,5: /3 width=2 by seq_sym, mg/ |1,2: skip ]
+ /2 width=1 by mr/
+| #f #p * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #gv #lv #d destruct
+ [ @(mq … H1M) [4,5: /3 width=2 by seq_sym, md/ |1,2: skip ]
@(seq_trans … H1M)
- [2: @(ti_comp_l … H1M) | skip ]
- [2: @(vlift_comp … lv lv) | skip ]
- [3: /2 width=1 by veq_refl/ ]
- [2: @(IHV … d) // | skip ]
- @(seq_trans … H1M) [2: @(IHT (↑m) … d) // | skip ]
- /4 width=1 by seq_sym, ti_ext_l, vlift_swap/
- | @mx /2 width=1 by/ #d0 @(seq_trans … H1M)
- [3: @(seq_sym … H1M) @(ti_ext_l … H1M) | skip ]
- [2: @vlift_swap // | skip ]
+ [3: @ti_comp // | skip ]
+ [1,2: /2 width=2 by veq_refl/ ]
+ [2: @(vlift_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 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 width=1 by/
]
-| #f * #V1 #v2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #lv #d
- [ /4 width=5 by seq_sym, ma, mc, mr/
- | /4 width=5 by seq_sym, me, mr/
+| #f * #V1 #v2 #T1 #T2 #_ #_ #IHV #IHT #m #Hm #gv #lv #d
+ [ /4 width=5 by seq_sym, ma, mp, mq/
+ | /4 width=5 by seq_sym, me, mq/
]
]
qed-.
lemma lifts_SO_fwd_vlift (M) (gv): is_model M → is_extensional M →
∀T1,T2. ⬆*[1] T1 ≘ T2 →
- ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[d]lv].
+ ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[0←d]lv].
/2 width=3 by lifts_fwd_vlift_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/models/vdrop_vlift.ma".
-include "apps_2/models/veq.ma".
-
-(* EVALUATION EQUIVALENCE **************************************************)
-
-(* Properties with evaluation drop ******************************************)
-
-lemma vdrop_comp (M): ∀i. compatible_2 … (vdrop M i) (veq M) (veq M).
-#M #i #lv1 #lv2 #Hlv12 #j elim (lt_or_ge j i) #Hji
-[ >vdrop_lt // >vdrop_lt //
-| >vdrop_ge // >vdrop_ge //
-]
-qed.
-
-(* Advanced inversion lemmas with evaluation evaluation lift ****************)
-
-lemma veq_inv_vlift_sn (M): ∀lv1,y2,d1,i. ⫯[i←d1]lv1 ≗{M} y2 →
- ∃∃lv2,d2. lv1 ≗ lv2 & d1 ≗ d2 & ⫯[i←d2]lv2 ≐ y2.
-#M #lv1 #y2 #d1 #i #H
-@(ex3_2_intro)
-[5: @exteq_sym @vlift_vdrop_eq |1,2: skip
-| #j elim (lt_or_ge j i) #Hji
- [ lapply (H j) -H >vlift_lt // >vdrop_lt //
- | lapply (H (↑j)) -H >vlift_gt /2 width=1 by monotonic_le_plus_l/ >vdrop_ge //
- ]
-| lapply (H i) >vlift_eq //
-]
-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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE "models" COMPONENT **************************************)
-
-notation < "hvbox( ⫰[ break term 46 i ] break term 46 lv )"
- non associative with precedence 46
- for @{ 'DownSpoon $M $i $lv }.
-
-notation > "hvbox( ⫰[ break term 46 i ] break term 46 lv )"
- non associative with precedence 46
- for @{ 'DownSpoon ? $i $lv }.
-
-notation > "hvbox( ⫰{ term 46 M }[ break term 46 i ] break term 46 lv )"
- non associative with precedence 46
- for @{ 'DownSpoon $M $i $lv }.
--- /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( L ⨁[ break term 46 gv ] break term 46 lv ≘ break term 46 v )"
+ non associative with precedence 45
+ for @{ 'ROPlus $M $gv $L $lv $v }.
+
+notation > "hvbox( L ⨁[ break term 46 gv ] break term 46 lv ≘ break term 46 v )"
+ non associative with precedence 45
+ for @{ 'ROPlus ? $gv $L $lv $v }.
+
+notation > "hvbox( L ⨁{ break term 46 M }[ break term 46 gv ] break term 46 lv ≘ break term 46 v )"
+ non associative with precedence 45
+ for @{ 'ROPlus $M $gv $L $lv $v }.
+++ /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( ⫯[ break term 46 d ] break term 46 lv )"
- non associative with precedence 46
- for @{ 'UpSpoon $M $d $lv }.
-
-notation > "hvbox( ⫯[ break term 46 d ] break term 46 lv )"
- non associative with precedence 46
- for @{ 'UpSpoon ? $d $lv }.
-
-notation > "hvbox( ⫯{ term 46 M }[ break term 46 d ] break term 46 lv )"
- non associative with precedence 46
- for @{ 'UpSpoon $M $d $lv }.
[ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ]
}
]
- [ { "evaluation equivalence" * } {
- [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" "veq_lifts" * ]
+ [ { "local environment interpretation" * } {
+ [ "li" + "( ? ϵ ⟦?⟧{?}[?] )" "li_vlifts" * ]
}
]
- [ { "evaluation drop" * } {
- [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
+ [ { "multiple evaluation lift" * } {
+ [ "vlifts" + "( ?⨁{?}[?]? ≘ ? )" "vlifts_shift" * ]
+ }
+ ]
+ [ { "evaluation equivalence" * } {
+ [ "veq" + "( ? ≗{?} ? )" "veq_lifts" * ]
}
]
[ { "model declaration" * } {
[ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
- "model_vlift" + "( ⫯{?}[?]? )" + "( ⫯{?}[?←?]? )"
+ "model_vlift" + "( ⫯{?}[?←?]? )"
"model_props"
- "model_li" + "( ? ϵ ⟦?⟧{?}[?] )"
- "model_gi"
* ]
}
]
class "capitalize italic" { 0 }
class "italic" { 1 }
+(*
+ [ { "evaluation drop" * } {
+ [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
+ }
+ ]
+*)
--- /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 lenvs" ] "append" + "( ? + ? )" "append_length" * ]
}
]
[":"; "⁝"; ];
["."; "•"; "◦"; ];
["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
- ["+"; "⨭"; "⨮"; "⊕"; "⊞"; ];
+ ["+"; "â¨"; "⨮"; "â¨\81"; "â\8a\95"; "â\8a\9e"; ];
["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];
["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
projects / helm.git / commitdiff