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 (* NON-NEGATIVE INTEGERS ****************************************************)
19 definition nsucc: nat → nat ≝ λm. match m with
25 "successor (non-negative integers"
26 'UpArrow m = (nsucc m).
28 (* Basic rewrites ***********************************************************)
30 lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
33 lemma nsucc_inj (p): ninj (↑p) = ↑(ninj p).
36 (* Basic eliminations *******************************************************)
39 lemma nat_ind (Q:predicate …):
40 Q (𝟎) → (∀n. Q n → Q (↑n)) → ∀n. Q n.
42 #p elim p -p /2 width=1 by/
46 lemma nat_ind_2 (Q:relation2 …):
49 (∀m,n. Q m n → Q (↑m) (↑n)) →
51 #Q #IH1 #IH2 #IH3 #m elim m -m [ // ]
52 #m #IH #n elim n -n /2 width=1 by/
55 (* Basic inversions *********************************************************)
58 lemma eq_inv_nsucc_bi: injective … nsucc.
59 * [| #p1 ] * [2,4: #p2 ]
60 [1,4: <nsucc_zero <nsucc_inj #H destruct
61 | <nsucc_inj <nsucc_inj #H destruct //
66 lemma eq_inv_nsucc_zero (m): ↑m = 𝟎 → ⊥.
67 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
70 lemma eq_inv_nzero_succ (m): 𝟎 = ↑m → ⊥.
71 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct