matita/matita/contribs/lambdadelta/ground_2/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_2/notation/functions/uniform_1.ma".
  16 include "ground_2/relocation/rtmap_id.ma".
  17 include "ground_2/relocation/rtmap_isuni.ma".
  18
  19 (* RELOCATION MAP ***********************************************************)
  20
  21 rec definition uni (n:nat) on n: rtmap  ≝ match n with
  22 [ O   ⇒ 𝐈𝐝
  23 | S n ⇒ ↑(uni n)
  24 ].
  25
  26 interpretation "uniform relocation (rtmap)"
  27    'Uniform n = (uni n).
  28
  29 (* Basic properties *********************************************************)
  30
  31 lemma uni_zero: 𝐈𝐝 = 𝐔❨0❩.
  32 // qed.
  33
  34 lemma uni_succ: ∀n. ↑𝐔❨n❩ = 𝐔❨↑n❩.
  35 // qed.
  36
  37 (* Basic inversion lemmas ***************************************************)
  38
  39 lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯f → 0 = n ∧ 𝐈𝐝 ≡ f.
  40 #f * /3 width=5 by eq_inv_pp, conj/
  41 #n <uni_succ #H elim (eq_inv_np … H) -H //
  42 qed-.
  43
  44 lemma uni_inv_push_sn: ∀f,n. ⫯f ≡ 𝐔❨n❩ → 0 = n ∧ 𝐈𝐝 ≡ f.
  45 /3 width=1 by uni_inv_push_dx, eq_sym/ qed-.
  46
  47 lemma uni_inv_id_dx: ∀n. 𝐔❨n❩ ≡ 𝐈𝐝 → 0 = n.
  48 #n <id_rew #H elim (uni_inv_push_dx … H) -H //
  49 qed-.
  50
  51 lemma uni_inv_id_sn: ∀n.  𝐈𝐝 ≡ 𝐔❨n❩ → 0 = 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 *
  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❫ → 𝐔❨0❩ ≡ 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. 𝐔❨0❩ ≡ 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 elim n -n /2 width=1 by fcla_isid, fcla_next/
  78 qed.
  79
  80 (* Properties with test for finite colength ***************************)
  81
  82 lemma isfin_uni: ∀n. 𝐅❪𝐔❨n❩❫.
  83 /3 width=2 by ex_intro/ qed.
  84
  85 (* Properties with test for uniformity **************************************)
  86
  87 lemma isuni_uni: ∀n. 𝐔❪𝐔❨n❩❫.
  88 #n elim n -n /3 width=3 by isuni_isid, isuni_next/
  89 qed.
  90
  91 lemma uni_isuni: ∀f. 𝐔❪f❫ → ∃n. 𝐔❨n❩ ≡ f.
  92 #f #H elim H -f /3 width=2 by uni_isid, ex_intro/
  93 #f #_ #g #H * /3 width=6 by eq_next, ex_intro/
  94 qed-.
  95
  96 (* Inversion lemmas with test for uniformity ********************************)
  97
  98 lemma uni_inv_isuni: ∀n,f. 𝐔❨n❩ ≡ f →  𝐔❪f❫.
  99 #n elim n -n /3 width=1 by uni_inv_isid, isuni_isid/
 100 #n #IH #x <uni_succ #H elim (eq_inv_nx … H) -H /3 width=3 by isuni_next/
 101 qed-.