From 62d0f5f2c89830ebe884e6afee91eb68b68790fc Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 16 Feb 2022 23:45:20 +0100
Subject: [PATCH] update in delayed_updating

+ important additionsand corrections
---
 .../delayed_updating/reduction/dfr.ma         |  1 -
 .../delayed_updating/reduction/dfr_ifr.ma     |  1 +
 .../delayed_updating/substitution/lift.ma     | 10 +++-
 .../substitution/lift_depth.ma                | 31 +++++++----
 .../substitution/lift_structure_depth.ma      |  1 -
 .../substitution/lift_update.ma               | 52 +++++++++++++++++--
 6 files changed, 77 insertions(+), 19 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 42d9e0c76..89c959907 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -20,7 +20,6 @@ include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_balanced.ma".
 include "delayed_updating/syntax/path_depth.ma".
 include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
-include "ground/arith/nat_rplus.ma".
 include "ground/xoa/ex_1_2.ma".
 include "ground/xoa/and_4.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index 84e271530..25d728a89 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -52,6 +52,7 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
     @(subset_eq_canc_dx … (lift_term_after …))
     @lift_term_eq_repl_sn -t1
     @(stream_eq_trans … (tr_compose_uni_dx …))
+    @tr_compose_eq_repl
 (*    
     >nrplus_inj_dx <tr_pap_plus
 *)    
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index bfb66f1bc..0c083d998 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/relocation/tr_compose.ma".
-include "ground/relocation/tr_uni.ma".
+include "ground/relocation/tr_compose_pap.ma".
+include "ground/relocation/tr_uni_pap.ma".
 include "delayed_updating/syntax/path.ma".
 include "delayed_updating/notation/functions/uparrow_4.ma".
 include "delayed_updating/notation/functions/uparrow_2.ma".
@@ -166,6 +166,12 @@ lemma lift_rmap_S_dx (f) (p):
       ↑[p]f = ↑[p◖𝗦]f.
 // qed.
 
+lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
+      ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩.
+#f #p #n #m
+<lift_rmap_d_dx <tr_compose_pap <tr_uni_pap //
+qed.
+
 (* Advanced eliminations with path ******************************************)
 
 lemma path_ind_lift (Q:predicate …):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
index dc8290889..cefb45d49 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
@@ -14,17 +14,28 @@
 
 include "delayed_updating/substitution/lift.ma".
 include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/tr_pushs.ma".
+include "ground/relocation/tr_id_compose.ma".
+include "ground/relocation/tr_compose_compose.ma".
+include "ground/relocation/tr_compose_pn.ma".
+include "ground/relocation/tr_compose_eq.ma".
+include "ground/relocation/tr_pn_eq.ma".
+include "ground/lib/stream_eq_eq.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
-(* Basic constructions with depth ******************************************)
+(* Constructions with depth ************************************************)
 
-lemma pippo (p) (f):
-      (⫯*[❘p❘]f) ∘ (↑[p]𝐢) = ↑[p]f.
-#p elim p -p
-[ #f <lift_rmap_empty <lift_rmap_empty <tr_pushs_zero
-| * [ #n ] #p #IH #f //
-  <lift_rmap_d_sn <lift_rmap_d_sn <depth_d_sn
-  @(trans_eq … (IH …)) -IH
-      
+lemma lift_rmap_decompose (p) (f):
+      ↑[p]f ≗ (⫯*[❘p❘]f)∘(↑[p]𝐢).
+#p @(list_ind_rcons … p) -p
+[ #f <lift_rmap_empty <lift_rmap_empty <tr_pushs_zero //
+| #p * [ #n ] #IH #f //
+  [ <lift_rmap_d_dx <lift_rmap_d_dx <depth_d_dx
+    @(stream_eq_trans … (tr_compose_assoc …))
+    /2 width=1 by tr_compose_eq_repl/
+  | <lift_rmap_L_dx <lift_rmap_L_dx <depth_L_dx
+    <tr_pushs_succ <tr_compose_push_bi
+    /2 width=1 by tr_push_eq_repl/
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure_depth.ma
index 228e132bf..a85caab1c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure_depth.ma
@@ -15,7 +15,6 @@
 include "delayed_updating/substitution/lift.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/tr_pushs.ma".
 include "ground/arith/nat_pred_succ.ma".
 
 (* LIFT FOR PATH ***********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma
index 999b0e188..e30fc9d19 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma
@@ -21,15 +21,48 @@ include "ground/lib/stream_eq_eq.ma".
 
 (* Constructions with update ***********************************************)
 
-axiom arith1 (p,q:pnat) (n:nat):
-      nrplus (pplus p q) n = pplus p (nrplus q n).
+lemma lift_rmap_pap_le (f1) (f2) (p) (m:pnat) (l:nat):
+      ninj (m+⧣p+l) = ❘p❘ →
+      (↑[p]f1)@❨m❩ = (↑[p]f2)@❨m❩.
+#f1 #f2 #p @(list_ind_rcons … p) -p
+[ #m #l <depth_empty #H0 destruct
+| #p * [ #n ] #IH #m #l
+  [ <update_d_dx <depth_d_dx <lift_rmap_pap_d_dx <lift_rmap_pap_d_dx
+    <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
+    #H0 <(IH … l) -IH //
+  | /2 width=2 by/
+  | <update_L_dx <depth_L_dx <lift_rmap_L_dx <lift_rmap_L_dx
+    cases m -m // #m
+    <nrplus_succ_sn <nrplus_succ_sn >nsucc_inj #H0
+    <tr_pap_push <tr_pap_push
+    <(IH … l) -IH //
+  | /2 width=2 by/
+  | /2 width=2 by/
+  ]
+]
+qed.
 
-lemma pippo (f) (p) (m:pnat):
+lemma lift_rmap_pap_gt (f) (p) (m):
+      f@❨m+⧣p❩+❘p❘ = (↑[p]f)@❨m+❘p❘❩.
+#f #p @(list_ind_rcons … p) -p [ // ]
+#p * [ #n ] #IH #m
+[ <update_d_dx <depth_d_dx
+  <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
+  <lift_rmap_pap_d_dx >IH -IH //
+| //
+| <update_L_dx <depth_L_dx
+  <nrplus_succ_dx <nrplus_succ_dx <lift_rmap_L_dx <tr_pap_push //
+| //
+| //
+]
+qed.
+
+lemma lift_rmap_tls_gt (f) (p) (m:pnat):
       ⇂*[ninj (m+⧣p)]f ≗ ⇂*[ninj (m+❘p❘)]↑[p]f.
 #f #p @(list_ind_rcons … p) -p [ // ]
 #p * [ #n ] #IH #m
 [ <update_d_dx <depth_d_dx
-  <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <arith1
+  <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
   @(stream_eq_trans … (lift_rmap_tls_d_dx …))
   @(stream_eq_canc_dx … (IH …)) -IH //
 | //
@@ -38,4 +71,13 @@ lemma pippo (f) (p) (m:pnat):
 | //
 | //
 ]
-qed.  
+qed.
+
+lemma lift_rmap_tls_eq (f) (p):
+      ⇂*[⧣p]f ≗ ⇂*[↑❘p❘]↑[p]⫯f.
+(*
+#f #p @(list_ind_rcons … p) -p //
+#p * [ #n ] #IH //
+<update_d_dx <depth_d_dx <lift_rmap_d_dx
+@(stream_eq_trans … (tr_tls_compose_uni_dx …))
+*)
-- 
2.39.2