matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.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/substitution/lift.ma".
  16 include "delayed_updating/syntax/path_depth.ma".
  17 include "ground/relocation/tr_id_compose.ma".
  18 include "ground/relocation/tr_compose_compose.ma".
  19 include "ground/relocation/tr_compose_pn.ma".
  20 include "ground/relocation/tr_compose_eq.ma".
  21 include "ground/relocation/tr_pn_eq.ma".
  22 include "ground/lib/stream_eq_eq.ma".
  23
  24 (* LIFT FOR PATH ***********************************************************)
  25
  26 (* Constructions with depth ************************************************)
  27
  28 lemma lift_rmap_decompose (p) (f):
  29       ↑[p]f ≗ (⫯*[❘p❘]f)∘(↑[p]𝐢).
  30 #p @(list_ind_rcons … p) -p
  31 [ #f <lift_rmap_empty <lift_rmap_empty <tr_pushs_zero //
  32 | #p * [ #n ] #IH #f //
  33   [ <lift_rmap_d_dx <lift_rmap_d_dx <depth_d_dx
  34     @(stream_eq_trans … (tr_compose_assoc …))
  35     /2 width=1 by tr_compose_eq_repl/
  36   | <lift_rmap_L_dx <lift_rmap_L_dx <depth_L_dx
  37     <tr_pushs_succ <tr_compose_push_bi
  38     /2 width=1 by tr_push_eq_repl/
  39   ]
  40 ]
  41 qed.
  42
  43 lemma lift_rmap_pap_le (f) (p) (n):
  44       (↑[p]𝐢)@❨n❩ < ↑❘p❘ → (↑[p]𝐢)@❨n❩ = (↑[p]f)@❨n❩.
  45 #f #p #n #Hn
  46 >(tr_pap_eq_repl … (↑[p]f) … (lift_rmap_decompose …))
  47 <tr_compose_pap @tr_pap_pushs_le //
  48 qed.