Peano axioms of natural numbers in Agda

gistfile1.txt

module Peano where

open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary.Core using (_≢_; refl)

{-
already defined:
data ℕ : Set where
  zero : ℕ             -- axiom 1
  suc  : (n : ℕ) -> ℕ  -- axiom 2
-}

-- axiom 3
-- there does not exist that a natural number m
-- such that 0 ≡ suc m
lemma1 : (n : ℕ) -> zero ≢ suc n
lemma1 _ ()

-- axiom 4
-- if m ≢ n then suc m ≢ suc n
lemma2 : (m n : ℕ) -> m ≢ n -> suc m ≢ suc n
lemma2 m .m p refl = p refl

-- axiom 5
-- Given P : ℕ -> Set such that
-- 1) P zero is satisfied
-- 2) forall m : P m -> P (suc m) is satisfied
-- then forall n : P n is satisfied
lemma3 : (P : ℕ -> Set) -> P zero -> 
         ((m : ℕ) -> P m -> P (suc m)) ->
         (n : ℕ) -> P n
lemma3 _ p _ zero = p
lemma3 P p f (suc n) = f n (lemma3 P p f n)