From 9b4e20442ec5a4028cfe2b6fe836c94acdb033b8 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 17 May 2022 21:09:39 +0200
Subject: [PATCH] update in delayed_updating

+ generic unwind meeds to be  even more generic
---
 .../delayed_updating/unwind/unwind_gen.ma            |  4 ++--
 .../delayed_updating/unwind/unwind_gen_after.ma      |  3 ++-
 .../delayed_updating/unwind/unwind_gen_eq.ma         | 12 ++++++++----
 .../delayed_updating/unwind/unwind_gen_structure.ma  |  4 ++--
 4 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
index 4c592528e..bff50807d 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
@@ -25,7 +25,7 @@ match p with
   match l with
   [ label_d n ⇒
     match q with
-    [ list_empty     ⇒ 𝗱(f@❨n❩)◗(unwind_gen f q)
+    [ list_empty     ⇒ 𝗱((f n)@❨n❩)◗(unwind_gen f q)
     | list_lcons _ _ ⇒ unwind_gen f q
     ]
   | label_m   ⇒ unwind_gen f q
@@ -46,7 +46,7 @@ lemma unwind_gen_empty (f):
 // qed.
 
 lemma unwind_gen_d_empty (f) (n):
-      𝗱(f@❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
+      𝗱((f n)@❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
 // qed.
 
 lemma unwind_gen_d_lcons (f) (p) (l) (n):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
index 2954be831..9d4955ff9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
@@ -20,6 +20,7 @@ include "ground/relocation/tr_compose_pap.ma".
 (* Properties with tr_compose ***********************************************)
 
 lemma unwind_gen_after (f2) (f1) (p):
-      ◆[f2]◆[f1]p = ◆[f2∘f1]p.
+      ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)@❨n❩))∘(f1 n)]p.
 #f2 #f1 #p @(path_ind_unwind … p) -p //
+#n #_ <unwind_gen_d_empty <unwind_gen_d_empty //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
index 11ddd2d03..34cb91a5a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
@@ -19,11 +19,15 @@ include "ground/relocation/tr_pap_eq.ma".
 
 (* Constructions with stream_eq *********************************************)
 
-lemma unwind_gen_eq_repl (p):
-      stream_eq_repl … (λf1,f2. ◆[f1]p = ◆[f2]p).
-#p @(path_ind_unwind … p) -p // [ #n |*: #p ] #IH #f1 #f2 #Hf
+lemma unwind_gen_eq_repl (p) (f1) (f2):
+      (∀n. f1 n ≗ f2 n) → ◆[f1]p = ◆[f2]p.
+#p @(path_ind_unwind … p) -p // [ #n | #n #l #p |*: #p ] #IH #f1 #f2 #Hf
 [ <unwind_gen_d_empty <unwind_gen_d_empty
-  <(tr_pap_eq_repl … Hf) -f2 -IH //
+  <(tr_pap_eq_repl … (Hf n)) -f2 -IH //
+| <unwind_gen_d_lcons <unwind_gen_d_lcons
+  <(IH … Hf) -f2 -IH //
+| <unwind_gen_m_sn <unwind_gen_m_sn
+  <(IH … Hf) -f2 -IH //
 | <unwind_gen_L_sn <unwind_gen_L_sn
   <(IH … Hf) -f2 -IH //
 | <unwind_gen_A_sn <unwind_gen_A_sn
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
index 2948a913e..7d75fe605 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
@@ -74,7 +74,7 @@ qed-.
 (* Advanced constructions with list_rcons ***********************************)
 
 lemma unwind_gen_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱(f@❨n❩) = ◆[f](p◖𝗱n).
+      (⊗p)◖𝗱((f n)@❨n❩) = ◆[f](p◖𝗱n).
 #n #p #f <unwind_gen_append_proper_dx // 
 qed.
 
@@ -110,7 +110,7 @@ qed-.
 
 lemma unwind_gen_inv_d_sn (k) (q) (p) (f):
       (𝗱k◗q) = ◆[f]p →
-      ∃∃r,h. 𝐞 = ⊗r & f@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+      ∃∃r,h. 𝐞 = ⊗r & (f h)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
 #k #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_gen_empty #H destruct
-- 
2.39.2