From 80e953c112c66f884d167e7ff876c1f6289e1400 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 7 Feb 2022 23:49:05 +0100
Subject: [PATCH] update in delayed_updating

+ WIP on updating grafted trees
---
 .../notation/functions/class_i_0.ma           | 19 +++++
 .../delayed_updating/reduction/dfr_ifr.ma     |  2 +-
 .../substitution/fsubst_lift.ma               |  2 +-
 .../delayed_updating/substitution/lift.ma     | 18 +++++
 .../substitution/lift_preterm_eq.ma           | 71 ++++++++++++++-----
 .../substitution/lift_structure.ma            | 70 ++++++++++++++++--
 .../delayed_updating/syntax/path_inner.ma     | 61 ++++++++++++++++
 .../delayed_updating/syntax/path_proper.ma    |  7 +-
 .../lambdadelta/ground/lib/list_rcons.ma      | 22 +++++-
 9 files changed, 243 insertions(+), 29 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_i_0.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_i_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_i_0.ma
new file mode 100644
index 000000000..628ffce52
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_i_0.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝐈 )"
+  non associative with precedence 70
+  for @{ 'ClassI }.
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 fc47782e7..66affad94 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -33,7 +33,7 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
 | #g <lift_rmap_structure <depth_structure
   >tr_pushs_swap <tr_pap_pushs_le //
 | lapply (in_comp_lift_bi f … Ht1) -Ht1 -H0t1 -Hb -Ht2
-  <lift_d_empty_dx //
+  <lift_path_d_empty_dx //
 | lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (lift_fsubst …))
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 c98698864..bf5c9b6f6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
@@ -29,7 +29,7 @@ lemma lift_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 →
 | * #q #Hq #H1 #H0
   @(ex2_intro … H1) @or_intror @conj // *
   [ <list_append_empty_dx #H2 destruct
-    elim (lift_root f q) #r #_ #Hr /2 width=2 by/
+    elim (lift_path_root f q) #r #_ #Hr /2 width=2 by/
   | #l #r #H2 destruct
     @H0 -H0 [| <lift_append_proper_dx /2 width=3 by ppc_lcons/ ]
   ]
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index 3a6991a92..f2b004a18 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -144,6 +144,24 @@ lemma lift_rmap_append (p2) (p1) (f):
 ]
 qed.
 
+(* Advanced constructions with proj_rmap and path_rcons *********************)
+
+lemma lift_rmap_m_dx (f) (p):
+      ↑[p]f = ↑[p◖𝗺]f.
+// qed.
+
+lemma lift_rmap_L_dx (f) (p):
+      (⫯↑[p]f) = ↑[p◖𝗟]f.
+// qed.
+
+lemma lift_rmap_A_dx (f) (p):
+      ↑[p]f = ↑[p◖𝗔]f.
+// qed.
+
+lemma lift_rmap_S_dx (f) (p):
+      ↑[p]f = ↑[p◖𝗦]f.
+// qed.
+
 (* Advanced eliminations with path ******************************************)
 
 lemma path_ind_lift (Q:predicate …):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm_eq.ma
index 91facd7c5..8143f8600 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm_eq.ma
@@ -17,32 +17,69 @@ include "delayed_updating/syntax/preterm.ma".
 include "delayed_updating/substitution/lift_structure.ma".
 include "delayed_updating/substitution/lift_prototerm.ma".
 
+lemma pippo (p):
+      ⊗p ϵ 𝐈.
+#p @(list_ind_rcons … p) -p
+[ <structure_empty //
+| #p * [ #n ] #IH
+  [ <structure_d_dx //
+  | <structure_m_dx //
+  | <structure_L_dx //
+  | <structure_A_dx //
+  | <structure_S_dx //
+  ]
+]
+qed.
+
 (* LIFT FOR PRETERM *********************************************************)
 
 (* Constructions with subset_equivalence ************************************)
 
-lemma lift_grafted_S_sn (f) (t) (p):
-      ↑[↑[p]f](t⋔(p◖𝗦)) ⊆ (↑[f]t)⋔((⊗p)◖𝗦).
-#f #t #p #q * #r #Hr #H0 destruct
+lemma lift_grafted_sn (f) (t) (p): p ϵ 𝐈 →
+      ↑[↑[p]f](t⋔p) ⊆ (↑[f]t)⋔(⊗p).
+#f #t #p #Hp #q * #r #Hr #H0 destruct
 @(ex2_intro … Hr) -Hr
-<list_append_rcons_sn <list_append_rcons_sn
-<lift_append_proper_dx //
+<lift_append_inner_sn //
 qed-.
 
-lemma lift_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
-      (↑[f]t)⋔((⊗p)◖𝗦) ⊆ ↑[↑[p]f](t⋔(p◖𝗦)).
-#f #t #p #Hp #Ht #q * #r #Hr
-<list_append_rcons_sn #H0
-elim (lift_inv_append_proper_dx … (sym_eq … H0)) -H0 //
+lemma lift_grafted_dx (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      (↑[f]t)⋔(⊗p) ⊆ ↑[↑[p]f](t⋔p).
+#f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
+elim (lift_inv_append_inner_sn … (sym_eq … H0)) -H0 //
 #p0 #q0 #Hp0 #Hq0 #H0 destruct
 <(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
-elim (lift_path_inv_S_sn … (sym_eq … Hq0)) -Hq0
-#r1 #r2 #Hr1 #Hr2 #H0 destruct
-lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1)
-[ /2 width=2 by ex_intro/ ] -Hr1 #Hr1 destruct
 /2 width=1 by in_comp_lift_bi/
 qed-.
 
-lemma lift_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
-      ↑[↑[p]f](t⋔(p◖𝗦)) ⇔ (↑[f]t)⋔((⊗p)◖𝗦).
-/3 width=1 by lift_grafted_S_sn, conj, lift_grafted_S_dx/ qed.
+lemma lift_grafted (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      ↑[↑[p]f](t⋔p) ⇔ (↑[f]t)⋔(⊗p).
+/3 width=1 by lift_grafted_sn, conj, lift_grafted_dx/ qed.
+
+(*
+
+-lemma lift_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ ������ →
+-      (↑[f]t)⋔((⊗p)◖������) ⊆ ↑[↑[p]f](t⋔(p◖������)).
+-#f #t #p #Hp #Ht #q * #r #Hr
+-<list_append_rcons_sn #H0
+-elim (lift_inv_append_proper_dx … (sym_eq … H0)) -H0 //
++lemma lift_grafted_dx (f) (t) (p): p ϵ ������ → p ϵ ▵t → t ϵ ������ →
++      (↑[f]t)⋔(⊗p) ⊆ ↑[↑[p]f](t⋔p).
++#f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
++elim (lift_inv_append_inner_sn … (sym_eq … H0)) -H0 //
+ #p0 #q0 #Hp0 #Hq0 #H0 destruct
+ <(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
+-elim (lift_path_inv_S_sn … (sym_eq … Hq0)) -Hq0
+-#r1 #r2 #Hr1 #Hr2 #H0 destruct
+-lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1)
+-[ /2 width=2 by ex_intro/ ] -Hr1 #Hr1 destruct
+ /2 width=1 by in_comp_lift_bi/
+ qed-.
+ 
+-lemma lift_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ ������ →
+-      ↑[↑[p]f](t⋔(p◖������)) ⇔ (↑[f]t)⋔((⊗p)◖������).
+-/3 width=1 by lift_grafted_S_sn, conj, lift_grafted_S_dx/ qed.
++lemma lift_grafted (f) (t) (p): p ϵ ������ → p ϵ ▵t → t ϵ ������ →
++      ↑[↑[p]f](t⋔p) ⇔ (↑[f]t)⋔(⊗p).
++/3 width=1 by lift_grafted_sn, conj, lift_grafted_dx/ qed.
+
+*)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
index 449317ee6..2a219e0ff 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -14,6 +14,7 @@
 
 include "delayed_updating/substitution/lift_eq.ma".
 include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_inner.ma".
 include "delayed_updating/syntax/path_proper.ma".
 include "ground/xoa/ex_4_2.ma".
 
@@ -53,34 +54,51 @@ lemma lift_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
 ]
 qed-.
 
-(* Advanced constructions with structure ************************************)
+(* Constructions with inner condition for path ******************************)
 
-lemma lift_d_empty_dx (n) (p) (f):
+lemma lift_append_inner_sn (p1) (p2) (f): p1 ϵ 𝐈 →
+      (⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
+#p1 @(list_ind_rcons … p1) -p1 // #p1 *
+[ #n ] #_ #p2 #f #Hp1
+[ elim (pic_inv_d_dx … Hp1)
+| <list_append_rcons_sn <lift_append_proper_dx //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_L_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_A_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_S_dx <list_append_rcons_sn //
+]
+qed-.
+
+(* Advanced constructions with proj_path ************************************)
+
+lemma lift_path_d_empty_dx (n) (p) (f):
       (⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
 #n #p #f <lift_append_proper_dx // 
 qed.
 
-lemma lift_m_dx (p) (f):
+lemma lift_path_m_dx (p) (f):
       ⊗p = ↑[f](p◖𝗺).
 #p #f <lift_append_proper_dx //
 qed.
 
-lemma lift_L_dx (p) (f):
+lemma lift_path_L_dx (p) (f):
       (⊗p)◖𝗟 = ↑[f](p◖𝗟).
 #p #f <lift_append_proper_dx //
 qed.
 
-lemma lift_A_dx (p) (f):
+lemma lift_path_A_dx (p) (f):
       (⊗p)◖𝗔 = ↑[f](p◖𝗔).
 #p #f <lift_append_proper_dx //
 qed.
 
-lemma lift_S_dx (p) (f):
+lemma lift_path_S_dx (p) (f):
       (⊗p)◖𝗦 = ↑[f](p◖𝗦).
 #p #f <lift_append_proper_dx //
 qed.
 
-lemma lift_root (f) (p):
+lemma lift_path_root (f) (p):
       ∃∃r. 𝐞 = ⊗r & ⊗p●r = ↑[f]p.
 #f #p @(list_ind_rcons … p) -p
 [ /2 width=3 by ex2_intro/
@@ -211,3 +229,41 @@ lemma lift_inv_append_proper_dx (q2) (q1) (p) (f):
   ]
 ]
 qed-.
+
+(* Inversions with inner condition for path *********************************)
+
+lemma lift_inv_append_inner_sn (q1) (q2) (p) (f):
+      q1 ϵ 𝐈 → q1●q2 = ↑[f]p →
+      ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]f]p2 = q2 & p1●p2 = p.
+#q1 @(list_ind_rcons … q1) -q1
+[ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
+  /2 width=5 by ex3_2_intro/
+| #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
+  [ elim (pic_inv_d_dx … Hq2)
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_m_sn … (sym_eq … H2))
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_L_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+    @(ex3_2_intro … (p1●r2◖𝗟)) [1,3: // ]
+    [ <structure_append <structure_L_dx <Hr2 -Hr2 //
+    | <list_append_assoc <list_append_rcons_sn //
+    ]
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_A_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+    @(ex3_2_intro … (p1●r2◖𝗔)) [1,3: // ]
+    [ <structure_append <structure_A_dx <Hr2 -Hr2 //
+    | <list_append_assoc <list_append_rcons_sn //
+    ]
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_S_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+    @(ex3_2_intro … (p1●r2◖𝗦)) [1,3: // ]
+    [ <structure_append <structure_S_dx <Hr2 -Hr2 //
+    | <list_append_assoc <list_append_rcons_sn //
+    ]
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
new file mode 100644
index 000000000..8e9fccefe
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/syntax/path.ma".
+include "delayed_updating/notation/functions/class_i_0.ma".
+include "ground/lib/subset.ma".
+
+(* INNER CONDITION FOR PATH *************************************************)
+
+definition pic: predicate path ≝
+           λp. ∀q,n. q◖𝗱n = p → ⊥
+.
+
+interpretation
+  "inner condition (path)"
+  'ClassI = (pic).
+
+(* Basic constructions ******************************************************)
+
+lemma pic_empty: 𝐞 ϵ 𝐈.
+#q #n #H0
+elim (eq_inv_list_empty_rcons ??? (sym_eq … H0))
+qed.
+
+lemma pic_m_dx (p): p◖𝗺 ϵ 𝐈.
+#p #q #n #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+qed.
+
+lemma pic_L_dx (p): p◖𝗟 ϵ 𝐈.
+#p #q #n #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+qed.
+
+lemma pic_A_dx (p): p◖𝗔 ϵ 𝐈.
+#p #q #n #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+qed.
+
+lemma pic_S_dx (p): p◖𝗦 ϵ 𝐈.
+#p #q #n #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+qed.
+
+(* Basic inversions ********************************************************)
+
+lemma pic_inv_d_dx (p) (n):
+      p◖𝗱n ϵ 𝐈 → ⊥.
+#p #n #H0 @H0 -H0 //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
index fca2eb91a..66de8a4f6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
@@ -35,10 +35,15 @@ qed.
 
 (* Basic inversions ********************************************************)
 
+lemma ppc_inv_empty:
+      (𝐞) ϵ 𝐏 → ⊥.
+#H0 @H0 -H0 //
+qed-.
+
 lemma ppc_inv_lcons (p):
       p ϵ 𝐏 → ∃∃l,q. l◗q = p.
 *
-[ #H elim H -H //
+[ #H0 elim (ppc_inv_empty … H0)
 | #l #q #_ /2 width=3 by ex1_2_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 9d2fcfaac..322235e7a 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -47,8 +47,26 @@ lemma list_append_rcons_dx (A):
 
 lemma eq_inv_list_empty_rcons (A):
       ∀l,a. ⓔ = l⨭{A}a → ⊥.
-#A #l #a #H
-elim (eq_inv_list_empty_append … H) -H #_ #H destruct
+#A #l #a #H0
+elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
+qed-.
+
+(* Advanced inversions ******************************************************)
+
+lemma eq_inv_list_rcons_bi (A):
+      ∀a1,a2,l1,l2. l1 ⨭{A} a1 = l2 ⨭ a2 →
+      ∧∧ l1 = l2 & a1 = a2.
+#A #a1 #a2 #l1 elim l1 -l1 [| #b1 #l1 #IH ] *
+[ <list_append_empty_sn <list_append_empty_sn #H destruct
+  /2 width=1 by conj/
+| #b2 #l2 <list_append_empty_sn <list_append_lcons_sn #H destruct -H
+  elim (eq_inv_list_empty_rcons ??? e0)
+| <list_append_lcons_sn <list_append_empty_sn #H destruct -H
+  elim (eq_inv_list_empty_rcons ??? (sym_eq … e0))
+| #b2 #l2 <list_append_lcons_sn <list_append_lcons_sn #H destruct -H
+  elim (IH … e0) -IH -e0 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
 qed-.
 
 (* Advanced eliminations ****************************************************)
-- 
2.39.2