matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.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/apply_2.ma".
  16 include "ground/arith/pnat_plus.ma".
  17 include "ground/relocation/tr_map.ma".
  18
  19 (* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
  20
  21 (*** apply *)
  22 rec definition tr_pap (i: pnat) on i: tr_map → pnat.
  23 * #p #f cases i -i
  24 [ @p
  25 | #i lapply (tr_pap i f) -tr_pap -i -f
  26   #i @(i+p)
  27 ]
  28 defined.
  29
  30 interpretation
  31   "functional positive application (total relocation maps)"
  32   'Apply f i = (tr_pap i f).
  33
  34 (* Basic constructions ******************************************************)
  35
  36 (*** apply_O1 *)
  37 lemma tr_pap_unit (f):
  38       ∀p. p = (p⨮f)@❨𝟏❩.
  39 // qed.
  40
  41 (*** apply_S1 *)
  42 lemma tr_pap_succ (f):
  43       ∀p,i. f@❨i❩+p = (p⨮f)@❨↑i❩.
  44 // qed.
  45 (*
  46 (*** apply_S2 *)
  47 lemma tr_pap_next (f):
  48       ∀i. ↑(f@❨i❩) = (↑f)@❨i❩.
  49 * #p #f * //
  50 qed.
  51
  52
  53
  54 (*** apply_eq_repl *)
  55 lemma apply_eq_repl (i):
  56       ∀f1,f2. f1 ≗ f2 → f1@❨i❩ = f2@❨i❩.
  57
  58
  59 (i): pr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
  60 #i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
  61 elim (eq_inv_seq_aux … H) -H #Hp #Hf //
  62 >apply_S1 >apply_S1 /3 width=1 by eq_f2/
  63 qed.
  64
  65
  66 (* Main inversion lemmas ****************************************************)
  67
  68 theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
  69 /2 width=4 by gr_pat_inj/ qed-.
  70
  71 corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
  72 * #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
  73 [ @(Hf (𝟏))
  74 | @nstream_eq_inv_ext -nstream_eq_inv_ext #i
  75   lapply (Hf (𝟏)) >apply_O1 >apply_O1 #H destruct
  76   lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
  77   /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
  78 ]
  79 qed-.
  80
  81 (*
  82 include "ground/relocation/pstream_eq.ma".
  83 *)
  84
  85 (*
  86 include "ground/relocation/rtmap_istot.ma".
  87
  88 lemma at_istot: ∀f. 𝐓❨f❩.
  89 /2 width=2 by ex_intro/ qed.
  90 *)
  91 *)