Last active
October 11, 2022 18:30
-
-
Save PhDP/ada06f2f1ea03f704a7aa3a3099729e0 to your computer and use it in GitHub Desktop.
First few problems in the Lean 3 number game.
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
import data.real.basic | |
#check ℝ | |
open nat | |
-- Links: | |
-- * Lean 3's big math library: https://github.com/leanprover-community/mathlib | |
-- * Number game: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ | |
-- * Agda's Unimath library: https://github.com/UniMath/agda-unimath | |
-- * Homotopy Type Theory Game: https://thehottgameguide.readthedocs.io/en/latest/index.html | |
-- Tutorial World 1/4 | |
lemma example' (x y z: ℕ): x * y + z = x * y + z := | |
begin | |
refl, | |
end | |
-- Tutorial World 2/4 | |
lemma example''(x y: ℕ) (h: y = x + 7): 2 * y = 2 * (x + 7) := | |
begin | |
rw h, | |
end | |
-- Tutorial World 3/4 | |
lemma example''' (a b: ℕ) (h: succ a = b): succ (succ a) = succ b := | |
begin | |
rw h, | |
end | |
-- Tutorial World 4/4 | |
lemma add_succ_zero' (a : ℕ) : a + succ 0 = succ a := | |
begin | |
rw nat.add_succ, | |
rw nat.add_zero, | |
end | |
-- Addition World 1/6 | |
lemma zero_add' (n : ℕ) : 0 + n = n := | |
begin | |
induction n with d hd, | |
rw nat.add_zero, | |
rw nat.add_succ, | |
rw hd, | |
end | |
-- Addition World 2/6 | |
lemma add_assoc' (a b c : ℕ) : (a + b) + c = a + (b + c) := | |
begin | |
induction c with d hd, | |
repeat { rw nat.add_zero }, | |
repeat { rw nat.add_succ }, | |
rw hd, | |
end | |
-- Addition World 3/6 | |
lemma succ_add' (a b : ℕ) : succ a + b = succ (a + b) := | |
begin | |
induction b with d hd, | |
repeat { rw nat.add_zero }, | |
repeat { rw nat.add_succ }, | |
rw hd, | |
end | |
-- Addition World 4/6 | |
lemma add_comm' (a b : ℕ) : a + b = b + a := | |
begin | |
induction b with d hd, | |
rw nat.add_zero, | |
rw zero_add', | |
rw nat.add_succ, | |
rw succ_add', | |
rw hd, | |
end | |
-- Addition World 5/6 | |
lemma succ_eq_add_one (n : ℕ) : succ n = n + 1 := | |
begin | |
simp, | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment