matita/matita/contribs/lambdadelta/ground/relocation/rtmap_uni.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/uniform_1.ma".
  16 include "ground/relocation/rtmap_nexts.ma".
  17 include "ground/relocation/rtmap_id.ma".
  18 include "ground/relocation/rtmap_isuni.ma".
  19
  20 (* RELOCATION MAP ***********************************************************)
  21
  22 definition uni (n) ≝ ↑*[n] 𝐈𝐝.
  23
  24 interpretation "uniform relocation (rtmap)"
  25    'Uniform n = (uni n).
  26
  27 (* Basic properties *********************************************************)
  28
  29 lemma uni_zero: 𝐈𝐝 = 𝐔❨𝟎❩.
  30 // qed.
  31
  32 lemma uni_succ: ∀n. ↑𝐔❨n❩ = 𝐔❨↑n❩.
  33 /2 width=1 by nexts_S/ qed.
  34
  35 (* Basic inversion lemmas ***************************************************)
  36
  37 lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯f → 𝟎 = n ∧ 𝐈𝐝 ≡ f.
  38 #f #n @(nat_ind_succ … n) -n
  39 [ /3 width=5 by eq_inv_pp, conj/
  40 | #n #_ <uni_succ #H elim (eq_inv_np … H) -H //
  41 ]
  42 qed-.
  43
  44 lemma uni_inv_push_sn: ∀f,n. ⫯f ≡ 𝐔❨n❩ → 𝟎 = n ∧ 𝐈𝐝 ≡ f.
  45 /3 width=1 by uni_inv_push_dx, eq_sym/ qed-.
  46
  47 lemma uni_inv_id_dx: ∀n. 𝐔❨n❩ ≡ 𝐈𝐝 → 𝟎 = n.
  48 #n <id_rew #H elim (uni_inv_push_dx … H) -H //
  49 qed-.
  50
  51 lemma uni_inv_id_sn: ∀n.  𝐈𝐝 ≡ 𝐔❨n❩ → 𝟎 = n.
  52 /3 width=1 by uni_inv_id_dx, eq_sym/ qed-.
  53
  54 lemma uni_inv_next_dx: ∀f,n. 𝐔❨n❩ ≡ ↑f → ∃∃m. 𝐔❨m❩ ≡ f & ↑m = n.
  55 #f #n @(nat_ind_succ … n) -n
  56 [ <uni_zero <id_rew #H elim (eq_inv_pn … H) -H //
  57 | #n #_ <uni_succ /3 width=5 by eq_inv_nn, ex2_intro/
  58 ]
  59 qed-.
  60
  61 lemma uni_inv_next_sn: ∀f,n. ↑f ≡ 𝐔❨n❩ → ∃∃m. 𝐔❨m❩ ≡ f & ↑m = n.
  62 /3 width=1 by uni_inv_next_dx, eq_sym/ qed-.
  63
  64 (* Properties with test for identity ****************************************)
  65
  66 lemma uni_isid: ∀f. 𝐈❪f❫ → 𝐔❨𝟎❩ ≡ f.
  67 /2 width=1 by eq_id_inv_isid/ qed-.
  68
  69 (* Inversion lemmas with test for identity **********************************)
  70
  71 lemma uni_inv_isid: ∀f. 𝐔❨𝟎❩ ≡ f → 𝐈❪f❫.
  72 /2 width=1 by eq_id_isid/ qed-.
  73
  74 (* Properties with finite colength assignment ***************************)
  75
  76 lemma fcla_uni: ∀n. 𝐂❪𝐔❨n❩❫ ≘ n.
  77 #n @(nat_ind_succ … n) -n
  78 /2 width=1 by fcla_isid, fcla_next/
  79 qed.
  80
  81 (* Properties with test for finite colength ***************************)
  82
  83 lemma isfin_uni: ∀n. 𝐅❪𝐔❨n❩❫.
  84 /3 width=2 by ex_intro/ qed.
  85
  86 (* Properties with test for uniformity **************************************)
  87
  88 lemma isuni_uni: ∀n. 𝐔❪𝐔❨n❩❫.
  89 #n @(nat_ind_succ … n) -n
  90 /3 width=3 by isuni_isid, isuni_next/
  91 qed.
  92
  93 lemma uni_isuni: ∀f. 𝐔❪f❫ → ∃n. 𝐔❨n❩ ≡ f.
  94 #f #H elim H -f /3 width=2 by uni_isid, ex_intro/
  95 #f #_ #g #H * /3 width=6 by eq_next, ex_intro/
  96 qed-.
  97
  98 (* Inversion lemmas with test for uniformity ********************************)
  99
 100 lemma uni_inv_isuni: ∀n,f. 𝐔❨n❩ ≡ f →  𝐔❪f❫.
 101 #n @(nat_ind_succ … n) -n
 102 [ /3 width=1 by uni_inv_isid, isuni_isid/
 103 | #n #IH #x <uni_succ #H elim (eq_inv_nx … H) -H /3 width=3 by isuni_next/
 104 ]
 105 qed-.