- commit of the "s_computation" component ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lifts.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
index 45cd021ebbb0e8d580f590c35570340114e08060..97db4d98ebc44802a34760c22715ef789b99b6a3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -1,3 +1,4 @@
+
 (**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
@@ -12,7 +13,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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".
 
@@ -34,8 +35,12 @@ inductive lifts: rtmap → relation term ≝
               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 ***************************************************)
 
@@ -101,7 +106,7 @@ lemma lifts_inv_bind1: ∀p,I,V1,T1,Y,f. ⬆*[f] ⓑ{p,I}V1.T1 ≡ Y →
                                 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.
@@ -116,7 +121,7 @@ qed-.
 
 (* 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-.
@@ -183,7 +188,7 @@ lemma lifts_inv_bind2: ∀p,I,V2,T2,X,f. ⬆*[f] X ≡ ⓑ{p,I}V2.T2 →
                                 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.
@@ -198,7 +203,7 @@ qed-.
 
 (* 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-.
@@ -245,7 +250,7 @@ lemma lifts_fwd_isid: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐈⦃f⦄ → T1 = T2.
 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/
@@ -254,7 +259,7 @@ lemma lifts_fwd_pair1: ∀I,V1,T1,Y,f. ⬆*[f] ②{I}V1.T1 ≡ Y →
 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/
@@ -264,20 +269,20 @@ qed-.
 
 (* 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 *)
@@ -291,6 +296,10 @@ elim (IHV1 f) -IHV1 #V2 #HV12
 ]
 qed-.
 
+lemma lift_lref_uni: ∀l,i. ⬆*[l] #i ≡ #(l+i).
+#l elim l -l /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 →
@@ -333,7 +342,7 @@ qed-.
 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