X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_path.ma;h=08115e1e43a424da880d2a6f06e5e4586fbd3b17;hb=61bc42e04598a9f5e489c3867af72e700c7fda04;hp=3288fc7348869901e972b030cd150290bc328abb;hpb=5c2d38b46908f662cbb717156b29101ff30f8352;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
index 3288fc734..08115e1e4 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
@@ -12,73 +12,159 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/unwind/unwind_gen.ma".
 include "delayed_updating/unwind/unwind2_rmap.ma".
-include "delayed_updating/syntax/path_reverse.ma".
+include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/notation/functions/black_downtriangle_2.ma".
-include "ground/lib/list_tl.ma".
 
-(* UNWIND FOR PATH **********************************************************)
+(* TAILED UNWIND FOR PATH ***************************************************)
 
 definition unwind2_path (f) (p): path ≝
-           ◆[▶[f]⇂(pᴿ)]p
-.
+match p with
+[ list_empty     ⇒ (𝐞)
+| list_lcons l q ⇒
+  match l with
+  [ label_d k ⇒ (⊗q)◖𝗱(▶[f]q＠⧣❨k❩)
+  | label_m   ⇒ ⊗p
+  | label_L   ⇒ ⊗p
+  | label_A   ⇒ ⊗p
+  | label_S   ⇒ ⊗p
+  ]
+].
 
 interpretation
-  "unwind (path)"
+  "tailed unwind (path)"
   'BlackDownTriangle f p = (unwind2_path f p).
 
 (* Basic constructions ******************************************************)
 
-lemma unwind2_path_unfold (f) (p):
-      ◆[▶[f]⇂(pᴿ)]p = ▼[f]p.
-// qed.
-
 lemma unwind2_path_empty (f):
       (𝐞) = ▼[f]𝐞.
 // qed.
 
-lemma unwind2_path_d_empty (f) (n):
-      (𝗱(f＠⧣❨n❩)◗𝐞) = ▼[f](𝗱n◗𝐞).
+lemma unwind2_path_d_dx (f) (p) (k) :
+      (⊗p)◖𝗱((▶[f]p)＠⧣❨k❩) = ▼[f](p◖𝗱k).
 // 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 <unwind2_path_unfold
-<unwind_gen_d_lcons <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l0 #_
-<reverse_rcons <reverse_lcons <reverse_lcons <reverse_rcons
-<list_tl_lcons <list_tl_lcons //
-qed.
+lemma unwind2_path_m_dx (f) (p):
+      ⊗p = ▼[f](p◖𝗺).
+// qed.
 
-lemma unwind2_path_m_sn (f) (p):
-      ▼[f]p = ▼[f](𝗺◗p).
-#f #p <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_m_sn <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
-qed.
+lemma unwind2_path_L_dx (f) (p):
+      (⊗p)◖𝗟 = ▼[f](p◖𝗟).
+// qed.
 
-lemma unwind2_path_L_sn (f) (p):
-      (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
-#f #p <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_L_sn <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
-qed.
+lemma unwind2_path_A_dx (f) (p):
+      (⊗p)◖𝗔 = ▼[f](p◖𝗔).
+// qed.
+
+lemma unwind2_path_S_dx (f) (p):
+      (⊗p)◖𝗦 = ▼[f](p◖𝗦).
+// qed.
 
-lemma unwind2_path_A_sn (f) (p):
-      (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
-#f #p <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_A_sn <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
+(* Constructions with structure *********************************************)
+
+lemma structure_unwind2_path (f) (p):
+      ⊗p = ⊗▼[f]p.
+#f * // * [ #k ] #p //
 qed.
 
-lemma unwind2_path_S_sn (f) (p):
-      (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
-#f #p <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_S_sn <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
+lemma unwind2_path_structure (f) (p):
+      ⊗p = ▼[f]⊗p.
+#f #p elim p -p // * [ #k ] #p #IH //
+[ <structure_L_dx <unwind2_path_L_dx //
+| <structure_A_dx <unwind2_path_A_dx //
+| <structure_S_dx <unwind2_path_S_dx //
+]
 qed.
+
+lemma unwind2_path_root (f) (p):
+      ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
+#f * [| * [ #k ] #p ]
+/2 width=3 by ex2_intro/
+<unwind2_path_d_dx <structure_d_dx
+/2 width=3 by ex2_intro/
+qed-.
+
+(* Destructions with structure **********************************************)
+
+lemma unwind2_path_des_structure (f) (q) (p):
+      ⊗q = ▼[f]p → ⊗q = ⊗p.
+// qed-.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_d_dx_unwind2_path (f) (q) (p) (h):
+      q◖𝗱h = ▼[f]p →
+      ∃∃r,k. q = ⊗r & h = ▶[f]r＠⧣❨k❩ & r◖𝗱k = p.
+#f #q * [| * [ #k ] #p ] #h
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_d_dx_structure … H0)
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_m_dx_unwind2_path (f) (q) (p):
+      q◖𝗺 = ▼[f]p → ⊥.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_m_dx_structure … H0)
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_L_dx_unwind2_path (f) (q) (p):
+      q◖𝗟 = ▼[f]p →
+      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗟◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_A_dx_unwind2_path (f) (q) (p):
+      q◖𝗔 = ▼[f]p →
+      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗔◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_S_dx_unwind2_path (f) (q) (p):
+      q◖𝗦 = ▼[f]p →
+      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗦◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+  /2 width=5 by ex3_2_intro/
+]
+qed-.