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