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