partial 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
deleted file mode 100644 (file)
index 4610e4f..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
+++ /dev/null
@@ -1,134 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/syntax/path_labels.ma".
-include "delayed_updating/notation/functions/downarrowright_2.ma".
-include "ground/arith/nat_plus.ma".
-include "ground/arith/nat_pred_succ.ma".
-
-(* HEAD FOR PATH ************************************************************)
-
-rec definition path_head (n) (p) on p: path ≝
-match n with
-[ nzero  ⇒ 𝐞
-| ninj m ⇒
-  match p with
-  [ list_empty     ⇒ 𝗟∗∗n
-  | list_lcons l q ⇒
-    match l with
-    [ 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 (path)"
-  'DownArrowRight n p = (path_head n p).
-
-(* basic constructions ****************************************************)
-
-lemma path_head_zero (p):
-      (𝐞) = ↳[𝟎]p.
-* // qed.
-
-lemma path_head_empty (n):
-      (𝗟∗∗n) = ↳[n]𝐞.
-* // qed.
-
-lemma path_head_d_dx (p) (n) (k:pnat):
-      (↳[↑n+k]p)◖𝗱k = ↳[↑n](p◖𝗱k).
-// qed.
-
-lemma path_head_m_dx (p) (n):
-      (↳[↑n]p)◖𝗺 = ↳[↑n](p◖𝗺).
-// qed.
-
-lemma path_head_L_dx (p) (n):
-      (↳[n]p)◖𝗟 = ↳[↑n](p◖𝗟).
-#p #n
-whd in ⊢ (???%); //
-qed.
-
-lemma path_head_A_dx (p) (n):
-      (↳[↑n]p)◖𝗔 = ↳[↑n](p◖𝗔).
-// qed.
-
-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.
-*
-[ #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-.