update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
index 9cdfe620ff67088da01fa37b512b41f1fa3e9e65..4610e4f69954158d247c451c92832a7819ff2455 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
@@ -19,25 +19,25 @@ include "ground/arith/nat_pred_succ.ma".
 
 (* HEAD FOR PATH ************************************************************)
 
-rec definition path_head (m) (p) on p: path ≝
-match m with
+rec definition path_head (n) (p) on p: path ≝
+match n with
 [ nzero  ⇒ 𝐞
-| ninj o ⇒ 
+| ninj m ⇒
   match p with
-  [ list_empty     ⇒ 𝗟∗∗m
+  [ list_empty     ⇒ 𝗟∗∗n
   | list_lcons l q ⇒
     match l with
-    [ label_d n ⇒ l◗(path_head (m+n) q)
-    | label_m   ⇒ l◗(path_head m q)
-    | label_L   ⇒ l◗(path_head (↓o) q)
-    | label_A   ⇒ l◗(path_head m q)
-    | label_S   ⇒ l◗(path_head m q)
+    [ label_d k ⇒ (path_head (n+k) q)◖l
+    | label_m   ⇒ (path_head n q)◖l
+    | label_L   ⇒ (path_head (↓m) q)◖l
+    | label_A   ⇒ (path_head n q)◖l
+    | label_S   ⇒ (path_head n q)◖l
     ]
   ]
 ].
 
 interpretation
-  "head (reversed path)"
+  "head (path)"
   'DownArrowRight n p = (path_head n p).
 
 (* basic constructions ****************************************************)
@@ -50,41 +50,85 @@ lemma path_head_empty (n):
       (𝗟∗∗n) = ↳[n]𝐞.
 * // qed.
 
-lemma path_head_d_sn (p) (n) (m:pnat):
-      (𝗱m◗↳[↑n+m]p) = ↳[↑n](𝗱m◗p).
+lemma path_head_d_dx (p) (n) (k:pnat):
+      (↳[↑n+k]p)◖𝗱k = ↳[↑n](p◖𝗱k).
 // qed.
 
-lemma path_head_m_sn (p) (n):
-      (𝗺◗↳[↑n]p) = ↳[↑n](𝗺◗p).
+lemma path_head_m_dx (p) (n):
+      (↳[↑n]p)◖𝗺 = ↳[↑n](p◖𝗺).
 // qed.
 
-lemma path_head_L_sn (p) (n):
-      (𝗟◗↳[n]p) = ↳[↑n](𝗟◗p).
+lemma path_head_L_dx (p) (n):
+      (↳[n]p)◖𝗟 = ↳[↑n](p◖𝗟).
 #p #n
 whd in ⊢ (???%); //
 qed.
 
-lemma path_head_A_sn (p) (n):
-      (𝗔◗↳[↑n]p) = ↳[↑n](𝗔◗p).
+lemma path_head_A_dx (p) (n):
+      (↳[↑n]p)◖𝗔 = ↳[↑n](p◖𝗔).
 // qed.
 
-lemma path_head_S_sn (p) (n):
-      (𝗦◗↳[↑n]p) = ↳[↑n](𝗦◗p).
+lemma path_head_S_dx (p) (n):
+      (↳[↑n]p)◖𝗦 = ↳[↑n](p◖𝗦).
 // qed.
 
 (* Basic inversions *********************************************************)
 
+lemma eq_inv_path_head_zero_dx (q) (p):
+      q = ↳[𝟎]p → 𝐞 = q.
+#q * //
+qed-.
+
 lemma eq_inv_path_empty_head (p) (n):
       (𝐞) = ↳[n]p → 𝟎 = n.
 *
-[ #m <path_head_empty #H0
-  <(eq_inv_empty_labels … H0) -m //
-| * [ #n ] #p #n @(nat_ind_succ … n) -n // #m #_
-  [ <path_head_d_sn
-  | <path_head_m_sn
-  | <path_head_L_sn
-  | <path_head_A_sn
-  | <path_head_S_sn
+[ #n <path_head_empty #H0
+  <(eq_inv_empty_labels … H0) -n //
+| * [ #k ] #p #n @(nat_ind_succ … n) -n // #n #_
+  [ <path_head_d_dx
+  | <path_head_m_dx
+  | <path_head_L_dx
+  | <path_head_A_dx
+  | <path_head_S_dx
   ] #H0 destruct
 ]
 qed-.
+
+(* Constructions with path_append *******************************************)
+
+lemma path_head_refl_append (p) (q) (n):
+      q = ↳[n]q → q = ↳[n](p●q).
+#p #q elim q -q
+[ #n #Hn <(eq_inv_path_empty_head … Hn) -Hn //
+| #l #q #IH #n @(nat_ind_succ … n) -n
+  [ #Hq | #n #_ cases l [ #k ] ]
+  [ lapply (eq_inv_path_head_zero_dx … Hq) -Hq #Hq destruct
+  | <path_head_d_dx <path_head_d_dx
+  | <path_head_m_dx <path_head_m_dx
+  | <path_head_L_dx <path_head_L_dx
+  | <path_head_A_dx <path_head_A_dx
+  | <path_head_S_dx <path_head_S_dx
+  ] #Hq
+  elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+  /3 width=1 by eq_f/
+]
+qed-.
+
+(* Inversions with path_append **********************************************)
+
+lemma eq_inv_path_head_refl_append (p) (q) (n):
+      q = ↳[n](p●q) → q = ↳[n]q.
+#p #q elim q -q
+[ #n #Hn <(eq_inv_path_empty_head … Hn) -p //
+| #l #q #IH #n @(nat_ind_succ … n) -n //
+  #n #_ cases l [ #k ]
+  [ <path_head_d_dx <path_head_d_dx
+  | <path_head_m_dx <path_head_m_dx
+  | <path_head_L_dx <path_head_L_dx
+  | <path_head_A_dx <path_head_A_dx
+  | <path_head_S_dx <path_head_S_dx
+  ] #Hq
+  elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+  /3 width=1 by eq_f/
+]
+qed-.