matita/matita/contribs/lambdadelta/ground/relocation/pstream.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/lib/stream.ma".
  17 include "ground/arith/pnat.ma".
  18
  19 (* RELOCATION P-STREAM ******************************************************)
  20
  21 definition rtmap: Type[0] ≝ stream pnat.
  22
  23 definition push: rtmap → rtmap ≝ λf. 𝟏⨮f.
  24
  25 interpretation "push (pstream)" 'UpSpoon f = (push f).
  26
  27 definition next: rtmap → rtmap.
  28 * #p #f @(↑p⨮f)
  29 defined.
  30
  31 interpretation "next (pstream)" 'UpArrow f = (next f).
  32
  33 (* Basic properties *********************************************************)
  34
  35 lemma push_rew: ∀f. 𝟏⨮f = ⫯f.
  36 // qed.
  37
  38 lemma next_rew: ∀f,p. (↑p)⨮f = ↑(p⨮f).
  39 // qed.
  40
  41 (* Basic inversion lemmas ***************************************************)
  42
  43 lemma injective_push: injective ? ? push.
  44 #f1 #f2 <push_rew <push_rew #H destruct //
  45 qed-.
  46
  47 lemma discr_push_next: ∀f1,f2. ⫯f1 = ↑f2 → ⊥.
  48 #f1 * #p2 #f2 <push_rew <next_rew #H destruct
  49 qed-.
  50
  51 lemma discr_next_push: ∀f1,f2. ↑f1 = ⫯f2 → ⊥.
  52 * #p1 #f1 #f2 <next_rew <push_rew #H destruct
  53 qed-.
  54
  55 lemma injective_next: injective ? ? next.
  56 * #p1 #f1 * #p2 #f2 <next_rew <next_rew #H destruct //
  57 qed-.
  58
  59 lemma push_inv_seq_sn: ∀f,g,p. p⨮g = ⫯f → ∧∧ 𝟏 = p & g = f.
  60 #f #g #p <push_rew #H destruct /2 width=1 by conj/
  61 qed-.
  62
  63 lemma push_inv_seq_dx: ∀f,g,p. ⫯f = p⨮g → ∧∧ 𝟏 = p & g = f.
  64 #f #g #p <push_rew #H destruct /2 width=1 by conj/
  65 qed-.
  66
  67 lemma next_inv_seq_sn: ∀f,g,p. p⨮g = ↑f → ∃∃q. q⨮g = f & ↑q = p.
  68 * #q #f #g #p <next_rew #H destruct /2 width=3 by ex2_intro/
  69 qed-.
  70
  71 lemma next_inv_seq_dx: ∀f,g,p. ↑f = p⨮g → ∃∃q. q⨮g = f & ↑q = p.
  72 * #q #f #g #p <next_rew #H destruct /2 width=3 by ex2_intro/
  73 qed-.
  74
  75 lemma case_prop (Q:predicate rtmap):
  76       (∀f. Q (⫯f)) → (∀f. Q (↑f)) → ∀f. Q f.
  77 #Q #H1 #H2 * * //
  78 qed-.
  79
  80 lemma case_type0 (Q:rtmap→Type[0]):
  81       (∀f. Q (⫯f)) → (∀f. Q (↑f)) → ∀f. Q f.
  82 #Q #H1 #H2 * * //
  83 qed-.
  84
  85 lemma iota_push: ∀Q,a,b,f. a f = case_type0 Q a b (⫯f).
  86 // qed.
  87
  88 lemma iota_next: ∀Q,a,b,f. b f = case_type0 Q a b (↑f).
  89 #Q #a #b * //
  90 qed.