From 9e31ac1f3f868349154b0ce2e550e2476aaf6a30 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 11 Sep 2022 23:13:53 +0200
Subject: [PATCH] update in delayed_updating

+ reference by depth with offset parked for now
---
 .../delayed_updating/etc/d2/d2.etc            | 77 +++++++++++++++++++
 .../d2/nodelabel_d_2.etc}                     |  0
 .../functions/tau_3.ma => etc/d2/tau_3.etc}   |  0
 .../delayed_updating/syntax/label.ma          | 18 ++---
 .../delayed_updating/syntax/path_depth.ma     | 22 ++----
 .../delayed_updating/syntax/path_inner.ma     |  6 --
 .../delayed_updating/syntax/path_structure.ma | 69 ++++-------------
 .../syntax/path_structure_inner.ma            |  3 +-
 .../syntax/prototerm_constructors.ma          | 16 ----
 .../syntax/prototerm_proper_constructors.ma   |  5 --
 10 files changed, 103 insertions(+), 113 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/d2.etc
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/nodelabel_d_2.ma => etc/d2/nodelabel_d_2.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/tau_3.ma => etc/d2/tau_3.etc} (100%)

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/d2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/d2.etc
new file mode 100644
index 000000000..32a628e3f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/d2.etc
@@ -0,0 +1,77 @@
+include "delayed_updating/notation/functions/nodelabel_d_2.ma".
+
+| label_d2: pnat → nat → label
+
+interpretation
+  "variable reference by depth with offset (label)"
+  'NodeLabelD k d = (label_d2 k d).
+
+  | label_d2 k d ⇒ depth q
+
+lemma depth_d2_dx (p) (k) (d):
+      ♭p = ♭(p◖𝗱❨k,d❩).
+// qed.
+
+lemma depth_d2_sn (p) (k) (d):
+      ♭p = ♭(𝗱❨k,d❩◗p).
+// qed.
+
+   | label_d2 k d ⇒ structure q
+
+lemma structure_d2_dx (p) (k) (d):
+      ⊗p = ⊗(p◖𝗱❨k,d❩).
+// qed.
+
+lemma structure_d2_sn (p) (k) (d):
+      ⊗p = ⊗(𝗱❨k,d❩◗p).
+#p #k #d <structure_append //
+qed.
+
+lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
+      q◖𝗱❨h,d❩ = ⊗p → ⊥.
+#d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_dx #H0 /2 width=1 by/
+| <structure_d2_dx #H0 /2 width=1 by/
+| <structure_m_dx #H0 /2 width=1 by/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_d2_sn_structure (d) (h) (q) (p):
+      (𝗱❨h,d❩◗q) = ⊗p → ⊥.
+#d #h #q #p >list_cons_comm #H0
+elim (eq_inv_append_structure … H0) -H0 #r1 #r2
+<list_cons_comm #H0 #H1 #H2 destruct
+elim (eq_inv_d2_dx_structure … H0)
+qed-.
+
+include "delayed_updating/notation/functions/tau_3.ma".
+
+interpretation
+  "inner variable reference by depth with offset (prototerm)"
+  'Tau k d t = (prototerm_node_1_2 (label_d2 k d) label_m t).
+
+lemma in_comp_iref2 (t) (q) (k) (d):
+      q ϵ t → 𝗱❨k,d❩◗𝗺◗q ϵ 𝛕❨k,d❩.t.
+/2 width=3 by ex2_intro/ qed.
+
+lemma in_comp_inv_iref2 (t) (p) (k) (d):
+      p ϵ 𝛕❨k,d❩.t →
+      ∃∃q. 𝗱❨k,d❩◗𝗺◗q = p & q ϵ t.
+#t #p #k #d * #q #Hq #Hp
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma ppc_iref2 (t) (k) (d):
+      (𝛕❨k,d❩.t) ϵ 𝐏.
+#t #k #d #p * #q #Hq #H0 destruct //
+qed.
+
+lemma pic_inv_d2_dx (p) (k) (d):
+      p◖𝗱❨k,d❩ ϵ 𝐈 → ⊥.
+#p #k #d @(insert_eq_1 … (p◖𝗱❨k,d❩))
+#q * -q [|*: #q ] #H0 destruct
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/nodelabel_d_2.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_2.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/nodelabel_d_2.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/tau_3.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/tau_3.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
index 7106e0b0b..6a607559c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -16,9 +16,8 @@
  * Initial invocation: - Patience on me to gain peace and perfection! -
  *)
 
-include "ground/arith/nat.ma".
+include "ground/arith/pnat.ma".
 include "delayed_updating/notation/functions/nodelabel_d_1.ma".
-include "delayed_updating/notation/functions/nodelabel_d_2.ma".
 include "delayed_updating/notation/functions/nodelabel_m_0.ma".
 include "delayed_updating/notation/functions/edgelabel_l_0.ma".
 include "delayed_updating/notation/functions/edgelabel_a_0.ma".
@@ -27,22 +26,17 @@ include "delayed_updating/notation/functions/edgelabel_s_0.ma".
 (* LABEL ********************************************************************)
 
 inductive label: Type[0] ≝
-| label_d : pnat → label
-| label_d2: pnat → nat → label
-| label_m : label
-| label_L : label
-| label_A : label
-| label_S : label
+| label_d: pnat → label
+| label_m: label
+| label_L: label
+| label_A: label
+| label_S: label
 .
 
 interpretation
   "variable reference by depth (label)"
   'NodeLabelD k = (label_d k).
 
-interpretation
-  "variable reference by depth with offset (label)"
-  'NodeLabelD k d = (label_d2 k d).
-
 interpretation
   "mark (label)"
   'NodeLabelM = (label_m).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index 2e638b8ac..a769327f6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -23,12 +23,11 @@ match p with
 [ list_empty     ⇒ 𝟎
 | list_lcons l q ⇒
   match l with
-  [ label_d k    ⇒ depth q
-  | label_d2 k d ⇒ depth q
-  | label_m      ⇒ depth q
-  | label_L      ⇒ ↑(depth q)
-  | label_A      ⇒ depth q
-  | label_S      ⇒ depth q
+  [ label_d k ⇒ depth q
+  | label_m   ⇒ depth q
+  | label_L   ⇒ ↑(depth q)
+  | label_A   ⇒ depth q
+  | label_S   ⇒ depth q
   ]
 ].
 
@@ -45,10 +44,6 @@ lemma depth_d_dx (p) (k):
       ♭p = ♭(p◖𝗱k).
 // qed.
 
-lemma depth_d2_dx (p) (k) (d):
-      ♭p = ♭(p◖𝗱❨k,d❩).
-// qed.
-
 lemma depth_m_dx (p):
       ♭p = ♭(p◖𝗺).
 // qed.
@@ -70,9 +65,8 @@ lemma depth_S_dx (p):
 theorem depth_append (p) (q):
         (♭p)+(♭q) = ♭(p●q).
 #p #q elim q -q //
-* [ #k | #k #d ] #q #IH <list_append_lcons_sn
+* [ #k ] #q #IH <list_append_lcons_sn
 [ <depth_d_dx <depth_d_dx //
-| <depth_d2_dx <depth_d2_dx //
 | <depth_m_dx <depth_m_dx //
 | <depth_L_dx <depth_L_dx //
 | <depth_A_dx <depth_A_dx //
@@ -86,10 +80,6 @@ lemma depth_d_sn (p) (k):
       ♭p = ♭(𝗱k◗p).
 // qed.
 
-lemma depth_d2_sn (p) (k) (d):
-      ♭p = ♭(𝗱❨k,d❩◗p).
-// qed.
-
 lemma depth_m_sn (p):
       ♭p = ♭(𝗺◗p).
 // 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
index 25678301b..b2b0cb03f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -39,12 +39,6 @@ lemma pic_inv_d_dx (p) (k):
 #q * -q [|*: #q ] #H0 destruct
 qed-.
 
-lemma pic_inv_d2_dx (p) (k) (d):
-      p◖𝗱❨k,d❩ ϵ 𝐈 → ⊥.
-#p #k #d @(insert_eq_1 … (p◖𝗱❨k,d❩))
-#q * -q [|*: #q ] #H0 destruct
-qed-.
-
 (* Constructions with path_lcons ********************************************)
 
 lemma pic_m_sn (p):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index 95c728682..288575c4e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -23,12 +23,11 @@ match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
-   [ label_d k    ⇒ structure q
-   | label_d2 k d ⇒ structure q
-   | label_m      ⇒ structure q
-   | label_L      ⇒ (structure q)◖𝗟
-   | label_A      ⇒ (structure q)◖𝗔
-   | label_S      ⇒ (structure q)◖𝗦
+   [ label_d k ⇒ structure q
+   | label_m   ⇒ structure q
+   | label_L   ⇒ (structure q)◖𝗟
+   | label_A   ⇒ (structure q)◖𝗔
+   | label_S   ⇒ (structure q)◖𝗦
    ]
 ].
 
@@ -46,10 +45,6 @@ lemma structure_d_dx (p) (k):
       ⊗p = ⊗(p◖𝗱k).
 // qed.
 
-lemma structure_d2_dx (p) (k) (d):
-      ⊗p = ⊗(p◖𝗱❨k,d❩).
-// qed.
-
 lemma structure_m_dx (p):
       ⊗p = ⊗(p◖𝗺).
 // qed.
@@ -71,13 +66,13 @@ lemma structure_S_dx (p):
 theorem structure_idem (p):
         ⊗p = ⊗⊗p.
 #p elim p -p //
-* [ #k | #k #d ] #p #IH //
+* [ #k ] #p #IH //
 qed.
 
 theorem structure_append (p) (q):
         ⊗p●⊗q = ⊗(p●q).
 #p #q elim q -q //
-* [ #k | #k #d ] #q #IH //
+* [ #k ] #q #IH //
 <list_append_lcons_sn //
 qed.
 
@@ -88,11 +83,6 @@ lemma structure_d_sn (p) (k):
 #p #k <structure_append //
 qed.
 
-lemma structure_d2_sn (p) (k) (d):
-      ⊗p = ⊗(𝗱❨k,d❩◗p).
-#p #k #d <structure_append //
-qed.
-
 lemma structure_m_sn (p):
       ⊗p = ⊗(𝗺◗p).
 #p <structure_append //
@@ -117,23 +107,9 @@ qed.
 
 lemma eq_inv_d_dx_structure (h) (q) (p):
       q◖𝗱h = ⊗p → ⊥.
-#h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#h #q #p elim p -p [| * [ #k ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0 /2 width=1 by/
-| <structure_d2_dx #H0 /2 width=1 by/
-| <structure_m_dx #H0 /2 width=1 by/
-| <structure_L_dx #H0 destruct
-| <structure_A_dx #H0 destruct
-| <structure_S_dx #H0 destruct
-]
-qed-.
-
-lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
-      q◖𝗱❨h,d❩ = ⊗p → ⊥.
-#d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
-[ <structure_empty #H0 destruct
-| <structure_d_dx #H0 /2 width=1 by/
-| <structure_d2_dx #H0 /2 width=1 by/
 | <structure_m_dx #H0 /2 width=1 by/
 | <structure_L_dx #H0 destruct
 | <structure_A_dx #H0 destruct
@@ -143,10 +119,9 @@ qed-.
 
 lemma eq_inv_m_dx_structure (q) (p):
       q◖𝗺 = ⊗p → ⊥.
-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0 /2 width=1 by/
-| <structure_d2_dx #H0 /2 width=1 by/
 | <structure_m_dx #H0 /2 width=1 by/
 | <structure_L_dx #H0 destruct
 | <structure_A_dx #H0 destruct
@@ -157,14 +132,11 @@ qed-.
 lemma eq_inv_L_dx_structure (q) (p):
       q◖𝗟 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.
-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
-| <structure_d2_dx #H0
-  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
-  /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
@@ -178,14 +150,11 @@ qed-.
 lemma eq_inv_A_dx_structure (q) (p):
       q◖𝗔 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗔◗r2 = p.
-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
-| <structure_d2_dx #H0
-  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
-  /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
@@ -199,14 +168,11 @@ qed-.
 lemma eq_inv_S_dx_structure (q) (p):
       q◖𝗦 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗦◗r2 = p.
-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
-| <structure_d2_dx #H0
-  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
-  /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
@@ -222,11 +188,10 @@ qed-.
 theorem eq_inv_append_structure (p) (q) (r):
         p●q = ⊗r →
         ∃∃r1,r2.p = ⊗r1 & q = ⊗r2 & r1●r2 = r.
-#p #q elim q -q [| * [ #k | #k #d ] #q #IH ] #r
+#p #q elim q -q [| * [ #k ] #q #IH ] #r
 [ <list_append_empty_sn #H0 destruct
   /2 width=5 by ex3_2_intro/
 | #H0 elim (eq_inv_d_dx_structure … H0)
-| #H0 elim (eq_inv_d2_dx_structure … H0)
 | #H0 elim (eq_inv_m_dx_structure … H0)
 | #H0 elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@@ -253,14 +218,6 @@ elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 elim (eq_inv_d_dx_structure … H0)
 qed-.
 
-lemma eq_inv_d2_sn_structure (d) (h) (q) (p):
-      (𝗱❨h,d❩◗q) = ⊗p → ⊥.
-#d #h #q #p >list_cons_comm #H0
-elim (eq_inv_append_structure … H0) -H0 #r1 #r2
-<list_cons_comm #H0 #H1 #H2 destruct
-elim (eq_inv_d2_dx_structure … H0)
-qed-.
-
 lemma eq_inv_m_sn_structure (q) (p):
       (𝗺 ◗q) = ⊗p → ⊥.
 #q #p >list_cons_comm #H0
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
index 4de1097bb..99ed6a323 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
@@ -23,9 +23,8 @@ lemma structure_pic (p):
       ⊗p ϵ 𝐈.
 #p elim p -p
 [ <structure_empty //
-| * [ #k | #k #d ] #p #IH
+| * [ #k ] #p #IH
   [ <structure_d_dx //
-  | <structure_d2_dx //
   | <structure_m_dx //
   | <structure_L_dx //
   | <structure_A_dx //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
index 8bffdb64a..5bb66e16a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
@@ -16,7 +16,6 @@ include "delayed_updating/syntax/prototerm.ma".
 include "delayed_updating/notation/functions/m_hook_1.ma".
 include "delayed_updating/notation/functions/hash_1.ma".
 include "delayed_updating/notation/functions/tau_2.ma".
-include "delayed_updating/notation/functions/tau_3.ma".
 include "delayed_updating/notation/functions/lamda_1.ma".
 include "delayed_updating/notation/functions/at_2.ma".
 
@@ -48,10 +47,6 @@ interpretation
   "inner variable reference by depth (prototerm)"
   'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
 
-interpretation
-  "inner variable reference by depth with offset (prototerm)"
-  'Tau k d t = (prototerm_node_1_2 (label_d2 k d) label_m t).
-
 interpretation
   "name-free functional abstraction (prototerm)"
   'Lamda t = (prototerm_node_1 label_L t).
@@ -66,10 +61,6 @@ lemma in_comp_iref (t) (q) (k):
       q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
 /2 width=3 by ex2_intro/ qed.
 
-lemma in_comp_iref2 (t) (q) (k) (d):
-      q ϵ t → 𝗱❨k,d❩◗𝗺◗q ϵ 𝛕❨k,d❩.t.
-/2 width=3 by ex2_intro/ qed.
-
 (* Basic inversions *********************************************************)
 
 lemma in_comp_inv_iref (t) (p) (k):
@@ -79,13 +70,6 @@ lemma in_comp_inv_iref (t) (p) (k):
 /2 width=3 by ex2_intro/
 qed-.
 
-lemma in_comp_inv_iref2 (t) (p) (k) (d):
-      p ϵ 𝛕❨k,d❩.t →
-      ∃∃q. 𝗱❨k,d❩◗𝗺◗q = p & q ϵ t.
-#t #p #k #d * #q #Hq #Hp
-/2 width=3 by ex2_intro/
-qed-.
-
 (* COMMENT
 lemma prototerm_in_root_inv_lcons_oref:
       ∀p,l,n. l◗p ϵ ▵#n →
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
index c5a27617a..f7f921bcf 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
@@ -23,8 +23,3 @@ lemma ppc_iref (t) (k):
       (𝛕k.t) ϵ 𝐏.
 #t #k #p * #q #Hq #H0 destruct //
 qed.
-
-lemma ppc_iref2 (t) (k) (d):
-      (𝛕❨k,d❩.t) ϵ 𝐏.
-#t #k #d #p * #q #Hq #H0 destruct //
-qed.
-- 
2.39.2