(* *)
(**************************************************************************)
-include "ground_2/relocation/nstream_id.ma".
+include "ground_2/relocation/nstream_after.ma".
include "basic_2/notation/relations/rliftstar_3.ma".
include "basic_2/grammar/term.ma".
lifts f (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
.
+interpretation "uniform relocation (term)"
+ 'RLiftStar i T1 T2 = (lifts (uni i) T1 T2).
+
interpretation "generic relocation (term)"
- 'RLiftStar cs T1 T2 = (lifts cs T1 T2).
+ 'RLiftStar f T1 T2 = (lifts f T1 T2).
+
(* Basic inversion lemmas ***************************************************)
Y = ⓑ{p,I}V2.T2.
/2 width=3 by lifts_inv_bind1_aux/ qed-.
-fact lifts_inv_flat1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
+fact lifts_inv_flat1_aux: ∀X,Y. ∀f:rtmap. ⬆*[f] X ≡ Y →
∀I,V1,T1. X = ⓕ{I}V1.T1 →
∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 &
Y = ⓕ{I}V2.T2.
(* Basic_1: was: lift1_flat *)
(* Basic_2A1: includes: lift_inv_flat1 *)
-lemma lifts_inv_flat1: ∀I,V1,T1,Y,f. ⬆*[f] ⓕ{I}V1.T1 ≡ Y →
+lemma lifts_inv_flat1: ∀I,V1,T1,Y. ∀f:rtmap. ⬆*[f] ⓕ{I}V1.T1 ≡ Y →
∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 &
Y = ⓕ{I}V2.T2.
/2 width=3 by lifts_inv_flat1_aux/ qed-.
X = ⓑ{p,I}V1.T1.
/2 width=3 by lifts_inv_bind2_aux/ qed-.
-fact lifts_inv_flat2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
+fact lifts_inv_flat2_aux: ∀X,Y. ∀f:rtmap. ⬆*[f] X ≡ Y →
∀I,V2,T2. Y = ⓕ{I}V2.T2 →
∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 &
X = ⓕ{I}V1.T1.
(* Basic_1: includes: lift_gen_flat *)
(* Basic_2A1: includes: lift_inv_flat2 *)
-lemma lifts_inv_flat2: ∀I,V2,T2,X,f. ⬆*[f] X ≡ ⓕ{I}V2.T2 →
+lemma lifts_inv_flat2: ∀I,V2,T2,X. ∀f:rtmap. ⬆*[f] X ≡ ⓕ{I}V2.T2 →
∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 &
X = ⓕ{I}V1.T1.
/2 width=3 by lifts_inv_flat2_aux/ qed-.
qed-.
(* Basic_2A1: includes: lift_fwd_pair1 *)
-lemma lifts_fwd_pair1: ∀I,V1,T1,Y,f. ⬆*[f] ②{I}V1.T1 ≡ Y →
+lemma lifts_fwd_pair1: ∀I,V1,T1,Y. ∀f:rtmap. ⬆*[f] ②{I}V1.T1 ≡ Y →
∃∃V2,T2. ⬆*[f] V1 ≡ V2 & Y = ②{I}V2.T2.
* [ #p ] #I #V1 #T1 #Y #f #H
[ elim (lifts_inv_bind1 … H) -H /2 width=4 by ex2_2_intro/
qed-.
(* Basic_2A1: includes: lift_fwd_pair2 *)
-lemma lifts_fwd_pair2: ∀I,V2,T2,X,f. ⬆*[f] X ≡ ②{I}V2.T2 →
+lemma lifts_fwd_pair2: ∀I,V2,T2,X. ∀f:rtmap. ⬆*[f] X ≡ ②{I}V2.T2 →
∃∃V1,T1. ⬆*[f] V1 ≡ V2 & X = ②{I}V1.T1.
* [ #p ] #I #V2 #T2 #X #f #H
[ elim (lifts_inv_bind2 … H) -H /2 width=4 by ex2_2_intro/
(* Basic properties *********************************************************)
-lemma lifts_eq_repl_back: ∀T1,T2. eq_stream_repl_back … (λf. ⬆*[f] T1 ≡ T2).
+lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≡ T2).
#T1 #T2 #f1 #H elim H -T1 -T2 -f1
-/4 width=3 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, push_eq_repl/
+/4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/
qed-.
-lemma lifts_eq_repl_fwd: ∀T1,T2. eq_stream_repl_fwd … (λf. ⬆*[f] T1 ≡ T2).
-#T1 #T2 @eq_stream_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *)
+lemma lifts_eq_repl_fwd: ∀T1,T2. eq_repl_fwd … (λf. ⬆*[f] T1 ≡ T2).
+#T1 #T2 @eq_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *)
qed-.
(* Basic_1: includes: lift_r *)
(* Basic_2A1: includes: lift_refl *)
lemma lifts_refl: ∀T,f. 𝐈⦃f⦄ → ⬆*[f] T ≡ T.
#T elim T -T *
-/4 width=1 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/
+/4 width=3 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/
qed.
(* Basic_2A1: includes: lift_total *)
]
qed-.
+lemma lift_SO: ∀i. ⬆*[1] #i ≡ #(⫯i).
+/2 width=1 by lifts_lref/ qed.
+
(* Basic_1: includes: lift_free (right to left) *)
(* Basic_2A1: includes: lift_split *)
lemma lifts_split_trans: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 →
lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⬆*[f] T1 ≡ T2).
#T1 elim T1 -T1
[ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ]
- #i2 #f elim (is_at_dec f i2)
+ #i2 #f elim (is_at_dec f i2) //
[ * /4 width=3 by lifts_lref, ex_intro, or_introl/
| #H @or_intror *
#X #HX elim (lifts_inv_lref2 … HX) -HX