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 npsucc (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 = (npsucc 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 npsucc_zero: (𝟏) = ↑𝟎.
  39 // qed.
  40
  41 lemma npsucc_inj (p): (↑p) = ↑(ninj p).
  42 // qed.
  43
  44 lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
  45 // qed.
  46
  47 lemma nsucc_inj (p): ninj (↑p) = ↑(ninj p).
  48 // qed.
  49
  50 lemma npsucc_succ (n): psucc (npsucc n) = npsucc (nsucc n).
  51 // qed.
  52
  53 (* Basic eliminations *******************************************************)
  54
  55 (*** nat_ind *)
  56 lemma nat_ind_succ (Q:predicate …):
  57       Q (𝟎) → (∀n. Q n → Q (↑n)) → ∀n. Q n.
  58 #Q #IH1 #IH2 * //
  59 #p elim p -p /2 width=1 by/
  60 qed-.
  61
  62 (*** nat_elim2 *)
  63 lemma nat_ind_2_succ (Q:relation2 …):
  64       (∀n. Q (𝟎) n) →
  65       (∀m. Q m (𝟎) → Q (↑m) (𝟎)) →
  66       (∀m,n. Q m n → Q (↑m) (↑n)) →
  67       ∀m,n. Q m n.
  68 #Q #IH1 #IH2 #IH3 #m @(nat_ind_succ … m) -m [ // ]
  69 #m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
  70 qed-.
  71
  72 (* Basic inversions *********************************************************)
  73
  74 lemma eq_inv_npsucc_bi: injective … npsucc.
  75 * [| #p1 ] * [2,4: #p2 ]
  76 [ 1,4: <npsucc_zero <npsucc_inj #H destruct
  77 | <npsucc_inj <npsucc_inj #H destruct //
  78 | //
  79 ]
  80 qed-.
  81
  82 (*** injective_S *)
  83 lemma eq_inv_nsucc_bi: injective … nsucc.
  84 #n1 #n2 #H
  85 @eq_inv_npsucc_bi @eq_inv_ninj_bi @H
  86 qed-.
  87
  88 lemma eq_inv_nsucc_zero (m): ↑m = 𝟎 → ⊥.
  89 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
  90 qed-.
  91
  92 lemma eq_inv_zero_nsucc (m): 𝟎 = ↑m → ⊥.
  93 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
  94 qed-.
  95
  96 (*** succ_inv_refl_sn *)
  97 lemma nsucc_inv_refl (n): n = ↑n → ⊥.
  98 #n @(nat_ind_succ … n) -n
  99 [ /2 width=2 by eq_inv_zero_nsucc/
 100 | #n #IH #H /3 width=1 by eq_inv_nsucc_bi/
 101 ]
 102 qed-.