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