matita/matita/contribs/lambdadelta/ground/arith/nat_succ.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/arith/nat.ma".
  16
  17 (* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
  18
  19 definition nsucc_pos (m): pnat ≝
  20 match m with
  21 [ nzero  ⇒ 𝟏
  22 | ninj p ⇒ ↑p
  23 ].
  24
  25 interpretation
  26   "positive successor (non-negative integers)"
  27   'UpArrow m = (nsucc_pos m).
  28
  29 definition nsucc (m): nat ≝
  30            ninj (↑m).
  31
  32 interpretation
  33   "successor (non-negative integers)"
  34   'UpArrow m = (nsucc m).
  35
  36 (* Basic constructions ******************************************************)
  37
  38 lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
  39 // qed.
  40
  41 lemma nsucc_inj (p): ninj (↑p) = ↑(ninj p).
  42 // qed.
  43
  44 (* Basic eliminations *******************************************************)
  45
  46 (*** nat_ind *)
  47 lemma nat_ind_succ (Q:predicate …):
  48       Q (𝟎) → (∀n. Q n → Q (↑n)) → ∀n. Q n.
  49 #Q #IH1 #IH2 * //
  50 #p elim p -p /2 width=1 by/
  51 qed-.
  52
  53 (*** nat_elim2 *)
  54 lemma nat_ind_2_succ (Q:relation2 …):
  55       (∀n. Q (𝟎) n) →
  56       (∀m. Q (↑m) (𝟎)) →
  57       (∀m,n. Q m n → Q (↑m) (↑n)) →
  58       ∀m,n. Q m n.
  59 #Q #IH1 #IH2 #IH3 #m @(nat_ind_succ … m) -m [ // ]
  60 #m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
  61 qed-.
  62
  63 (* Basic inversions *********************************************************)
  64
  65 (*** injective_S *)
  66 lemma eq_inv_nsucc_bi: injective … nsucc.
  67 * [| #p1 ] * [2,4: #p2 ]
  68 [1,4: <nsucc_zero <nsucc_inj #H destruct
  69 | <nsucc_inj <nsucc_inj #H destruct //
  70 | //
  71 ]
  72 qed-.
  73
  74 lemma eq_inv_nsucc_zero (m): ↑m = 𝟎 → ⊥.
  75 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
  76 qed-.
  77
  78 lemma eq_inv_zero_nsucc (m): 𝟎 = ↑m → ⊥.
  79 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
  80 qed-.
  81
  82 (*** succ_inv_refl_sn *)
  83 lemma nsucc_inv_refl (n): n = ↑n → ⊥.
  84 #n @(nat_ind_succ … n) -n
  85 [ /2 width=2 by eq_inv_zero_nsucc/
  86 | #n #IH #H /3 width=1 by eq_inv_nsucc_bi/
  87 ]
  88 qed-.