matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.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/pr_pat.ma".
  18 include "ground/relocation/tr_map.ma".
  19 (*
  20 include "ground/arith/pnat_le_plus.ma".
  21 include "ground/relocation/pstream_eq.ma".
  22 include "ground/relocation/rtmap_istot.ma".
  23 *)
  24 (* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
  25
  26 (*** apply *)
  27 rec definition tr_pat (i: pnat) on i: tr_map → pnat.
  28 * #p #f cases i -i
  29 [ @p
  30 | #i lapply (tr_pat i f) -tr_pat -i -f
  31   #i @(i+p)
  32 ]
  33 defined.
  34
  35 interpretation
  36   "functional positive application (total relocation maps)"
  37   'apply f i = (tr_pat i f).
  38
  39 (* Constructions with pr_pat ***********************************************)
  40
  41 (*** at_O1 *)
  42 lemma pr_pat_unit_sn: ∀i2,f. @❨𝟏,𝐭❨i2⨮f❩❩ ≘ i2.
  43 #i2 elim i2 -i2 /2 width=5 by gr_pat_refl, gr_pat_next/
  44 qed.
  45
  46 lemma at_S1: ∀p,f,i1,i2. @❨i1, f❩ ≘ i2 → @❨↑i1, p⨮f❩ ≘ i2+p.
  47 #p elim p -p /3 width=7 by gr_pat_push, gr_pat_next/
  48 qed.
  49
  50 lemma at_total: ∀i1,f. @❨i1, f❩ ≘ f@❨i1❩.
  51 #i1 elim i1 -i1
  52 [ * // | #i #IH * /3 width=1 by at_S1/ ]
  53 qed.
  54
  55 lemma at_istot: ∀f. 𝐓❨f❩.
  56 /2 width=2 by ex_intro/ qed.
  57
  58 lemma at_plus2: ∀f,i1,i,p,q. @❨i1, p⨮f❩ ≘ i → @❨i1, (p+q)⨮f❩ ≘ i+q.
  59 #f #i1 #i #p #q #H elim q -q
  60 /2 width=5 by gr_pat_next/
  61 qed.
  62
  63 (* Inversion lemmas on at (specific) ******************************************)
  64
  65 lemma at_inv_O1: ∀f,p,i2. @❨𝟏, p⨮f❩ ≘ i2 → p = i2.
  66 #f #p elim p -p /2 width=6 by gr_pat_inv_unit_push/
  67 #p #IH #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
  68 #j2 #Hj * -i2 /3 width=1 by eq_f/
  69 qed-.
  70
  71 lemma at_inv_S1: ∀f,p,j1,i2. @❨↑j1, p⨮f❩ ≘ i2 →
  72                  ∃∃j2. @❨j1, f❩ ≘ j2 & j2+p = i2.
  73 #f #p elim p -p /2 width=5 by gr_pat_inv_succ_push/
  74 #p #IH #j1 #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
  75 #j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
  76 #i2 #Hi * -j2 /2 width=3 by ex2_intro/
  77 qed-.
  78
  79 lemma at_inv_total: ∀f,i1,i2. @❨i1, f❩ ≘ i2 → f@❨i1❩ = i2.
  80 /2 width=6 by fr2_nat_mono/ qed-.
  81
  82 (* Forward lemmas on at (specific) *******************************************)
  83
  84 lemma at_increasing_plus: ∀f,p,i1,i2. @❨i1, p⨮f❩ ≘ i2 → i1 + p ≤ ↑i2.
  85 #f #p *
  86 [ #i2 #H <(at_inv_O1 … H) -i2 //
  87 | #i1 #i2 #H elim (at_inv_S1 … H) -H
  88   #j1 #Ht * -i2 <pplus_succ_sn
  89   /4 width=2 by gr_pat_increasing, ple_plus_bi_dx, ple_succ_bi/
  90 ]
  91 qed-.
  92
  93 lemma at_fwd_id: ∀f,p,i. @❨i, p⨮f❩ ≘ i → 𝟏 = p.
  94 #f #p #i #H elim (gr_pat_des_id … H) -H
  95 #g #H elim (push_inv_seq_dx … H) -H //
  96 qed-.
  97
  98 (* Basic properties *********************************************************)
  99
 100 lemma tr_pat_O1: ∀p,f. (p⨮f)@❨𝟏❩ = p.
 101 // qed.
 102
 103 lemma tr_pat_S1: ∀p,f,i. (p⨮f)@❨↑i❩ = f@❨i❩+p.
 104 // qed.
 105
 106 lemma tr_pat_eq_repl (i): gr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
 107 #i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
 108 elim (eq_inv_seq_aux … H) -H #Hp #Hf //
 109 >tr_pat_S1 >tr_pat_S1 /3 width=1 by eq_f2/
 110 qed.
 111
 112 lemma tr_pat_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
 113 * #p #f * //
 114 qed.
 115
 116 (* Main inversion lemmas ****************************************************)
 117
 118 theorem tr_pat_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
 119 /2 width=4 by gr_pat_inj/ qed-.
 120
 121 corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
 122 * #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
 123 [ @(Hf (𝟏))
 124 | @nstream_eq_inv_ext -nstream_eq_inv_ext #i
 125   ltr_pat (Hf (𝟏)) >tr_pat_O1 >tr_pat_O1 #H destruct
 126   ltr_pat (Hf (↑i)) >tr_pat_S1 >tr_pat_S1 #H
 127   /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
 128 ]
 129 qed-.