matita/matita/contribs/lambdadelta/ground/relocation/gr_map.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/notation/functions/upspoon_1.ma".
  16 include "ground/notation/functions/uparrow_1.ma".
  17 include "ground/lib/stream.ma".
  18 include "ground/lib/bool.ma".
  19
  20 (* GENERIC RELOCATION MAPS **************************************************)
  21
  22 (*** rtmap *)
  23 definition gr_map: Type[0] ≝ stream bool.
  24
  25 (*** push *)
  26 definition gr_push (f): gr_map ≝ Ⓕ⨮f.
  27
  28 interpretation
  29   "push (generic relocation maps)"
  30   'UpSpoon f = (gr_push f).
  31
  32 (*** next *)
  33 definition gr_next (f): gr_map ≝ Ⓣ⨮f.
  34
  35 interpretation
  36   "next (generic relocation maps)"
  37   'UpArrow f = (gr_next f).
  38
  39 (* Basic constructions (specific) *******************************************)
  40
  41 (*** push_rew *)
  42 lemma gr_push_unfold (f): Ⓕ⨮f = ⫯f.
  43 // qed.
  44
  45 (*** next_rew *)
  46 lemma gr_next_unfold (f): Ⓣ⨮f = ↑f.
  47 // qed.
  48
  49 (* Basic inversions *********************************************************)
  50
  51 (*** injective_push *)
  52 lemma eq_inv_gr_push_bi: injective ? ? gr_push.
  53 #f1 #f2 <gr_push_unfold <gr_push_unfold #H destruct //
  54 qed-.
  55
  56 (*** discr_push_next *)
  57 lemma eq_inv_gr_push_next (f1) (f2): ⫯f1 = ↑f2 → ⊥.
  58 #f1 #f2 <gr_push_unfold <gr_next_unfold #H destruct
  59 qed-.
  60
  61 (*** discr_next_push *)
  62 lemma eq_inv_gr_next_push (f1) (f2): ↑f1 = ⫯f2 → ⊥.
  63 #f1 #f2 <gr_next_unfold <gr_push_unfold #H destruct
  64 qed-.
  65
  66 (*** injective_next *)
  67 lemma eq_inv_gr_next_bi: injective ? ? gr_next.
  68 #f1 #f2 <gr_next_unfold <gr_next_unfold #H destruct //
  69 qed-.