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 *******************************************************)
[ list_empty β π
| list_lcons l q β
match l with
- [ label_d n β structure q
+ [ label_d k β structure q
| label_m β structure q
- | label_L β πβstructure q
- | label_A β πβstructure q
- | label_S β π¦βstructure q
+ | label_L β (structure q)βπ
+ | label_A β (structure q)βπ
+ | label_S β (structure q)βπ¦
]
].
π = βπ.
// qed.
-lemma structure_d_sn (p) (n):
- βp = β(π±nβp).
+lemma structure_d_dx (p) (k):
+ βp = β(pβπ±k).
// qed.
-lemma structure_m_sn (p):
- βp = β(πΊβp).
+lemma structure_m_dx (p):
+ βp = β(pβπΊ).
// qed.
-lemma structure_L_sn (p):
- (πββp) = β(πβp).
+lemma structure_L_dx (p):
+ (βp)βπ = β(pβπ).
// qed.
-lemma structure_A_sn (p):
- (πββp) = β(πβp).
+lemma structure_A_dx (p):
+ (βp)βπ = β(pβπ).
// qed.
-lemma structure_S_sn (p):
- (π¦ββp) = β(π¦βp).
+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_m_dx (p):
- βp = β(pβπΊ).
+lemma structure_m_sn (p):
+ βp = β(πΊβp).
#p <structure_append //
qed.
-lemma structure_L_dx (p):
- (βp)βπ = β(pβπ).
+lemma structure_L_sn (p):
+ (πββp) = β(πβp).
#p <structure_append //
qed.
-lemma structure_A_dx (p):
- (βp)βπ = β(pβπ).
+lemma structure_A_sn (p):
+ (πββp) = β(πβp).
#p <structure_append //
qed.
-lemma structure_S_dx (p):
- (βp)βπ¦ = β(pβπ¦).
+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-.