+++ /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-.
(* *)
(**************************************************************************)
+include "ground_2/relocation/rtmap_basic.ma".
include "basic_2/relocation/lifts.ma".
include "apps_2/models/veq.ma".
(* EVALUATION EQUIVALENCE **************************************************)
-lemma pippo (M) (gv): is_model M → is_extensional M →
- ∀f,T1,T2. ⬆*[f] T1 ≘ T2 → ∀n. ⫯*[n] 𝐔❴1❵ = f →
- ∀lv,d. ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, ⫯[n←d]lv].
+(* 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 #n #Hn #lv #d
+| #f #i1 #i2 #Hi12 #m #Hm #lv #d destruct
@(mr … H1M) [4,5: @(seq_sym … H1M) @(ml … H1M) |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/
+ | lapply (at_basic_inv_ge … Hi12) -Hi12 // #H destruct
+ >vlift_gt /2 width=1 by mq, le_S_S/
+ ]
| /4 width=3 by seq_trans, seq_sym, mg/
-| #f #p * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #n #Hn #lv #d
+| #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 ]
@(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 … 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 ]
/2 width=1 by/
]
-| #f * #V1 #v2 #T1 #T2 #_ #_ #IHV #IHT #n #Hn #lv #d
+| #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/
]
-]
+]
+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].
+/2 width=3 by lifts_fwd_vlift_aux/ qed-.
}
]
[ { "evaluation equivalence" * } {
- [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" * ]
+ [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" "veq_lifts" * ]
}
]
[ { "evaluation drop" * } {
--- /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( 𝐁❴ break term 46 l, break term 46 h ❵ )"
+ non associative with precedence 90
+ for @{ 'Basic $l $h }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/basic_2.ma".
+include "ground_2/relocation/rtmap_at.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+definition basic: nat → nat → rtmap ≝ λm,n. ⫯*[m] 𝐔❴n❵.
+
+interpretation "basic relocation (rtmap)"
+ 'Basic m n = (basic m n).
+
+(* Prioerties with application **********************************************)
+
+lemma at_basic_lt: ∀m,n,i. i < m → @⦃i, 𝐁❴m,n❵⦄ ≘ i.
+#m elim m -m [ #n #i #H elim (lt_zero_false … H) ]
+#m #IH #n * [ /2 width=2 by refl, at_refl/ ]
+#i #H lapply (lt_S_S_to_lt … H) -H /3 width=7 by refl, at_push/
+qed.
+
+lemma at_basic_ge: ∀m,n,i. m ≤ i → @⦃i, 𝐁❴m,n❵⦄ ≘ n+i.
+#m elim m -m //
+#m #IH #n #j #H
+elim (le_inv_S1 … H) -H #i #Hmi #H destruct
+/3 width=7 by refl, at_push/
+qed.
+
+(* Inversion lemmas with application ****************************************)
+
+lemma at_basic_inv_lt: ∀m,n,i,j. i < m → @⦃i, 𝐁❴m,n❵⦄ ≘ j → i = j.
+/3 width=4 by at_basic_lt, at_mono/ qed-.
+
+lemma at_basic_inv_ge: ∀m,n,i,j. m ≤ i → @⦃i, 𝐁❴m,n❵⦄ ≘ j → n+i = j.
+/3 width=4 by at_basic_ge, at_mono/ qed-.
"rtmap_fcla ( 𝐂⦃?⦄ ≘ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )"
"rtmap_sle ( ? ⊆ ? )" "rtmap_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≘ ? )" "rtmap_sor ( ? ⋓ ? ≘ ? )"
"rtmap_at ( @⦃?,?⦄ ≘ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )"
+ "rtmap_basic ( 𝐁❴?,?❵ )"
* ]
[ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
"" "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
projects / helm.git / commitdiff