Last active
June 7, 2020 15:28
-
-
Save sjkillen/7ca7cab883264d787616a998f4674281 to your computer and use it in GitHub Desktop.
ℕ = ℕ is decidable
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open nat | |
/-- | |
Decide whether two natural numbers are equal | |
(already included in LEAN standard lib) | |
-/ | |
lemma eq_iff_succ_eq {a b : ℕ} : a = b <-> a+1 = b+1 := | |
begin | |
split, | |
-- ==> | |
assume ab_eq : a = b, | |
rw ab_eq, | |
-- <== | |
assume ab_eq : a.succ = b.succ, | |
have j : Π (n : ℕ), n = n+1-1, | |
from λ (n : ℕ), eq.refl n, | |
rw [j a, ab_eq, <-j b], | |
end | |
theorem decide_nat_eq : Π (n m : ℕ), decidable (n = m) | |
| zero zero := decidable.is_true (eq.refl zero) | |
| nat.zero (succ x) := begin | |
have h : ¬(zero = (succ x)) := begin apply nat.no_confusion, end, | |
exact decidable.is_false h, | |
end | |
| (succ x) nat.zero := begin | |
have h : ¬((succ x) = zero) := begin apply nat.no_confusion, end, | |
exact decidable.is_false h, | |
end | |
| (nat.succ dn) (nat.succ dm) := begin | |
have h : decidable (dn = dm), from decide_nat_eq dn dm, | |
rw eq_iff_succ_eq at h, | |
exact h, | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment