Proof: Difference between revisions

-- 1.1. The natural numbers.

-- ℕ-formation: ℕ is set.

data ℕ : Set where

zero : ℕ

suc : ℕ → ℕ

-- 2.1. The rule of addition.

-- via ℕ-elimination.

infixl 6 _+_

_+_ : ℕ → ℕ → ℕ

suc m + n = suc (m + n)

-- 3.1. Sum of any two even numbers is even.

-- This function takes any two even numbers and returns their sum as an even

-- number, this is the type, i.e. logical proposition, algorithm itself is a

-- typechecker performs that proof (by unification, so that this is a form of

-- compile-time verification).

even+even≡even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ (m + n)

even+even≡even (2+ m) n = 2+ (even+even≡even m n)

-- The identity type (for propositional equality).

infix 4 _≡_

data _≡_ {A : Set} (m : A) : A → Set where

-- 3.2.1. Direct proof of the associativity of addition using propositional

-- equality.

+-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

+-associative (suc m) n p = cong suc (+-associative m n p)

-- Proof _of_ mathematical induction on the natural numbers.

-- P 0, ∀ x. P x → P (suc x) | ∀ x. P x.

ind P P₀ next (suc n) = next n (ind P P₀ next n)

-- 3.2.2. The associativity of addition by induction (with propositional

-- equality, again).

+-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

+-associative′ m n p = ind P P₀ is m

P : ℕ → Set

P m = m + n + p ≡ m + (n + p)

P₀ = refl

is _ Pi = cong suc Pi

-- Some helper proofs.

m+0≡m (suc m) = cong suc (m+0≡m m)

m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)

-- 3.3. The commutativity of addition using equational reasoning.

+-commutative : (m n : ℕ) → m + n ≡ n + m

+-commutative (suc m) n =

begin

~⟨ refl ⟩

~⟨ cong suc (+-commutative m n) ⟩

~⟨ sym (m+1+n≡1+m+n n m) ⟩

∎

-- 3.4.

even+even≡odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ+1 (m + n)

-- ^

-- That gives

-- ?0 : 2×ℕ+1 (zero + zero)

-- but 2×ℕ+1 (zero + zero) = 2×ℕ+1 0 which is uninhabited, so that this proof

-- can not be writen.

-- The absurd (obviously uninhabited) type.

-- ⊥-introduction is empty.

data ⊥ : Set where

-- The negation of a proposition.

infix 6 ¬_

¬_ : Set → Set

-- 4.1. Disproof or proof by contradiction.

-- To disprove even+even≡odd we assume that even+even≡odd and derive

-- absurdity, i.e. uninhabited type.

even+even≢odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ+1 (m + n)

-- 4.2.

-- even+even≢even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ (m + n)

-- even+even≢even zero zero ()

-- ^

-- rejected with the following message:

-- 2×ℕ zero should be empty, but the following constructor patterns

-- are valid: