1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/arith/nat.ma".
17 (* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
19 definition nsucc_pos (m): pnat ≝
26 "positive successor (non-negative integers)"
27 'UpArrow m = (nsucc_pos m).
29 definition nsucc (m): nat ≝
33 "successor (non-negative integers)"
34 'UpArrow m = (nsucc m).
36 (* Basic constructions ******************************************************)
38 lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
41 lemma nsucc_inj (p): ninj (↑p) = ↑(ninj p).
44 (* Basic eliminations *******************************************************)
47 lemma nat_ind_succ (Q:predicate …):
48 Q (𝟎) → (∀n. Q n → Q (↑n)) → ∀n. Q n.
50 #p elim p -p /2 width=1 by/
54 lemma nat_ind_2_succ (Q:relation2 …):
57 (∀m,n. Q 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/
63 (* Basic inversions ***************************************************************)
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 //
74 lemma eq_inv_nsucc_zero (m): ↑m = 𝟎 → ⊥.
75 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
78 lemma eq_inv_zero_nsucc (m): 𝟎 = ↑m → ⊥.
79 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
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/