Proof: Difference between revisions
Content added Content deleted
mNo edit summary |
mNo edit summary |
||
| Line 124: | Line 124: | ||
-- P 0, ∀ x. P x → P (1 + x) | ∀ x. P x. |
-- P 0, ∀ x. P x → P (1 + x) | ∀ x. P x. |
||
-- |
-- |
||
ind : (P : ℕ → Set) → P 0 → ( |
ind : (P : ℕ → Set) → P 0 → ((m : ℕ) → P m → P (1 + m)) → (m : ℕ) → P m |
||
ind _ P₀ _ 0 = P₀ |
ind _ P₀ _ 0 = P₀ |
||
ind P P₀ next (1+ n) = next n (ind P P₀ next n) |
ind P P₀ next (1+ n) = next n (ind P P₀ next n) |
||
| Line 195: | Line 195: | ||
-- 4.1. Disproof or proof by contradiction. |
-- 4.1. Disproof or proof by contradiction. |
||
-- |
-- |
||
-- To disprove even+even≡odd we assume that even+even≡odd and derive |
-- To disprove even+even≡odd we assume that even+even≡odd and derive |
||
-- i.e. uninhabited type. |
-- absurdity, i.e. uninhabited type. |
||
-- |
-- |
||
even+even≢odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ+1 (m + n) |
even+even≢odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ+1 (m + n) |
||
| Line 205: | Line 205: | ||
=={{header|Coq}}== |
=={{header|Coq}}== |
||
1.1., 1.2, 2.1. and 3.1: |
1.1., 1.2., 2.1. and 3.1.: |
||
<lang coq>Inductive nat : Set := |
<lang coq>Inductive nat : Set := |
||