]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_structure.ma
index 4db66c0648f69ee5e9b1f6082df56c699d65a0f8..2a219e0ffd08d7b7545f97aaecc7767a4b44570b 100644 (file)
@@ -14,9 +14,9 @@
 
 include "delayed_updating/substitution/lift_eq.ma".
 include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_inner.ma".
 include "delayed_updating/syntax/path_proper.ma".
 include "ground/xoa/ex_4_2.ma".
-include "ground/xoa/ex_3_2.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -41,41 +41,64 @@ lemma lift_des_structure (q) (p) (f):
 
 (* Constructions with proper condition for path *****************************)
 
-lemma lift_append_proper_dx (p2) (p1) (f): ź”p2 ā†’
+lemma lift_append_proper_dx (p2) (p1) (f): p2 Ļµ š ā†’
       (āŠ—p1)ā—(ā†‘[ā†‘[p1]f]p2) = ā†‘[f](p1ā—p2).
 #p2 #p1 @(path_ind_lift ā€¦ p1) -p1 //
 [ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
 [ elim (ppc_inv_lcons ā€¦ Hp2) -Hp2 #l #q #H destruct //
 | <lift_path_d_lcons_sn <IH //
+| <lift_path_m_sn <IH //
 | <lift_path_L_sn <IH //
 | <lift_path_A_sn <IH //
 | <lift_path_S_sn <IH //
 ]
 qed-.
 
-(* Advanced constructions with structure ************************************)
+(* Constructions with inner condition for path ******************************)
 
-lemma lift_d_empty_dx (n) (p) (f):
+lemma lift_append_inner_sn (p1) (p2) (f): p1 Ļµ šˆ ā†’
+      (āŠ—p1)ā—(ā†‘[ā†‘[p1]f]p2) = ā†‘[f](p1ā—p2).
+#p1 @(list_ind_rcons ā€¦ p1) -p1 // #p1 *
+[ #n ] #_ #p2 #f #Hp1
+[ elim (pic_inv_d_dx ā€¦ Hp1)
+| <list_append_rcons_sn <lift_append_proper_dx //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_L_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_A_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_S_dx <list_append_rcons_sn //
+]
+qed-.
+
+(* Advanced constructions with proj_path ************************************)
+
+lemma lift_path_d_empty_dx (n) (p) (f):
       (āŠ—p)ā—–š—±((ā†‘[p]f)@āØnā©) = ā†‘[f](pā—–š—±n).
 #n #p #f <lift_append_proper_dx // 
 qed.
 
-lemma lift_L_dx (p) (f):
+lemma lift_path_m_dx (p) (f):
+      āŠ—p = ā†‘[f](pā—–š—ŗ).
+#p #f <lift_append_proper_dx //
+qed.
+
+lemma lift_path_L_dx (p) (f):
       (āŠ—p)ā—–š—Ÿ = ā†‘[f](pā—–š—Ÿ).
 #p #f <lift_append_proper_dx //
 qed.
 
-lemma lift_A_dx (p) (f):
+lemma lift_path_A_dx (p) (f):
       (āŠ—p)ā—–š—” = ā†‘[f](pā—–š—”).
 #p #f <lift_append_proper_dx //
 qed.
 
-lemma lift_S_dx (p) (f):
+lemma lift_path_S_dx (p) (f):
       (āŠ—p)ā—–š—¦ = ā†‘[f](pā—–š—¦).
 #p #f <lift_append_proper_dx //
 qed.
 
-lemma lift_root (f) (p):
+lemma lift_path_root (f) (p):
       āˆƒāˆƒr. šž = āŠ—r & āŠ—pā—r = ā†‘[f]p.
 #f #p @(list_ind_rcons ā€¦ p) -p
 [ /2 width=3 by ex2_intro/
@@ -96,6 +119,23 @@ lemma lift_path_inv_d_sn (k) (q) (p) (f):
 | <lift_path_d_lcons_sn #H
   elim (IH ā€¦ H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
   /2 width=5 by ex4_2_intro/
+| <lift_path_m_sn #H
+  elim (IH ā€¦ H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
+  /2 width=5 by ex4_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_m_sn (q) (p) (f):
+      (š—ŗā——q) = ā†‘[f]p ā†’ āŠ„.
+#q #p @(path_ind_lift ā€¦ p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H /2 width=2 by/
+| <lift_path_m_sn #H /2 width=2 by/
 | <lift_path_L_sn #H destruct
 | <lift_path_A_sn #H destruct
 | <lift_path_S_sn #H destruct
@@ -112,6 +152,9 @@ lemma lift_path_inv_L_sn (q) (p) (f):
 | <lift_path_d_lcons_sn #H
   elim (IH ā€¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+  elim (IH ā€¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
 | <lift_path_L_sn #H destruct -IH
   /2 width=5 by ex3_2_intro/
 | <lift_path_A_sn #H destruct
@@ -129,6 +172,9 @@ lemma lift_path_inv_A_sn (q) (p) (f):
 | <lift_path_d_lcons_sn #H
   elim (IH ā€¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+  elim (IH ā€¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
 | <lift_path_L_sn #H destruct
 | <lift_path_A_sn #H destruct -IH
   /2 width=5 by ex3_2_intro/
@@ -146,7 +192,9 @@ lemma lift_path_inv_S_sn (q) (p) (f):
 | <lift_path_d_lcons_sn #H
   elim (IH ā€¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
-| <lift_path_L_sn #H destruct
+| <lift_path_m_sn #H
+  elim (IH ā€¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/| <lift_path_L_sn #H destruct
 | <lift_path_A_sn #H destruct
 | <lift_path_S_sn #H destruct -IH
   /2 width=5 by ex3_2_intro/
@@ -155,8 +203,8 @@ qed-.
 
 (* Inversions with proper condition for path ********************************)
 
-lemma lift_inv_append_proper_dx (q2) (q1) (p) (f): ź”q2 ā†’
-      q1ā—q2 = ā†‘[f]p ā†’
+lemma lift_inv_append_proper_dx (q2) (q1) (p) (f):
+      q2 Ļµ š ā†’ q1ā—q2 = ā†‘[f]p ā†’
       āˆƒāˆƒp1,p2. āŠ—p1 = q1 & ā†‘[ā†‘[p1]f]p2 = q2 & p1ā—p2 = p.
 #q2 #q1 elim q1 -q1
 [ #p #f #Hq2 <list_append_empty_sn #H destruct
@@ -165,6 +213,7 @@ lemma lift_inv_append_proper_dx (q2) (q1) (p) (f): ź”q2 ā†’
   [ elim (lift_path_inv_d_sn ā€¦ H) -H #r1 #m1 #_ #_ #H0 #_ -IH
     elim (eq_inv_list_empty_append ā€¦ H0) -H0 #_ #H0 destruct
     elim Hq2 -Hq2 //
+  | elim (lift_path_inv_m_sn ā€¦ H)
   | elim (lift_path_inv_L_sn ā€¦ H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
     elim (IH ā€¦ Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
     @(ex3_2_intro ā€¦ (r1ā—š—Ÿā——p1)) //
@@ -180,3 +229,41 @@ lemma lift_inv_append_proper_dx (q2) (q1) (p) (f): ź”q2 ā†’
   ]
 ]
 qed-.
+
+(* Inversions with inner condition for path *********************************)
+
+lemma lift_inv_append_inner_sn (q1) (q2) (p) (f):
+      q1 Ļµ šˆ ā†’ q1ā—q2 = ā†‘[f]p ā†’
+      āˆƒāˆƒp1,p2. āŠ—p1 = q1 & ā†‘[ā†‘[p1]f]p2 = q2 & p1ā—p2 = p.
+#q1 @(list_ind_rcons ā€¦ q1) -q1
+[ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
+  /2 width=5 by ex3_2_intro/
+| #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
+  [ elim (pic_inv_d_dx ā€¦ Hq2)
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx ā€¦ H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_m_sn ā€¦ (sym_eq ā€¦ H2))
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx ā€¦ H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_L_sn ā€¦ (sym_eq ā€¦ H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+    @(ex3_2_intro ā€¦ (p1ā—r2ā—–š—Ÿ)) [1,3: // ]
+    [ <structure_append <structure_L_dx <Hr2 -Hr2 //
+    | <list_append_assoc <list_append_rcons_sn //
+    ]
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx ā€¦ H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_A_sn ā€¦ (sym_eq ā€¦ H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+    @(ex3_2_intro ā€¦ (p1ā—r2ā—–š—”)) [1,3: // ]
+    [ <structure_append <structure_A_dx <Hr2 -Hr2 //
+    | <list_append_assoc <list_append_rcons_sn //
+    ]
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx ā€¦ H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_S_sn ā€¦ (sym_eq ā€¦ H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+    @(ex3_2_intro ā€¦ (p1ā—r2ā—–š—¦)) [1,3: // ]
+    [ <structure_append <structure_S_dx <Hr2 -Hr2 //
+    | <list_append_assoc <list_append_rcons_sn //
+    ]
+  ]
+]
+qed-.