matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.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.tcs.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/apply_2.ma".
  16 include "ground_2/relocation/nstream_eq.ma".
  17 include "ground_2/relocation/rtmap_istot.ma".
  18
  19 (* RELOCATION N-STREAM ******************************************************)
  20
  21 rec definition apply (i: nat) on i: rtmap → nat ≝ ?.
  22 * #n #f cases i -i
  23 [ @n
  24 | #i lapply (apply i f) -apply -i -f
  25   #i @(↑(n+i))
  26 ]
  27 defined.
  28
  29 interpretation "functional application (nstream)"
  30    'Apply f i = (apply i f).
  31
  32 (* Specific properties on at ************************************************)
  33
  34 lemma at_O1: ∀i2,f. @❪0, i2⨮f❫ ≘ i2.
  35 #i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
  36 qed.
  37
  38 lemma at_S1: ∀n,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, n⨮f❫ ≘ ↑(n+i2).
  39 #n elim n -n /3 width=7 by at_push, at_next/
  40 qed.
  41
  42 lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩.
  43 #i1 elim i1 -i1
  44 [ * // | #i #IH * /3 width=1 by at_S1/ ]
  45 qed.
  46
  47 lemma at_istot: ∀f. 𝐓❪f❫.
  48 /2 width=2 by ex_intro/ qed.
  49
  50 lemma at_plus2: ∀f,i1,i,n,m. @❪i1, n⨮f❫ ≘ i → @❪i1, (m+n)⨮f❫ ≘ m+i.
  51 #f #i1 #i #n #m #H elim m -m //
  52 #m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
  53 qed.
  54
  55 (* Specific inversion lemmas on at ******************************************)
  56
  57 lemma at_inv_O1: ∀f,n,i2. @❪0, n⨮f❫ ≘ i2 → n = i2.
  58 #f #n elim n -n /2 width=6 by at_inv_ppx/
  59 #n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
  60 #j2 #Hj * -i2 /3 width=1 by eq_f/
  61 qed-.
  62
  63 lemma at_inv_S1: ∀f,n,j1,i2. @❪↑j1, n⨮f❫ ≘ i2 →
  64                  ∃∃j2. @❪j1, f❫ ≘ j2 & ↑(n+j2) = i2.
  65 #f #n elim n -n /2 width=5 by at_inv_npx/
  66 #n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
  67 #j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
  68 #i2 #Hi * -j2 /2 width=3 by ex2_intro/
  69 qed-.
  70
  71 lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2.
  72 /2 width=6 by at_mono/ qed-.
  73
  74 (* Spercific forward lemmas on at *******************************************)
  75
  76 lemma at_increasing_plus: ∀f,n,i1,i2. @❪i1, n⨮f❫ ≘ i2 → i1 + n ≤ i2.
  77 #f #n *
  78 [ #i2 #H <(at_inv_O1 … H) -i2 //
  79 | #i1 #i2 #H elim (at_inv_S1 … H) -H
  80   #j1 #Ht * -i2 /4 width=2 by at_increasing, monotonic_le_plus_r, le_S_S/
  81 ]
  82 qed-.
  83
  84 lemma at_fwd_id: ∀f,n,i. @❪i, n⨮f❫ ≘ i → 0 = n.
  85 #f #n #i #H elim (at_fwd_id_ex … H) -H
  86 #g #H elim (push_inv_seq_dx … H) -H //
  87 qed-.
  88
  89 (* Basic properties *********************************************************)
  90
  91 lemma apply_O1: ∀n,f. (n⨮f)@❨0❩ = n.
  92 // qed.
  93
  94 lemma apply_S1: ∀n,f,i. (n⨮f)@❨↑i❩ = ↑(n+f@❨i❩).
  95 // qed.
  96
  97 lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
  98 #i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
  99 elim (eq_inv_seq_aux … H) -H normalize //
 100 #Hn #Hf /4 width=1 by eq_f2, eq_f/
 101 qed.
 102
 103 lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
 104 * #n #f * //
 105 qed.
 106
 107 (* Main inversion lemmas ****************************************************)
 108
 109 theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
 110 /2 width=4 by at_inj/ qed-.
 111
 112 corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
 113 * #n1 #f1 * #n2 #f2 #Hf @eq_seq
 114 [ @(Hf 0)
 115 | @nstream_eq_inv_ext -nstream_eq_inv_ext #i
 116   lapply (Hf 0) >apply_O1 >apply_O1 #H destruct
 117   lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
 118   /3 width=2 by injective_plus_r, injective_S/
 119 ]
 120 qed-.