mirror of
https://github.com/SinTan1729/lean-talk-sp24.git
synced 2024-12-26 05:38:37 -06:00
61 lines
1.4 KiB
Text
61 lines
1.4 KiB
Text
import Mathlib.Data.Nat.Basic
|
||
import Mathlib.Data.Nat.Parity
|
||
import Mathlib.Tactic
|
||
|
||
open Nat
|
||
|
||
-- Obligatory Hello World
|
||
#eval "Hello world!"
|
||
|
||
-- These are pieces of data.
|
||
#check 2 + 2
|
||
|
||
def f (x : ℕ) :=
|
||
x + 3
|
||
|
||
#eval f 5
|
||
|
||
#check f
|
||
|
||
-- These are propositions, of type `Prop`.
|
||
#check 2 + 2 = 4
|
||
|
||
def FermatLastTheorem :=
|
||
∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n
|
||
|
||
#check FermatLastTheorem
|
||
|
||
-- These are proofs of propositions.
|
||
theorem easy : 2 + 2 = 4 :=
|
||
rfl
|
||
|
||
#check easy
|
||
|
||
theorem hard : FermatLastTheorem :=
|
||
sorry
|
||
|
||
#check hard
|
||
|
||
-- Here are some proofs.
|
||
example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ =>
|
||
have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
|
||
show ∃ l, m * n = l + l from ⟨_, hmn⟩
|
||
|
||
example : ∀ m n : Nat, Even n → Even (m * n) :=
|
||
fun m n ⟨k, hk⟩ => ⟨m * k, by rw [hk, mul_add]⟩
|
||
|
||
example : ∀ m n : Nat, Even n → Even (m * n) := by
|
||
-- say m and n are natural numbers, and assume n=2*k
|
||
rintro m n ⟨k, hk⟩
|
||
-- We need to prove m*n is twice a natural number. Let's show it's twice m*k.
|
||
use m * k
|
||
-- substitute in for n
|
||
rw [hk]
|
||
-- and now it's obvious
|
||
ring
|
||
|
||
example : ∀ m n : Nat, Even n → Even (m * n) := by
|
||
rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring
|
||
|
||
example : ∀ m n : Nat, Even n → Even (m * n) := by
|
||
intros; simp [*, parity_simps]
|