update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_structure.ma

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 8c60eea7595c8a88c43250865500b11010701dee..288575c4e7680630668be3a61108478261a6d0c4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -14,6 +14,7 @@
 
 include "delayed_updating/syntax/path.ma".
 include "delayed_updating/notation/functions/circled_times_1.ma".
+include "ground/xoa/ex_3_2.ma".
 
 (* STRUCTURE FOR PATH *******************************************************)
 
@@ -22,10 +23,11 @@ match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
-   [ label_node_d n ⇒ structure q
-   | label_edge_L   ⇒ 𝗟◗structure q
-   | label_edge_A   ⇒ 𝗔◗structure q
-   | label_edge_S   ⇒ 𝗦◗structure q
+   [ label_d k ⇒ structure q
+   | label_m   ⇒ structure q
+   | label_L   ⇒ (structure q)◖𝗟
+   | label_A   ⇒ (structure q)◖𝗔
+   | label_S   ⇒ (structure q)◖𝗦
    ]
 ].
 
@@ -39,53 +41,220 @@ lemma structure_empty:
       𝐞 = ⊗𝐞.
 // qed.
 
-lemma structure_d_sn (p) (n):
-      ⊗p = ⊗(𝗱n◗p).
+lemma structure_d_dx (p) (k):
+      ⊗p = ⊗(p◖𝗱k).
 // qed.
 
-lemma structure_L_sn (p):
-      𝗟◗⊗p = ⊗(𝗟◗p).
+lemma structure_m_dx (p):
+      ⊗p = ⊗(p◖𝗺).
 // qed.
 
-lemma structure_A_sn (p):
-      𝗔◗⊗p = ⊗(𝗔◗p).
+lemma structure_L_dx (p):
+      (⊗p)◖𝗟 = ⊗(p◖𝗟).
 // qed.
 
-lemma structure_S_sn (p):
-      𝗦◗⊗p = ⊗(𝗦◗p).
+lemma structure_A_dx (p):
+      (⊗p)◖𝗔 = ⊗(p◖𝗔).
+// qed.
+
+lemma structure_S_dx (p):
+      (⊗p)◖𝗦 = ⊗(p◖𝗦).
 // qed.
 
 (* Main constructions *******************************************************)
 
 theorem structure_idem (p):
         ⊗p = ⊗⊗p.
-#p elim p -p [| * [ #n ] #p #IH ] //
+#p elim p -p //
+* [ #k ] #p #IH //
 qed.
 
-theorem structure_append (p1) (p2):
-        ⊗p1●⊗p2 = ⊗(p1●p2).
-#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
-[||*: <list_append_lcons_sn ] //
+theorem structure_append (p) (q):
+        ⊗p●⊗q = ⊗(p●q).
+#p #q elim q -q //
+* [ #k ] #q #IH //
+<list_append_lcons_sn //
 qed.
 
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
 
-lemma structure_d_dx (p) (n):
-      ⊗p = ⊗(p◖𝗱n).
-#p #n <structure_append //
+lemma structure_d_sn (p) (k):
+      ⊗p = ⊗(𝗱k◗p).
+#p #k <structure_append //
 qed.
 
-lemma structure_L_dx (p):
-      (⊗p)◖𝗟 = ⊗(p◖𝗟).
+lemma structure_m_sn (p):
+      ⊗p = ⊗(𝗺◗p).
 #p <structure_append //
 qed.
 
-lemma structure_A_dx (p):
-      (⊗p)◖𝗔 = ⊗(p◖𝗔).
+lemma structure_L_sn (p):
+      (𝗟◗⊗p) = ⊗(𝗟◗p).
 #p <structure_append //
 qed.
 
-lemma structure_S_dx (p):
-      (⊗p)◖𝗦 = ⊗(p◖𝗦).
+lemma structure_A_sn (p):
+      (𝗔◗⊗p) = ⊗(𝗔◗p).
 #p <structure_append //
 qed.
+
+lemma structure_S_sn (p):
+      (𝗦◗⊗p) = ⊗(𝗦◗p).
+#p <structure_append //
+qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_d_dx_structure (h) (q) (p):
+      q◖𝗱h = ⊗p → ⊥.
+#h #q #p elim p -p [| * [ #k ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_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_m_dx_structure (q) (p):
+      q◖𝗺 = ⊗p → ⊥.
+#q #p elim p -p [| * [ #k ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_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_L_dx_structure (q) (p):
+      q◖𝗟 = ⊗p →
+      ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.
+#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_m_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_L_dx #H0 destruct -IH
+  /2 width=5 by ex3_2_intro/
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct
+]
+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 ] #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_m_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct -IH
+  /2 width=5 by ex3_2_intro/
+| <structure_S_dx #H0 destruct
+]
+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 ] #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_m_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct -IH
+  /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Main inversions **********************************************************)
+
+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 ] #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_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
+  @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
+  <structure_append <structure_L_sn <Hr2 -Hr2 //
+| #H0 elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
+  <structure_append <structure_A_sn <Hr2 -Hr2 //
+| #H0 elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
+  <structure_append <structure_S_sn <Hr2 -Hr2 //
+]
+qed-.
+
+(* Inversions with path_lcons ***********************************************)
+
+lemma eq_inv_d_sn_structure (h) (q) (p):
+      (𝗱h◗q) = ⊗p → ⊥.
+#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_d_dx_structure … H0)
+qed-.
+
+lemma eq_inv_m_sn_structure (q) (p):
+      (𝗺 ◗q) = ⊗p → ⊥.
+#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_m_dx_structure … H0)
+qed-.
+
+lemma eq_inv_L_sn_structure (q) (p):
+      (𝗟◗q) = ⊗p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗟◗r2 = p.
+#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_L_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
+@(ex3_2_intro … s1 (s2●r2)) // -s1
+<structure_append <H2 -s2 //
+qed-.
+
+lemma eq_inv_A_sn_structure (q) (p):
+      (𝗔◗q) = ⊗p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗔◗r2 = p.
+#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_A_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
+@(ex3_2_intro … s1 (s2●r2)) // -s1
+<structure_append <H2 -s2 //
+qed-.
+
+lemma eq_inv_S_sn_structure (q) (p):
+      (𝗦◗q) = ⊗p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗦◗r2 = p.
+#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_S_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
+@(ex3_2_intro … s1 (s2●r2)) // -s1
+<structure_append <H2 -s2 //
+qed-.