--- /dev/null
+
+lemma pippo: ∀M,v1,v2,d,i. [i⬐d] v1 ≐⦋M⦌ v2 → v1 ≐⦋M⦌ ↓[i,1] v2.
+#M #v1 #v2 #d #i #H #j elim (lt_or_ge … j i) #Hij
+[ >lower_lt // <(H j) >raise_lt //
+| >lower_ge // <(H (j+1)) >raise_gt /2 width=1 by le_S_S/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reduction/cpr.ma".
+include "apps_2/models/model_drop.ma".
+
+(* MODEL ********************************************************************)
+
+(* Forward lemmas on context-sensitive parallel reduction for terms *********)
+
+lemma sound_fwd_cpr: ∀M. sound M → extensional M →
+ ∀sv,gv,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 →
+ ∀lv. lv ∈ 〚L〛⦋M⦌{sv, gv} → 〚T1〛{sv, gv, lv} = 〚T2〛{sv, gv, lv}.
+#M #H1M #H2M #sv #gv #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
+[ #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #lv #Hlv >(m2 … H1M)
+ <(sound_fwd_lift … H1M H2M … HVW2) -HVW2
+ lapply (sound_drop … HLK … Hlv) // -L -H2M #H
+ elim (li_inv_ldef … H) -H #v #HK #H
+ elim (lower_inv_raise_be … H) -H #H >H -H #Hlv
+ <IHV12 -IHV12 /3 width=3 by sound_ti_eq_l, li_veq, veq_sym/
+| #a * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #lv #Hlv
+ [ >(m4 … H1M) >(m4 … H1M) -H1M <IHV12 -IHV12 /3 width=1 by li_ldef/
+ | @(mx … H2M) -H2M /3 width=1 by li_ldec/
+ ]
+| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #lv #Hlv
+ [ >(m6 … H1M) >(m6 … H1M) -H1M /3 width=1 by eq_f2/
+ | -IHV12 >(m7 … H1M) >(m7 … H1M) -H1M /2 width=1 by/
+ ]
+| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #lv #Hlv >(m4 … H1M)
+ >IHU12 -IHU12 /2 width=1 by li_ldef/
+ <(sound_fwd_lift … H1M H2M … HTU2) -H2M -HTU2
+ /2 width=1 by sound_ti_eq_l/
+| #G #L #V #T1 #T2 #_ #IHT12 #lv #Hlv >(m7 … H1M) -H1M /2 width=1 by/
+| #a #G #L #V1 #V2 #W1 #w2 #T1 #T2 #_ #_ #_ #IHV12 #_ #IHT12 #lv #Hlv
+ >(m6 … H1M) >(m8 … H1M) >(m4 … H1M) >(m7 … H1M) -H1M
+ >IHV12 -IHV12 /3 width=1 by li_ldec/
+| #a #G #L #V1 #V2 #W2 #U1 #U2 #T1 #T2 #_ #HVW2 #_ #_ #IHV12 #IHU12 #IHT12 #lv #Hlv
+ >(m6 … H1M) >(m4 … H1M) >(m4 … H1M) >(m6 … H1M)
+ >IHV12 -IHV12 // <IHU12 -IHU12 // @eq_f2 /3 width=1 by li_ldef/
+ <(sound_fwd_lift … H1M H2M … HVW2) -H2M -HVW2
+ /2 width=1 by sound_ti_eq_l/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/drop.ma".
+include "apps_2/models/model_li.ma".
+include "apps_2/models/model_lift.ma".
+
+(* MODEL ********************************************************************)
+
+(* Properties on basic slicing **********************************************)
+
+lemma sound_drop: ∀M. sound M → extensional M →
+ ∀sv,gv,L,K,s,l,m. ⬇[s, l, m] L ≡ K →
+ ∀lv. lv ∈ 〚L〛⦋M⦌{sv, gv} → ↓[l, m] lv ∈ 〚K〛⦋M⦌{sv, gv}.
+#M #H1M #H2M #sv #gv #L #K #s #l #m #H elim H -l -m /2 width=3 by li_veq/
+[ * #L #K #V #m #_ #IHLK #x #H -H1M -H2M
+ [ elim (li_inv_ldef … H) | elim (li_inv_ldec … H) ] -H
+ /4 width=5 by li_veq, lower_raise_be, lower_veq/ (* 2 x li_veq *)
+| * #L #K #W #V #l #m #_ #HVW #IHLK #x #H
+ [ elim (li_inv_ldef … H) #lv | elim (li_inv_ldec … H) #lv #d ] -H
+ <(sound_fwd_lift M H1M H2M sv gv … HVW lv) -H1M -H2M -HVW
+ /5 width=6 by li_veq, li_ldec, li_ldef, lower_raise_lt, lower_veq/ (* 2 x li_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 "basic_2/substitution/lift.ma".
+include "apps_2/models/model_lower.ma".
+include "apps_2/models/model_sound.ma".
+
+(* MODEL ********************************************************************)
+
+(* Forward lemmas on basic relocation ***************************************)
+
+lemma sound_fwd_lift: ∀M. sound M → extensional M →
+ ∀sv,gv,T1,T2,l,m. ⬆[l, m] T1 ≡ T2 →
+ ∀lv. 〚T1〛{sv, gv, ↓[l, m]⦋M⦌ lv} = 〚T2〛{sv, gv, lv}.
+#M #H1M #H2M #sv #gv #T1 #T2 #l #m #H elim H -T1 -T2 -l -m
+[ #k #l #m #lv >(m1 … H1M) >(m1 … H1M) -H1M //
+| #i #l #m #Hil #lv >(m2 … H1M) >(m2 … H1M) -H1M >lower_lt //
+| #i #l #m #Hli #lv >(m2 … H1M) >(m2 … H1M) -H1M >lower_ge //
+| #p #l #m #lv >(m3 … H1M) >(m3 … H1M) -H1M //
+| #a * #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #lv
+ [ >(m4 … H1M) >(m4 … H1M) /3 width=1 by raise_lower_lt, sound_ti_eq_l/
+ | @(mx … H2M) /3 width=1 by raise_lower_lt, sound_ti_eq_l/
+ ]
+| * #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #lv
+ [ >(m6 … H1M) >(m6 … H1M) /3 width=1 by eq_f2/
+ | >(m7 … H1M) >(m7 … H1M) /2 width=1 by/
+ ]
+]
+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/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
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/lift_neg.ma".
+include "apps_2/models/model_sound.ma".
+
+(* MODEL ********************************************************************)
+
+lemma sound_ti_eq_nlift: ∀M. sound M → ∀sv,gv,U,lv1,lv2.
+ (∀i. (∀T. ⬆[i, 1]T ≡ U → ⊥) → lv1 i = lv2 i) →
+ 〚U〛⦋M⦌{sv, gv, lv1} = 〚U〛⦋M⦌{sv, gv, lv2}.
+#M #HM #sv #gv #U elim U -U * [||| #a * | * ]
+[ #k #lv1 #lv2 #H >(m1 … HM) >(m1 … HM) -HM //
+| #i #lv1 #lv2 #H >(m2 … HM) >(m2 … HM) -HM
+ /3 width=7 by lift_inv_lref2_be/
+| #p #lv1 #lv2 #H >(m3 … HM) >(m3 … HM) -HM //
+| #W #U #IHW #IHU #lv1 #lv2 #H >(m4 … HM) >(m4 … HM)
+ @IHU -IHU #i @(nat_ind_plus … i) -i
+ [ /5 width=9 by nlift_bind_sn/
+ | #i #_ #H0 >raise_gt // >raise_gt //
+ /4 width=9 by nlift_bind_dx/
+ ]
+| #W #U #IHW #IHU #lv1 #lv2 #H @(m5 … HM) /5 width=9 by nlift_bind_sn/
+ #d @IHU -IHU #i @(nat_ind_plus … i) -i //
+ #i #_ #H0 lapply (nlift_bind_dx … H0) -H0
+ #H0 lapply (H i ?) -H /2 width=5 by/ -H0 #H
+ >raise_gt // >raise_gt //
+| #W #U #IHW #IHU #lv1 #lv2 #H >(m6 … HM) >(m6 … HM)
+ /6 width=8 by nlift_flat_sn, nlift_flat_dx, eq_f2/
+| #W #U #_ #IHU #lv1 #lv2 #H >(m7 … HM) >(m7 … HM)
+ /5 width=8 by nlift_flat_dx/
+]
+qed-.
(* *)
(**************************************************************************)
+include "ground_2/lib/functions.ma".
include "apps_2/models/model_push.ma".
(* 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);
ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s;
ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i;
mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l;
(∀d. ⟦T1⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T2⟧{M}[gv, ⫯[d]lv2]) →
⟦ⓛ{p}W1.T1⟧[gv, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv, lv2]
}.
+
+(* Basic properties *********************************************************)
+
+lemma seq_sym (M): is_model M → symmetric … (sq M).
+/3 width=5 by mr, mq/ qed-.
+
+lemma seq_trans (M): is_model M → Transitive … (sq M).
+/3 width=5 by mr, mq/ qed-.
lemma veq_refl (M): is_model M →
reflexive … (veq M).
/2 width=1 by mq/ qed.
+
+lemma veq_repl (M): is_model M →
+ replace_2 … (veq M) (veq M) (veq M).
+/2 width=5 by mr/ qed-.
+
+(* Properties with evaluation push ******************************************)
+
+lemma push_comp (M): ∀i. compatible_3 … (push 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) //
+]
+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.
(*
-lemma veq_sym: ∀M. symmetric … (veq M).
-// qed-.
+#M #lv1 #y2 #d1 #i #H
+*)
+(* Properies with term interpretation ***************************************)
-theorem veq_trans: ∀M. transitive … (veq M).
-// qed-.
-*)
\ No newline at end of file
+lemma ti_comp_l (M): is_model M →
+ ∀T,gv,lv1,lv2. lv1 ≗{M} lv2 →
+ ⟦T⟧[gv, lv1] ≗ ⟦T⟧[gv, 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=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/
+| /4 width=5 by seq_sym, ma, mc, mr/
+| /4 width=5 by seq_sym, me, mr/
+]
+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.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_push_sn … H) -H #lv2 #d2 #Hlv12 #Hd12 #H destruct
+ /4 width=5 by 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/
+| #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/
+]
+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 $d $lv }.
+
+notation > "hvbox( ⫰[ break term 46 i ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'DownSpoon ? $d $lv }.
+
+notation > "hvbox( ⫰{ term 46 M }[ break term 46 i ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'DownSpoon $M $d $lv }.
]
}
]
+ class "orange"
+ [ { "models" * } {
+ [ { "denotational equivalence" * } {
+ [ "deq" + "( ? ⊢ ? ≗{?} ? )" * ]
+ }
+ ]
+ [ { "evaluation equivalence" * } {
+ [ "veq" + "( ? ≗{?} ? )" "veq_li" * ]
+ }
+ ]
+ [ { "model declaration" * } {
+ [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
+ "model_push" + "( ⫯{?}[?] )" + "( ⫯{?}[?←?] )"
+ "model_props"
+ "model_li" + "( ? ϵ ⟦?⟧{?}[?] )"
+ * ]
+ }
+ ]
+ }
+ ]
(*
class "yellow"
[ { "MLTT1" * } {
(* FUNCTIONS ****************************************************************)
-definition left_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f i a.
+definition left_identity (A) (f): predicate A ≝ λi. ∀a:A. a = f i a.
-definition right_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f a i.
+definition right_identity (A) (f): predicate A ≝ λi. ∀a:A. a = f a i.
+
+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).
lemma insert_eq: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a.
/2 width=1 by/ qed-.
+definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝
+ λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2.
+
(* Inclusion ****************************************************************)
definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
projects / helm.git / commitdiff