From d7ff8dcf71f18a17fbf66696f0293cd411c1dbca Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 22 Jun 2022 13:38:11 +0200
Subject: [PATCH 1/1] update in delayed updating

+ dfr_lift_bi proved
---
 .../delayed_updating/reduction/dfr_lift.ma    | 56 ++++---------
 .../delayed_updating/reduction/ifr.ma         |  1 -
 .../substitution/fsubst_lift.ma               |  7 +-
 .../substitution/lift_constructors.ma         | 12 +--
 .../delayed_updating/substitution/lift_eq.ma  | 79 +++++++++++--------
 .../substitution/lift_prototerm_eq.ma         | 24 ++++++
 .../substitution/lift_rmap_head.ma            | 62 +++++++++++++++
 7 files changed, 154 insertions(+), 87 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_head.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
index 3c6e4d6d9..9fbf809b3 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
@@ -14,34 +14,19 @@
 
 include "delayed_updating/reduction/dfr.ma".
 include "delayed_updating/reduction/ifr.ma".
-(*
-include "delayed_updating/unwind/unwind2_constructors.ma".
-include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
-include "delayed_updating/unwind/unwind2_preterm_eq.ma".
-include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_head.ma".
-*)
+
+include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_constructors.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 include "delayed_updating/substitution/lift_path_head.ma".
-
-include "delayed_updating/syntax/prototerm_proper_constructors.ma".
-
+include "delayed_updating/substitution/lift_rmap_head.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
 (* Constructions with lift **************************************************)
-(*
-lemma pippo (f) (r):
-      ↑[↑[r]f](rᴿ) = (↑[f]r)ᴿ.
-#f #r @(list_ind_rcons … r) -r //
-#p * [ #n ] #IH
-[ <reverse_rcons <lift_path_d_sn <lift_rmap_d_dx
-  <lift_path_d_dx <reverse_rcons
-  <IH  
-*)
 
-theorem dfr_lift_bi (f) (p) (q) (t1) (t2): (*t1 ϵ 𝐓 → *)
+theorem dfr_lift_bi (f) (p) (q) (t1) (t2):
         t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]p,↑[↑[p◖𝗔◖𝗟]f]q] ↑[f]t2.
 #f #p #q #t1 #t2
 * #n * #H1n #Ht1 #Ht2
@@ -52,30 +37,17 @@ theorem dfr_lift_bi (f) (p) (q) (t1) (t2): (*t1 ϵ 𝐓 → *)
   <(lift_path_head … H1n) -H1n //
 | lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1n
   <lift_path_d_dx #Ht1 //
-| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
+| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
   @(subset_eq_trans … Ht2) -t2
-(*  
-  @(subset_eq_trans … (unwind2_term_fsubst …))
-  [ @fsubst_eq_repl [ // | // ]
-    @(subset_eq_trans … (unwind2_term_iref …))
-    @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
-    [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
-    @(subset_eq_trans … (unwind2_lift_term_after …))
-    @unwind2_term_eq_repl_sn
+  @(subset_eq_trans … (lift_term_fsubst …))
+  @fsubst_eq_repl [ // | // ]
+  @(subset_eq_trans … (lift_term_iref …))
+  @iref_eq_repl
+  @(subset_eq_canc_sn … (lift_term_grafted_S …))
+  @lift_term_eq_repl_sn
 (* Note: crux of the proof begins *)
-    @nstream_eq_inv_ext #m
-    <tr_compose_pap <tr_compose_pap
-    <tr_uni_pap <tr_uni_pap <tr_pap_plus
-    >list_append_rcons_sn in H1n; <reverse_append #H1n
-    lapply (unwind2_rmap_append_pap_closed f … H1n) #H2n
-    >nrplus_inj_dx in ⊢ (???%); <H2n -H2n
-    lapply (tls_unwind2_rmap_append_closed f … H1n) #H2n
-    <(tr_pap_eq_repl … H2n) -H2n -H1n //
+  >list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx
+  /2 width=1 by tls_lift_rmap_append_closed/
 (* Note: crux of the proof ends *)
-  | //
-  | /2 width=2 by ex_intro/
-  | //
-  ]
 ]
 qed.
-*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index a63368e1e..fcc12edbf 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -16,7 +16,6 @@ include "delayed_updating/unwind/unwind2_prototerm.ma".
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/syntax/path_head.ma".
-include "delayed_updating/syntax/path_reverse.ma".
 include "delayed_updating/notation/relations/black_rightarrow_if_4.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION ************************************************)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
index e1be5ded0..383bc24f9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
@@ -14,10 +14,7 @@
 
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
-(*
-include "delayed_updating/syntax/preterm.ma".
-include "delayed_updating/syntax/prototerm_proper.ma".
-*)
+
 (* FOCALIZED SUBSTITUTION ***************************************************)
 
 (* Constructions with lift for preterm **************************************)
@@ -43,7 +40,7 @@ lemma lift_term_fsubst_dx (f) (t) (u) (p):
   /2 width=3 by ex2_intro/
 | #Hq #H0 #H1 destruct
   @or_intror @conj [ /2 width=1 by in_comp_lift_path_term/ ] -Hq #r #Hr
-  elim (lift_path_inv_append_dx … Hr) -Hr #s1 #s2 #Hs1 #_ #H1 destruct
+  elim (lift_path_inv_append_sn … Hr) -Hr #s1 #s2 #Hs1 #_ #H1 destruct
   lapply (lift_path_inj … Hs1) -Hs1 #H1 destruct 
   /2 width=2 by/
 ]
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
index d7dde19bc..d36698b5f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
@@ -18,29 +18,29 @@ include "delayed_updating/syntax/prototerm_constructors_eq.ma".
 
 (* LIFT FOR PROTOTERM *******************************************************)
 
-lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
+lemma lift_term_iref_sn (f) (t:prototerm) (n:pnat):
       (𝛕f＠⧣❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛕n.t).
 #f #t #n #p * #q * #r #Hr #H1 #H2 destruct
 @(ex2_intro … (𝗱n◗𝗺◗r))
 /2 width=1 by in_comp_iref/
 qed-.
 
-lemma lift_iref_dx (f) (t) (n:pnat):
+lemma lift_term_iref_dx (f) (t) (n:pnat):
       ↑[f](𝛕n.t) ⊆ 𝛕f＠⧣❨n❩.↑[⇂*[n]f]t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
 /3 width=1 by in_comp_iref, in_comp_lift_path_term/
 qed-.
 
-lemma lift_iref (f) (t) (n:pnat):
+lemma lift_term_iref (f) (t) (n:pnat):
       (𝛕f＠⧣❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛕n.t).
-/3 width=1 by conj, lift_iref_sn, lift_iref_dx/
+/3 width=1 by conj, lift_term_iref_sn, lift_term_iref_dx/
 qed.
 
-lemma lift_iref_uni (t) (m) (n):
+lemma lift_term_iref_uni (t) (m) (n):
       (𝛕(n+m).t) ⇔ ↑[𝐮❨m❩](𝛕n.t).
 #t #m #n
-@(subset_eq_trans … (lift_iref …))
+@(subset_eq_trans … (lift_term_iref …))
 <tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
 /3 width=1 by iref_eq_repl, lift_term_id/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index 5ab8d7f05..317e1f424 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -16,7 +16,10 @@ include "delayed_updating/substitution/lift.ma".
 include "ground/relocation/tr_pap_pap.ma".
 include "ground/relocation/tr_pap_eq.ma".
 include "ground/relocation/tr_pn_eq.ma".
+include "ground/lib/stream_tls_plus.ma".
 include "ground/lib/stream_tls_eq.ma".
+include "ground/arith/nat_plus_rplus.ma".
+include "ground/arith/nat_rplus_pplus.ma".
 
 (* LIFT FOR PATH ************************************************************)
 
@@ -144,7 +147,27 @@ lemma lift_path_S_dx (f) (p):
 #f #p <lift_path_append //
 qed.
 
-(* Advanced inversions ******************************************************)
+(* Advanced constructions with proj_rmap ************************************)
+
+lemma lift_rmap_eq_repl (p):
+      stream_eq_repl … (λf1,f2. ↑[p]f1 ≗ ↑[p]f2).
+#p elim p -p //
+* [ #n ] #p #IH #f1 #f2 #Hf
+[ /3 width=1 by stream_tls_eq_repl/
+| /2 width=1 by/
+| /3 width=1 by tr_push_eq_repl/
+| /2 width=1 by/
+| /2 width=1 by/
+]
+qed.
+
+lemma tls_lift_rmap_d_dx (f) (p) (m) (n):
+      ⇂*[m+n]↑[p]f ≗ ⇂*[m]↑[p◖𝗱n]f.
+#f #p #m #n
+<lift_rmap_d_dx >nrplus_inj_dx >nrplus_inj_sn //
+qed.
+
+(* Advanced inversions with proj_path ***************************************)
 
 lemma lift_path_inv_empty (f) (p):
       (𝐞) = ↑[f]p → 𝐞 = p.
@@ -227,7 +250,7 @@ lemma lift_path_inv_S_sn (f) (p) (q):
 /2 width=3 by ex2_intro/
 qed-.
 
-lemma lift_path_inv_append_dx (q2) (q1) (p) (f):
+lemma lift_path_inv_append_sn (q2) (q1) (p) (f):
       q1●q2 = ↑[f]p →
       ∃∃p1,p2. q1 = ↑[f]p1 & q2 = ↑[↑[p1]f]p2 & p1●p2 = p.
 #q2 #q1 elim q1 -q1
@@ -235,27 +258,29 @@ lemma lift_path_inv_append_dx (q2) (q1) (p) (f):
 [ <list_append_empty_sn #H0 destruct
   /2 width=5 by ex3_2_intro/
 | <list_append_lcons_sn #H0
-  elim (lift_path_inv_d_sn … H0) -H0 #r1 #m1 #_ #_ #H0 #_ -IH
-    elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
-    elim Hq2 -Hq2 //
-  | elim (lift_path_inv_m_sn … H)
-  | elim (lift_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
-    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
-    @(ex3_2_intro … (r1●𝗟◗p1)) //
-    <structure_append <Hr1 -Hr1 //
-  | elim (lift_path_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
-    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
-    @(ex3_2_intro … (r1●𝗔◗p1)) //
-    <structure_append <Hr1 -Hr1 //
-  | elim (lift_path_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
-    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
-    @(ex3_2_intro … (r1●𝗦◗p1)) //
-    <structure_append <Hr1 -Hr1 //
-  ]
+  elim (lift_path_inv_d_sn … H0) -H0 #r1 #m1 #H1 #H0 #H2 destruct
+  elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+  elim (lift_path_inv_m_sn … H0) -H0 #r1 #H0 #H1 destruct
+  elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+  elim (lift_path_inv_L_sn … H0) -H0 #r1 #H0 #H1 destruct
+  elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+  elim (lift_path_inv_A_sn … H0) -H0 #r1 #H0 #H1 destruct
+  elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+  elim (lift_path_inv_S_sn … H0) -H0 #r1 #H0 #H1 destruct
+  elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
-(* Main inversions **********************************************************)
+(* Main inversions with proj_path *******************************************)
 
 theorem lift_path_inj (q:path) (p) (f):
         ↑[f]q = ↑[f]p → q = p.
@@ -264,7 +289,7 @@ theorem lift_path_inj (q:path) (p) (f):
   <(lift_path_inv_empty … H0) -H0 //
 | <lift_path_d_sn #H0
   elim (lift_path_inv_d_sn … H0) -H0 #r #h #H0
-  <(tr_pap_inj ????? H0) -h [1,3: // ] #Hr #H0 destruct
+  >(tr_pap_inj ???? H0) -k [1,3: // ] #Hr #H0 destruct
 | <lift_path_m_sn #H0
   elim (lift_path_inv_m_sn … H0) -H0 #r #Hr #H0 destruct
 | <lift_path_L_sn #H0
@@ -277,15 +302,3 @@ theorem lift_path_inj (q:path) (p) (f):
 <(IH … Hr) -r -IH //
 qed-.
 
-(* COMMENT 
-
-(* Advanced constructions with proj_rmap and stream_tls *********************)
-
-lemma lift_rmap_tls_d_dx (f) (p) (m) (n):
-      ⇂*[m+n]↑[p]f ≗ ⇂*[m]↑[p◖𝗱n]f.
-#f #p #m #n
-<lift_rmap_d_dx >nrplus_inj_dx
-/2 width=1 by tr_tls_compose_uni_dx/
-qed.
-
-*)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
index 920a16cf0..afe2ddd01 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
@@ -38,3 +38,27 @@ lemma lift_term_after (f1) (f2) (t):
 | @subset_equivalence_ext_f1_exteq /2 width=5/
 ]
 qed.
+
+lemma lift_term_grafted_sn (f) (t) (p):
+      ↑[↑[p]f](t⋔p) ⊆ (↑[f]t)⋔(↑[f]p).
+#f #t #p #q * #r #Hr #H0 destruct
+@(ex2_intro … Hr) -Hr
+<lift_path_append_sn //
+qed-.
+
+lemma lift_term_grafted_dx (f) (t) (p):
+      (↑[f]t)⋔(↑[f]p) ⊆ ↑[↑[p]f](t⋔p).
+#f #t #p #q * #r #Hr #H0
+elim (lift_path_inv_append_sn … (sym_eq … H0)) -H0
+#p0 #q0 #Hp0 #Hq0 #H0 destruct
+lapply (lift_path_inj … Hp0) -Hp0 #Hp0 destruct
+/2 width=1 by in_comp_lift_path_term/
+qed-.
+
+lemma lift_term_grafted (f) (t) (p):
+      ↑[↑[p]f](t⋔p) ⇔ (↑[f]t)⋔(↑[f]p).
+/3 width=1 by lift_term_grafted_sn, lift_term_grafted_dx, conj/ qed.
+
+lemma lift_term_grafted_S (f) (t) (p):
+      ↑[↑[p]f](t⋔(p◖𝗦)) ⇔ (↑[f]t)⋔((↑[f]p)◖𝗦).
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_head.ma
new file mode 100644
index 000000000..122262026
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_head.ma
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_reverse.ma".
+include "ground/lib/stream_eq_eq.ma".
+
+(* LIFT MAP FOR PATH ********************************************************)
+
+(* Constructions with path_head *********************************************)
+
+lemma tls_plus_lift_rmap_reverse_closed (f) (q) (p) (n) (k):
+      q = (↳[n]q)●p →
+      ⇂*[k]↑[pᴿ]f ≗ ⇂*[n+k]↑[qᴿ]f.
+#f #q elim q -q
+[ #p #n #k #Hp
+  elim (eq_inv_list_empty_append … Hp) -Hp #Hn #H0 destruct
+  <path_head_empty in Hn; #Hn
+  <(eq_inv_empty_labels … Hn) -n //
+| #l #q #IH #p #n @(nat_ind_succ … n) -n //
+  #n #_ #k cases l [ #m ]
+  [ <path_head_d_sn <list_append_lcons_sn #Hp
+    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp <nrplus_inj_sn
+    <reverse_lcons
+    @(stream_eq_trans … (tls_lift_rmap_d_dx …))
+    >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
+    >nsucc_unfold /2 width=1 by/
+  | <path_head_m_sn <list_append_lcons_sn #Hp
+    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+    <reverse_lcons <lift_rmap_m_dx /2 width=1 by/
+  | <path_head_L_sn <list_append_lcons_sn #Hp
+    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+    <reverse_lcons <lift_rmap_L_dx <nplus_succ_sn /2 width=1 by/
+  | <path_head_A_sn <list_append_lcons_sn #Hp
+    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+    <reverse_lcons <lift_rmap_A_dx /2 width=2 by/
+  | <path_head_S_sn <list_append_lcons_sn #Hp
+    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+    <reverse_lcons <lift_rmap_S_dx /2 width=2 by/
+  ]
+]
+qed-.
+
+lemma tls_lift_rmap_append_closed (f) (p) (q) (n):
+      qᴿ = ↳[n](p●q)ᴿ →
+      ↑[p]f ≗ ⇂*[n]↑[p●q]f.
+#f #p #q #n #H0
+>(reverse_reverse p) >(reverse_reverse q)
+/2 width=1 by tls_plus_lift_rmap_reverse_closed/
+qed.
-- 
2.39.2