matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd.etc

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "delayed_updating/syntax/path_labels.ma".
  16 include "delayed_updating/notation/functions/downarrowrightsharp_2.ma".
  17 include "ground/arith/pnat_plus.ma".
  18
  19 (* HEAD BY DEPTH FOR PATH ***************************************************)
  20
  21 rec definition path_dhd (m) (p) on p: path ≝
  22 match p with
  23 [ list_empty     ⇒ 𝗟∗∗m
  24 | list_lcons l q ⇒
  25   match l with
  26   [ label_d n ⇒ l◗(path_dhd (m+n) q)
  27   | label_m   ⇒ l◗(path_dhd m q)
  28   | label_L   ⇒
  29     match m with
  30     [ punit   ⇒ l◗𝐞
  31     | psucc o ⇒ l◗(path_dhd o q)
  32     ]
  33   | label_A   ⇒ l◗(path_dhd m q)
  34   | label_S   ⇒ l◗(path_dhd m q)
  35   ]
  36 ].
  37
  38 interpretation
  39   "head by depth (reversed path)"
  40   'DownArrowRightSharp n p = (path_dhd n p).
  41
  42 (* basic constructions ****************************************************)
  43
  44 lemma path_dhd_empty (n:pnat):
  45       (𝗟∗∗n) = ↳⧣[n]𝐞.
  46 // qed.
  47
  48 lemma path_dhd_d_sn (p) (n) (m):
  49       (𝗱m◗↳⧣[n+m]p) = ↳⧣[n](𝗱m◗p).
  50 // qed.
  51
  52 lemma path_dhd_m_sn (p) (n):
  53       (𝗺◗↳⧣[n]p) = ↳⧣[n](𝗺◗p).
  54 // qed.
  55
  56 lemma path_dhd_L_sn_unit (p):
  57       (𝗟◗𝐞) = ↳⧣[𝟏](𝗟◗p).
  58 // qed.
  59
  60 lemma path_dhd_L_sn_succ (p) (n):
  61       (𝗟◗↳⧣[n]p) = ↳⧣[↑n](𝗟◗p).
  62 // qed.
  63
  64 lemma path_dhd_A_sn (p) (n):
  65       (𝗔◗↳⧣[n]p) = ↳⧣[n](𝗔◗p).
  66 // qed.
  67
  68 lemma path_dhd_S_sn (p) (n):
  69       (𝗦◗↳⧣[n]p) = ↳⧣[n](𝗦◗p).
  70 // qed.