matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma

   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/unwind/unwind_gen.ma".
  16 include "delayed_updating/unwind/unwind2_rmap.ma".
  17 include "delayed_updating/syntax/path_reverse.ma".
  18 include "delayed_updating/notation/functions/black_downtriangle_2.ma".
  19 include "ground/lib/list_tl.ma".
  20
  21 (* UNWIND FOR PATH **********************************************************)
  22
  23 definition unwind2_path (f) (p): path ≝
  24            ◆[▶[f]⇂(pᴿ)]p
  25 .
  26
  27 interpretation
  28   "unwind (path)"
  29   'BlackDownTriangle f p = (unwind2_path f p).
  30
  31 (* Basic constructions ******************************************************)
  32
  33 lemma unwind2_path_unfold (f) (p):
  34       ◆[▶[f]⇂(pᴿ)]p = ▼[f]p.
  35 // qed.
  36
  37 lemma unwind2_path_empty (f):
  38       (𝐞) = ▼[f]𝐞.
  39 // qed.
  40
  41 lemma unwind2_path_d_empty (f) (n):
  42       (𝗱(f＠⧣❨n❩)◗𝐞) = ▼[f](𝗱n◗𝐞).
  43 // qed.
  44
  45 lemma unwind2_path_d_lcons (f) (p) (l) (n:pnat):
  46       ▼[f∘𝐮❨n❩](l◗p) = ▼[f](𝗱n◗l◗p).
  47 #f #p #l #n <unwind2_path_unfold <unwind2_path_unfold
  48 <unwind_gen_d_lcons <reverse_lcons
  49 @(list_ind_rcons … p) -p // #p #l0 #_
  50 <reverse_rcons <reverse_lcons <reverse_lcons <reverse_rcons
  51 <list_tl_lcons <list_tl_lcons //
  52 qed.
  53
  54 lemma unwind2_path_m_sn (f) (p):
  55       ▼[f]p = ▼[f](𝗺◗p).
  56 #f #p <unwind2_path_unfold <unwind2_path_unfold
  57 <unwind_gen_m_sn <reverse_lcons
  58 @(list_ind_rcons … p) -p // #p #l #_
  59 <reverse_rcons <list_tl_lcons <list_tl_lcons //
  60 qed.
  61
  62 lemma unwind2_path_L_sn (f) (p):
  63       (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
  64 #f #p <unwind2_path_unfold <unwind2_path_unfold
  65 <unwind_gen_L_sn <reverse_lcons
  66 @(list_ind_rcons … p) -p // #p #l #_
  67 <reverse_rcons <list_tl_lcons <list_tl_lcons //
  68 qed.
  69
  70 lemma unwind2_path_A_sn (f) (p):
  71       (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
  72 #f #p <unwind2_path_unfold <unwind2_path_unfold
  73 <unwind_gen_A_sn <reverse_lcons
  74 @(list_ind_rcons … p) -p // #p #l #_
  75 <reverse_rcons <list_tl_lcons <list_tl_lcons //
  76 qed.
  77
  78 lemma unwind2_path_S_sn (f) (p):
  79       (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
  80 #f #p <unwind2_path_unfold <unwind2_path_unfold
  81 <unwind_gen_S_sn <reverse_lcons
  82 @(list_ind_rcons … p) -p // #p #l #_
  83 <reverse_rcons <list_tl_lcons <list_tl_lcons //
  84 qed.