+++ /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/fdrop_4.ma".
-include "apps_2/models/model_veq.ma".
-include "apps_2/models/model_raise.ma".
-
-(* MODEL ********************************************************************)
-
-definition lower: ∀M. nat → nat → evaluation M → evaluation M ≝
- λM,l,m,lv,i. tri … i l (lv i) (lv (i+m)) (lv (i+m)).
-
-interpretation "evaluation lower (models)"
- 'FDrop M l m lv = (lower M l m lv).
-
-(* Basic properties *********************************************************)
-
-lemma lower_lt: ∀M,lv,l,m,i. i < l → (↓[l, m]⦋M⦌ lv) i = lv i.
-/2 width=1 by tri_lt/ qed-.
-
-lemma lower_ge: ∀M,lv,l,m,i. l ≤ i → (↓[l, m]⦋M⦌ lv) i = lv (i+m).
-#M #lv #l #m #i #Hli elim (le_to_or_lt_eq … Hli) -Hli #Hli destruct
-[ /2 width=1 by tri_gt/
-| /2 width=1 by tri_eq/
-]
-qed-.
-
-lemma lower_veq: ∀M,v1,v2. v1 ≐⦋M⦌ v2 → ∀l,m. ↓[l, m] v1 ≐ ↓[l, m] v2.
-#m #v1 #v2 #Hv12 #l #m #i elim (lt_or_ge i l) #Hli
-[ >lower_lt // >lower_lt //
-| >lower_ge // >lower_ge //
-]
-qed.
-
-lemma lower_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v.
-#M #v #l #i elim (lt_or_ge … i l) #Hil
-[ >lower_lt //
-| >lower_ge //
-]
-qed.
-
-(* Main properties **********************************************************)
-
-theorem lower_lower_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
- >lower_lt // >lower_lt /2 width=3 by lt_to_le_to_lt/
- >lower_lt // >lower_lt //
-| >lower_ge // elim (lt_or_ge … j l2) #Hjl2 -Hl12
- [ >lower_lt /2 width=1 by lt_minus_to_plus/
- >lower_lt // >lower_ge //
- | >lower_ge /2 width=1 by monotonic_le_plus_l/
- >lower_ge // >lower_ge /2 width=1 by le_plus/
- ]
-]
-qed.
-
-lemma lower_lower_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 lower_lower_le_sym, veq_sym/ qed-.
-
-(* Properties on raise ******************************************************)
-
-lemma lower_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
- >lower_lt /2 width=1 by le_S/ >raise_lt // >raise_lt // >lower_lt //
-| >lower_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 >lower_lt // >lower_lt /2 width=2 by lt_plus_to_minus/ >raise_gt //
- | >lower_ge // >lower_ge /2 width=1 by le_plus_to_minus_r/
- >raise_gt /2 width=1 by le_plus/ >plus_minus //
- ]
-]
-qed.
-
-lemma raise_lower_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 lower_raise_lt, veq_sym/ qed.
-
-lemma lower_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
- >lower_lt // >lower_lt // >raise_lt //
-| lapply (transitive_le … (j+m) Hilm ?) -Hli -Hilm /2 width=1 by monotonic_le_plus_l/ #Hijm
- >lower_ge // >lower_ge // >raise_gt /2 width=1 by le_S_S/
-]
-qed.
-
-lemma lower_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 lower_raise_be, veq_sym/ qed.
-
-lemma lower_raise: ∀M,v,d,l. ↓[l, 1] [l⬐d] v ≐⦋M⦌ v.
-/3 width=3 by lower_raise_be, veq_trans/ qed.
-
-lemma lower_raise_sym: ∀M,v,d,l. v ≐⦋M⦌ ↓[l, 1] [l⬐d] v.
-/2 width=1 by veq_sym/ qed.
-
-lemma raise_lower: ∀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 // >lower_lt //
-| >raise_eq //
-| >raise_gt // >lower_ge /2 width=1 by monotonic_pred/
- <plus_minus_m_m /2 width=2 by ltn_to_ltO/
-]
-qed.
-
-lemma raise_lower_sym: ∀M,v,i. v ≐⦋M⦌ [i⬐v i] ↓[i,1] v.
-/3 width=1 by raise_lower, veq_sym/ qed.
-
-lemma raise_lower_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
-[ >lower_lt // >raise_lt // >lower_lt //
-| >lower_ge // >raise_eq //
-| lapply (ltn_to_ltO … Hlj) #Hj
- >lower_ge /2 width=1 by lt_to_le/ >raise_gt //
- >lower_ge /4 width=1 by plus_minus, monotonic_pred, eq_f/
-]
-qed.
-
-lemma raise_lower_be_sym: ∀M,v,l,m. [l⬐v (l+m)] ↓[l, m+1] v ≐⦋M⦌ ↓[l, m] v.
-/3 width=1 by raise_lower_be, veq_sym/ qed.
-
-(* Forward lemmas on raise **************************************************)
-
-lemma lower_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
- >lower_lt // >lower_lt // >raise_lt //
-| lapply (Hv12 (j+1))
- >lower_ge /2 width=1 by le_S/ >lower_ge // >raise_gt /2 width=1 by le_S_S/
-]
-qed-.
-
-lemma raise_fwd_lower_be_S: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
- v2 ≐ ↓[l, m+1] v1.
-/3 width=2 by lower_fwd_raise_be_S, veq_sym/ qed-.
-
-lemma lower_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)
->lower_ge // >raise_eq //
-qed-.
-
-lemma raise_fwd_lower_be_O: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → d = v1 (l+m).
-/4 width=7 by lower_fwd_raise_be_O, veq_sym, sym_eq/ qed-.
-
-(* Inversion lemmas on raise ************************************************)
-
-lemma raise_inv_lower_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 >lower_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 lower_lower_le_sym, lower_veq, veq_trans/
-qed-.
-
-lemma lower_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_lower_lt, veq_sym/ qed-.
-
-lemma lower_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 lower_fwd_raise_be_O, lower_fwd_raise_be_S, conj/ qed-.
-
-lemma raise_inv_lower_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_lower_be_O, raise_fwd_lower_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-.
(**************************************************************************)
include "basic_2/syntax/lenv.ma".
-include "apps_2/models/model_push.ma".
+include "apps_2/models/model_vlift.ma".
include "apps_2/notation/models/inwbrackets_4.ma".
(* LOCAL ENVIRONMENT INTERPRETATION ****************************************)
| 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)"
(* 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 * -v -Y
+ ∃∃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
+| #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.
+ ∃∃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 * -v -Y
+ ∃∃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
+| #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.
+ ∃∃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 * -v -Y
+ ∃∃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 #L #V #_ #J #K #H destruct
-| #lv #d #I #L #HL #J #K #H destruct /2 width=4 by ex2_2_intro/
+| #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.
+ ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv ≐ v.
/2 width=4 by li_inv_unit_aux/ qed-.
(* *)
(**************************************************************************)
-include "ground_2/lib/functions.ma".
-include "apps_2/models/model_push.ma".
+include "apps_2/models/model_vlift.ma".
(* 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 "apps_2/notation/models/upspoon_4.ma".
-include "apps_2/notation/models/upspoon_3.ma".
-include "apps_2/models/model.ma".
-
-(* MODEL ********************************************************************)
-
-definition push (M): nat → dd M → evaluation M → evaluation M ≝
- λj,d,lv,i. tri … i j (lv i) d (lv (↓i)).
-
-interpretation "generic push (model evaluation)"
- 'UpSpoon M i d lv = (push M i d lv).
-
-interpretation "push (model evaluation)"
- 'UpSpoon M d lv = (push M O d lv).
-
-(* Basic properties *********************************************************)
-
-lemma push_lt: ∀M,lv,d,j,i. i < j → (⫯{M}[j←d] lv) i = lv i.
-/2 width=1 by tri_lt/ qed-.
-
-lemma push_eq: ∀M,lv,d,i. (⫯{M}[i←d] lv) i = d.
-/2 width=1 by tri_eq/ qed-.
-
-lemma push_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 "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).
+
+(* 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-.
+
+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.
replace_2 … (veq M) (veq M) (veq M).
/2 width=5 by mr/ qed-.
-(* Properties with evaluation push ******************************************)
+lemma ext_veq (M): is_model M →
+ ∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2.
+/2 width=1 by mq/ qed.
+
+lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv →
+ ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2.
+// qed-.
-lemma push_comp (M): ∀i. compatible_3 … (push M i) (sq M) (veq M) (veq M).
+(* Properties with evaluation evaluation lift *******************************)
+
+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
elim (lt_or_eq_or_gt j i) #Hij destruct
-[ >(push_lt … Hij) >(push_lt … Hij) //
-| >(push_eq …) >(push_eq …) //
-| >(push_gt … Hij) >(push_gt … Hij) //
+[ >(vlift_lt … Hij) >(vlift_lt … Hij) //
+| >(vlift_eq …) >(vlift_eq …) //
+| >(vlift_gt … Hij) >(vlift_gt … Hij) //
]
qed.
-(* Inversion lemmas with evaluation push *************************************)
-
-axiom veq_inv_push_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
-*)
(* Properies with term interpretation ***************************************)
lemma ti_comp_l (M): is_model M →
[ /4 width=3 by seq_trans, seq_sym, ms/
| /4 width=5 by seq_sym, ml, mr/
| /4 width=3 by seq_trans, seq_sym, mg/
-| /5 width=5 by push_comp, seq_sym, md, mr/
-| /5 width=1 by push_comp, mi, mq/
+| /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/
]
(**************************************************************************)
include "apps_2/models/model_li.ma".
-include "apps_2/models/veq.ma".
+include "apps_2/models/veq_vdrop.ma".
(* EVALUATION EQUIVALENCE **************************************************)
∀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_push_sn … H) -H #lv2 #d2 #Hlv12 #Hd12 #H destruct
- /4 width=5 by li_abbr, ti_comp_l, mr/
+ 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_push_sn … H) -H #lv2 #d2 #Hlv12 #_ #H destruct
- /3 width=1 by li_abst/
+ 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_push_sn … H) -H #lv2 #d2 #Hlv12 #_ #H destruct
- /3 width=1 by li_unit/
+ 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-.
}
]
[ { "evaluation equivalence" * } {
- [ "veq" + "( ? ≗{?} ? )" "veq_li" * ]
+ [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" * ]
+ }
+ ]
+ [ { "evaluation drop" * } {
+ [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
}
]
[ { "model declaration" * } {
[ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
- "model_push" + "( ⫯{?}[?] )" + "( ⫯{?}[?←?] )"
+ "model_vlift" + "( ⫯{?}[?]? )" + "( ⫯{?}[?←?]? )"
"model_props"
"model_li" + "( ? ϵ ⟦?⟧{?}[?] )"
* ]
#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
qed-.
+lemma lt_succ_pred: ∀m,n. n < m → m = ↑↓m.
+#m #n #Hm >S_pred /2 width=2 by ltn_to_ltO/
+qed-.
+
fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
/2 width=1 by plus_minus_minus_be/ 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/relations/doteq_4.ma".
+include "ground_2/lib/relations.ma".
+
+(* EXTENSIONAL EQUIVALENCE **************************************************)
+
+definition exteq (A,B:Type[0]): relation (A → B) ≝
+ λf1,f2. ∀a. f1 a = f2 a.
+
+interpretation "extensional equivalence"
+ 'DotEq A B f1 f2 = (exteq A B f1 f2).
+
+(* Basic_properties *********************************************************)
+
+lemma exteq_refl (A) (B): reflexive … (exteq A B).
+// qed.
+
+lemma exteq_repl (A) (B): replace_2 … (exteq A B) (exteq A B) (exteq A B).
+// qed-.
+
+lemma exteq_sym (A) (B): symmetric … (exteq A B).
+/2 width=1 by exteq_repl/ qed-.
+
+lemma exteq_trans (A) (B): Transitive … (exteq A B).
+/2 width=1 by exteq_repl/ qed-.
+
definition right_identity (A) (f): predicate A ≝ λi. ∀a:A. a = f a i.
+definition compatible_2 (A) (B): relation3 … (relation A) (relation B) ≝
+ λf,Sa,Sb.
+ ∀a1,a2. Sa a1 a2 → Sb (f a1) (f a2).
+
definition compatible_3 (A) (B) (C): relation4 … (relation A) (relation B) (relation C) ≝
λf,Sa,Sb,Sc.
∀a1,a2. Sa a1 a2 → ∀b1,b2. Sb b1 b2 → Sc (f a1 b1) (f a2 b2).
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation < "hvbox( f1 ≐ break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'DotEq $A $B $f1 $f2 }.
+
+notation > "hvbox( f1 ≐ break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'DotEq ? ? $f1 $f2 }.
+
+notation > "hvbox( f1 ≐{ break term 46 A, break term 46 B } break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'DotEq $A $B $f1 $f2 }.
[ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
[ "list ( ◊ ) ( ? ⨮{?} ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} ⨮{?,?} ? ) ( |?| )" * ]
[ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
- [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "star" "ltc" * ]
+ [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "ltc" * ]
}
]
}
projects / helm.git / commitdiff