From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 28 Apr 2022 15:34:11 +0000 (+0200)
Subject: update in delayed_updating
X-Git-Tag: make_still_working~76^2~1
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d08b01eee540a6e955cb12cb7421da4198a4ef48;p=helm.git

update in delayed_updating

+ alternative definition of unwind based on lift
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index 5865fe6ad..e6e1e661e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -111,6 +111,14 @@ lemma lift_rmap_S_sn (f) (p):
       ↑[p]f = ↑[𝗦◗p]f.
 // qed.
 
+(* Advanced cinstructionswith proj_rmap and tr_id ***************************)
+
+lemma lift_rmap_id (p):
+      (𝐢) = ↑[p]𝐢.
+#p elim p -p //
+* [ #n ] #p #IH //
+qed.
+
 (* Advanced constructions with proj_rmap and path_append ********************)
 
 lemma lift_rmap_append (p2) (p1) (f):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path.ma
new file mode 100644
index 000000000..b23db01af
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path.ma
@@ -0,0 +1,108 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_length.ma".
+include "delayed_updating/notation/functions/black_downtriangle_1.ma".
+include "ground/relocation/tr_uni.ma".
+
+(* BASIC UNWIND FOR PATH ****************************************************)
+
+rec definition unwind1_path_pnat (n) (p) on n ≝
+match n with
+[ punit   ⇒ p
+| psucc m ⇒
+  match p with
+  [ list_empty     ⇒ 𝐞
+  | list_lcons l q ⇒
+    match l with
+    [ label_d n ⇒
+      match q with
+      [ list_empty     ⇒ l◗(unwind1_path_pnat m q)
+      | list_lcons _ _ ⇒ unwind1_path_pnat m (↑[𝐮❨n❩]q)
+      ]
+    | label_m   ⇒ unwind1_path_pnat m q
+    | label_L   ⇒ 𝗟◗(unwind1_path_pnat m q)
+    | label_A   ⇒ 𝗔◗(unwind1_path_pnat m q)
+    | label_S   ⇒ 𝗦◗(unwind1_path_pnat m q)
+    ]
+  ]
+].
+
+definition unwind1_path (p) ≝
+           unwind1_path_pnat (↑❘p❘) p.
+
+interpretation
+  "basic unwind (path)"
+  'BlackDownTriangle p = (unwind1_path p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind1_path_unfold (p):
+      unwind1_path_pnat (↑❘p❘) p = ▼p.
+// qed-.
+
+lemma unwind1_path_empty:
+      (𝐞) = ▼𝐞.
+// qed.
+
+lemma unwind1_path_d_empty (n):
+      (𝗱n◗𝐞) = ▼(𝗱n◗𝐞).
+// qed.
+
+lemma unwind1_path_d_lcons (p) (l) (n:pnat):
+      ▼(↑[𝐮❨n❩](l◗p)) = ▼(𝗱n◗l◗p).
+#p #l #n
+<unwind1_path_unfold <lift_path_length //
+qed.
+
+lemma unwind1_path_m_sn (p):
+      ▼p = ▼(𝗺◗p).
+// qed.
+
+lemma unwind1_path_L_sn (p):
+      (𝗟◗▼p) = ▼(𝗟◗p).
+// qed.
+
+lemma unwind1_path_A_sn (p):
+      (𝗔◗▼p) = ▼(𝗔◗p).
+// qed.
+
+lemma unwind1_path_S_sn (p):
+      (𝗦◗▼p) = ▼(𝗦◗p).
+// qed.
+
+(* Main constructions *******************************************************)
+
+fact unwind1_path_fix_aux (k) (p):
+     k = ❘p❘ → ▼p = ▼▼p.
+#k @(nat_ind_succ … k) -k
+[ #p #H0 >(list_length_inv_zero_sn … H0) -p //
+| #k #IH *
+  [ #H0 elim (eq_inv_nsucc_zero … H0)
+  | * [ #n ] #p #H0
+    lapply (eq_inv_nsucc_bi … H0) -H0
+    [ cases p -p [ -IH | #l #p ] #H0 destruct //
+      <unwind1_path_d_lcons <IH -IH //
+    | #H0 destruct <unwind1_path_m_sn <IH -IH //
+    | #H0 destruct <unwind1_path_L_sn <unwind1_path_L_sn <IH -IH //
+    | #H0 destruct <unwind1_path_A_sn <unwind1_path_A_sn <IH -IH //
+    | #H0 destruct <unwind1_path_S_sn <unwind1_path_S_sn <IH -IH //
+    ]
+  ]
+]
+qed-.
+
+theorem unwind1_path_fix (p):
+        ▼p = ▼▼p.
+/2 width=2 by unwind1_path_fix_aux/ qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path_structure.ma
new file mode 100644
index 000000000..3a838ebe8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path_structure.ma
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind0/unwind1_rmap_eq.ma".
+include "delayed_updating/unwind0/unwind1_path.ma".
+include "delayed_updating/substitution/lift_structure.ma".
+
+(* BASIC UNWIND FOR PATH ****************************************************)
+
+(* Constructions with structure *********************************************)
+
+fact unwind1_path_d_dx_aux (k) (p) (n):
+     k = ❘p❘ → (⊗p)◖𝗱((▶p)@❨n❩) = ▼(p◖𝗱n).
+#k @(nat_ind_succ … k) -k
+[ #p #n #H0 >(list_length_inv_zero_sn … H0) -p //
+| #k #IH *
+  [ #n #H0 elim (eq_inv_nsucc_zero … H0)
+  | * [ #m ] #p #n #H0
+    lapply (eq_inv_nsucc_bi … H0) -H0
+    [ cases p -p [ -IH | #l #p ] #H0 destruct <unwind1_path_d_lcons
+      [ <lift_path_d_sn <lift_path_empty <unwind1_path_d_empty
+        <list_cons_comm <(tr_pap_eq_repl … (unwind1_rmap_d_empty …)) //
+      | >list_cons_shift <lift_path_d_dx <IH -IH //
+        <structure_lift <structure_d_sn /3 width=1 by eq_f2/
+      ]
+    | #H0 destruct <unwind1_path_m_sn <IH -IH //
+    | #H0 destruct <unwind1_path_L_sn <IH -IH //
+    | #H0 destruct <unwind1_path_A_sn <IH -IH //
+    | #H0 destruct <unwind1_path_S_sn <IH -IH //
+    ]
+  ]
+]
+qed-.
+
+lemma unwind1_path_d_dx (p) (n):
+      (⊗p)◖𝗱((▶p)@❨n❩) = ▼(p◖𝗱n).
+/2 width=2 by unwind1_path_d_dx_aux/ qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap.ma
new file mode 100644
index 000000000..66a77d170
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap.ma
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_length.ma".
+include "delayed_updating/notation/functions/black_righttriangle_1.ma".
+include "ground/relocation/tr_uni.ma".
+include "ground/relocation/tr_compose.ma".
+
+(* BASIC UNWIND FOR RELOCATION MAP ******************************************)
+
+rec definition unwind1_rmap_pnat (n) (p) on n ≝
+match n with
+[ punit   ⇒ 𝐢
+| psucc m ⇒
+  match p with
+  [ list_empty     ⇒ 𝐢
+  | list_lcons l q ⇒
+    match l with
+    [ label_d n ⇒ (unwind1_rmap_pnat m (↑[𝐮❨n❩]q))∘(↑[q]𝐮❨n❩)
+    | label_m   ⇒ unwind1_rmap_pnat m q
+    | label_L   ⇒ unwind1_rmap_pnat m q
+    | label_A   ⇒ unwind1_rmap_pnat m q
+    | label_S   ⇒ unwind1_rmap_pnat m q
+    ]
+  ]
+].
+
+definition unwind1_rmap (p) ≝
+           unwind1_rmap_pnat (↑❘p❘) p.
+
+interpretation
+  "basic unwind (relocation map)"
+  'BlackRightTriangle p = (unwind1_rmap p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind1_rmap_unfold (p):
+      unwind1_rmap_pnat (↑❘p❘) p = ▶p.
+// qed-.
+
+lemma unwind1_rmap_empty:
+      (𝐢) = ▶(𝐞).
+// qed.
+
+lemma unwind1_rmap_d_sn (p) (n:pnat):
+      (▶(↑[𝐮❨n❩]p))∘(↑[p]𝐮❨n❩) = ▶(𝗱n◗p).
+#p #n
+<unwind1_rmap_unfold <lift_path_length //
+qed.
+
+lemma unwind1_rmap_m_sn (p):
+      ▶p = ▶(𝗺◗p).
+// qed.
+
+lemma unwind1_rmap_L_sn (p):
+      ▶p = ▶(𝗟◗p).
+// qed.
+
+lemma unwind1_rmap_A_sn (p):
+      ▶p = ▶(𝗔◗p).
+// qed.
+
+lemma unwind1_rmap_S_sn (p):
+      ▶p = ▶(𝗦◗p).
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap_eq.ma
new file mode 100644
index 000000000..113e0ccb6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap_eq.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind0/unwind1_rmap.ma".
+include "ground/relocation/tr_id_compose.ma".
+
+(* BASIC UNWIND FOR RELOCATION MAP ******************************************)
+
+(* Constructions with stream_eq *********************************************)
+
+lemma unwind1_rmap_d_empty (n:pnat):
+      (𝐮❨n❩) ≗ ▶(𝗱n◗𝐞).
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path.ma
new file mode 100644
index 000000000..859c1b8e1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path.ma
@@ -0,0 +1,109 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind0/unwind1_path.ma".
+include "delayed_updating/notation/functions/black_downtriangle_2.ma".
+
+(* EXTENDED UNWIND FOR PATH *************************************************)
+
+definition unwind2_path (f) (p) ≝
+           ▼↑[f]p.
+
+interpretation
+  "extended unwind (path)"
+  'BlackDownTriangle f p = (unwind2_path f p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind2_path_unfold (f) (p):
+      ▼↑[f]p = ▼[f]p.
+// qed.
+
+lemma unwind2_path_id (p):
+      ▼p = ▼[𝐢]p.
+// qed.
+
+lemma unwind2_path_empty (f):
+      (𝐞) = ▼[f]𝐞.
+// qed.
+
+lemma unwind2_path_d_empty (f) (n):
+      (𝗱(f@❨n❩)◗𝐞) = ▼[f](𝗱n◗𝐞).
+// qed.
+
+lemma unwind2_path_d_lcons (f) (p) (l) (n:pnat):
+      ▼[𝐮❨f@❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
+#f #p #l #n
+<unwind2_path_unfold in ⊢ (???%);
+<lift_path_d_sn <lift_path_id <unwind1_path_d_lcons //
+qed.
+
+lemma unwind2_path_m_sn (f) (p):
+      ▼[f]p = ▼[f](𝗺◗p).
+#f #p
+<unwind2_path_unfold in ⊢ (???%);
+<lift_path_m_sn //
+qed.
+
+lemma unwind2_path_L_sn (f) (p):
+      (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
+#f #p
+<unwind2_path_unfold in ⊢ (???%);
+<lift_path_L_sn //
+qed.
+
+lemma unwind2_path_A_sn (f) (p):
+      (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
+#f #p
+<unwind2_path_unfold in ⊢ (???%);
+<lift_path_A_sn //
+qed.
+
+lemma unwind2_path_S_sn (f) (p):
+      (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
+#f #p
+<unwind2_path_unfold in ⊢ (???%);
+<lift_path_S_sn //
+qed.
+
+(* Main constructions *******************************************************)
+
+theorem unwind2_path_after_id_sn (p) (f):
+        ▼[f]p = ▼▼[f]p.
+// qed.
+
+(* Constructions with stream_eq *********************************************)
+
+lemma unwind2_path_eq_repl (p):
+      stream_eq_repl … (λf1,f2. ▼[f1]p = ▼[f2]p).
+#p #f1 #f2 #Hf
+<unwind2_path_unfold <unwind2_path_unfold
+<(lift_path_eq_repl … Hf) -Hf //
+qed.
+
+(* Advanced eliminations with path ******************************************)
+
+lemma path_ind_unwind2 (Q:predicate …):
+      Q (𝐞) →
+      (∀n. Q (𝐞) → Q (𝗱n◗𝐞)) →
+      (∀n,l,p. Q (l◗p) → Q (𝗱n◗l◗p)) →
+      (∀p. Q p → Q (𝗺◗p)) →
+      (∀p. Q p → Q (𝗟◗p)) →
+      (∀p. Q p → Q (𝗔◗p)) →
+      (∀p. Q p → Q (𝗦◗p)) →
+      ∀p. Q p.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
+elim p -p [| * [ #n * ] ]
+/2 width=1 by/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path_structure.ma
new file mode 100644
index 000000000..3ed240682
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path_structure.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind0/unwind2_rmap.ma".
+include "delayed_updating/unwind0/unwind2_path.ma".
+include "delayed_updating/unwind0/unwind1_path_structure.ma".
+
+(* EXTENDED UNWIND FOR PATH *************************************************)
+
+(* Constructions with structure *********************************************)
+
+lemma unwind2_path_d_dx (f) (p) (n):
+      (⊗p)◖𝗱((▶[f]p)@❨n❩) = ▼[f](p◖𝗱n).
+#f #p #n
+<unwind2_path_unfold <lift_path_d_dx <unwind1_path_d_dx
+<structure_lift >tr_compose_pap //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap.ma
new file mode 100644
index 000000000..9bb26750a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap.ma
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind0/unwind1_rmap.ma".
+include "delayed_updating/notation/functions/black_righttriangle_2.ma".
+
+(* EXTENDED UNWIND FOR RELOCATION MAP ***************************************)
+
+definition unwind2_rmap (f) (p): tr_map ≝
+           (▶↑[f]p)∘(↑[p]f).
+
+interpretation
+  "extended unwind (relocation map)"
+  'BlackRightTriangle f p = (unwind2_rmap f p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind2_rmap_unfold (f) (p):
+      (▶↑[f]p)∘(↑[p]f) = ▶[f]p.
+// qed.
+
+lemma unwind2_rmap_m_sn (f) (p):
+      ▶[f]p = ▶[f](𝗺◗p).
+#f #p
+<unwind2_rmap_unfold in ⊢ (???%);
+<lift_rmap_m_sn <lift_path_m_sn //
+qed.
+
+lemma unwind2_rmap_L_sn (f) (p):
+      ▶[⫯f]p = ▶[f](𝗟◗p).
+#f #p
+<unwind2_rmap_unfold in ⊢ (???%);
+<lift_rmap_L_sn <lift_path_L_sn //
+qed.
+
+lemma unwind2_rmap_A_sn (f) (p):
+      ▶[f]p = ▶[f](𝗔◗p).
+#f #p
+<unwind2_rmap_unfold in ⊢ (???%);
+<lift_rmap_A_sn <lift_path_A_sn //
+qed.
+
+lemma unwind2_rmap_S_sn (f) (p):
+      ▶[f]p = ▶[f](𝗦◗p).
+#f #p
+<unwind2_rmap_unfold in ⊢ (???%);
+<lift_rmap_S_sn <lift_path_S_sn //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap_eq.ma
new file mode 100644
index 000000000..7666c1c7f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap_eq.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind0/unwind2_rmap.ma".
+include "ground/relocation/tr_id_compose.ma".
+
+(* EXTENDED UNWIND FOR RELOCATION MAP ***************************************)
+
+(* Advanced constructions ***************************************************)
+
+lemma unwind2_rmap_id (p):
+      ▶p ≗ ▶[𝐢]p.
+// qed.
+
+lemma unwind2_rmap_empty (f):
+      f ≗ ▶[f]𝐞.
+// qed.
+
+lemma unwind2_rmap_d_sn (f) (p) (n):
+      ▶[𝐮❨f@❨n❩❩]p ≗ ▶[f](𝗱n◗p).
+#f #p #n
+<unwind2_rmap_unfold <unwind2_rmap_unfold
+<lift_rmap_d_sn <lift_rmap_id
+<lift_path_d_sn <lift_path_id <unwind1_rmap_d_sn //
+qed.