matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.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 "ground/relocation/tr_compose.ma".
  16 include "ground/relocation/tr_uni.ma".
  17 include "delayed_updating/syntax/path.ma".
  18 include "delayed_updating/notation/functions/uparrow_4.ma".
  19 include "delayed_updating/notation/functions/uparrow_2.ma".
  20
  21 (* LIFT FOR PATH ***********************************************************)
  22
  23 (* Note: inner numeric labels are not liftable, so they are removed *)
  24 rec definition lift_gen (A:Type[0]) (k:?→?→A) (p) (f) on p ≝
  25 match p with
  26 [ list_empty     ⇒ k 𝐞 f
  27 | list_lcons l q ⇒
  28   match l with
  29   [ label_node_d n ⇒
  30     match q with
  31     [ list_empty     ⇒ lift_gen (A) (λp. k (𝗱❨f@❨n❩❩◗p)) q f
  32     | list_lcons _ _ ⇒ lift_gen (A) k q (f∘𝐮❨n❩)
  33     ]
  34   | label_edge_L   ⇒ lift_gen (A) (λp. k (𝗟◗p)) q (⫯f)
  35   | label_edge_A   ⇒ lift_gen (A) (λp. k (𝗔◗p)) q f
  36   | label_edge_S   ⇒ lift_gen (A) (λp. k (𝗦◗p)) q f
  37   ]
  38 ].
  39
  40 interpretation
  41   "lift (gneric)"
  42   'UpArrow A k p f = (lift_gen A k p f).
  43
  44 definition proj_path (p:path) (f:tr_map) ≝ p.
  45
  46 definition proj_rmap (p:path) (f:tr_map) ≝ f.
  47
  48 interpretation
  49   "lift (path)"
  50   'UpArrow f p = (lift_gen ? proj_path p f).
  51
  52 interpretation
  53   "lift (relocation map)"
  54   'UpArrow p f = (lift_gen ? proj_rmap p f).
  55
  56 (* Basic constructions ******************************************************)
  57
  58 lemma lift_L (A) (k) (p) (f):
  59       ↑❨(λp. k (𝗟◗p)), p, ⫯f❩ = ↑{A}❨k, 𝗟◗p, f❩.
  60 // qed.
  61
  62 (* Basic constructions with proj_path ***************************************)
  63
  64 lemma lift_append (p) (f) (q):
  65       q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
  66 #p elim p -p
  67 [ //
  68 | #l #p #IH #f #q cases l
  69   [
  70   | <lift_L in ⊢ (???%);
  71     >(list_append_rcons_sn ? q) in ⊢ (???(??(λ_.%)??));
  72
  73      <IH
  74   normalize >IH
  75   | //
  76
  77 (* Constructions with append ************************************************)
  78
  79 theorem lift_append_A (p2) (p1) (f):
  80         (↑[f]p1)●𝗔◗↑[↑[p1]f]p2 = ↑[f](p1●𝗔◗p2).
  81 #p2 #p1 elim p1 -p1
  82 [ #f normalize