106 lines
3.7 KiB
Plaintext
106 lines
3.7 KiB
Plaintext
## Algorithm world
|
|
|
|
Optional. Learn about automating proofs with `simp` and/or `ac_rfl`.
|
|
|
|
Note : `add_add_add_comm` is needed for isEven_add_isEven
|
|
and also in power world with pow_add I think it was,
|
|
and also if you choose a lousy variable
|
|
to induct on in one of mul_add/add_mul (the
|
|
one you don't prove via comm)
|
|
|
|
Where does a reduction tactic which turns all numerals
|
|
into succ succ succ 0 live? Here or functional program world?
|
|
|
|
**TODO** Aesop levels. Tutorial about how to get aesop proving...something.
|
|
|
|
## Functional program world
|
|
|
|
After advanced addition world (because here they learn `apply`).
|
|
Prove succ_ne_zero and succ_inj, and make decidable equality.
|
|
Give proof that 20+20!=41 (note that 2+2!=5 )
|
|
**TODO** find Testa post explaining how to do this.
|
|
|
|
## Inequality world:
|
|
|
|
a) 0 ≤ x;
|
|
b) x ≤ x;
|
|
c) x ≤ S(x);
|
|
d) If x ≤ 0 then x = 0.
|
|
a) x ≤ x (reflexivity);
|
|
b) If x ≤ y and y ≤ z then x ≤ z (transitivity);
|
|
c) If x ≤ y and y ≤ x then x = y (antisymmetry);
|
|
d) Either x ≤ y or y ≤ x (totality).
|
|
|
|
What about succ m ≤ succ n ↔ m ≤ n? This was a lost level (but not about <)
|
|
|
|
If a ≤ b then a + x ≤ b + x. And iff version?
|
|
|
|
## Advanced Multiplication world: you can cancel multiplication
|
|
by nonzero x. ad+bc=ac+bd -> a=b or c=d? This should be preparation
|
|
for divisibility world.
|
|
|
|
## Divisibility world
|
|
|
|
a | b and b | c -> a | c
|
|
a | x and a | y -> a | x + y
|
|
a | x -> a | x * y
|
|
|
|
etc
|
|
|
|
## Prime world
|
|
|
|
2 is prime and that's it
|
|
|
|
## Hard world
|
|
|
|
twin prime, Goldbach, weak Goldbach, 3n+1.
|
|
|
|
## Even/Odd world
|
|
|
|
even + odd = odd etc
|
|
everything is odd or even
|
|
nothing is odd and even
|
|
|
|
## `<` world
|
|
|
|
Advanced inequality world should be `<` and strong induction. Nick from Lean 3 version.
|
|
Define a < b to be S(a)<=b
|
|
|
|
and given NNG3 levels 15 and 16 it should now just
|
|
be a few lines to prove `a < b ↔ `a ≤ b ∧ ¬ (b ≤ a)`,
|
|
|
|
lemma lt_irrefl (a : mynat) : ¬ (a < a) :=
|
|
lemma ne_of_lt (a b : mynat) : a < b → a ≠ b :=
|
|
-- theorem ne_zero_of_pos (a : mynat) : 0 < a → a ≠ 0 :=
|
|
theorem not_lt_zero (a : mynat) : ¬(a < 0) :=
|
|
theorem lt_of_lt_of_le (a b c : mynat) : a < b → b ≤ c → a < c :=
|
|
theorem lt_of_le_of_lt (a b c : mynat) : a ≤ b → b < c → a < c :=
|
|
theorem lt_trans (a b c : mynat) : a < b → b < c → a < c :=
|
|
theorem lt_iff_le_and_ne (a b : mynat) : a < b ↔ a ≤ b ∧ a ≠ b :=
|
|
theorem lt_succ_self (n : mynat) : n < succ n :=
|
|
lemma succ_le_succ_iff (m n : mynat) : succ m ≤ succ n ↔ m ≤ n :=
|
|
lemma lt_succ_iff_le (m n : mynat) : m < succ n ↔ m ≤ n :=
|
|
lemma le_of_add_le_add_left (a b c : mynat) : a + b ≤ a + c → b ≤ c :=
|
|
lemma lt_of_add_lt_add_left (a b c : mynat) : a + b < a + c → b < c :=
|
|
-- I SHOULD TEACH CONGR
|
|
lemma add_lt_add_right (a b : mynat) : a < b → ∀ c : mynat, a + c < b + c :=
|
|
instance : ordered_comm_monoid mynat :=
|
|
instance : ordered_cancel_comm_monoid mynat :=
|
|
def succ_lt_succ_iff (a b : mynat) : succ a < succ b ↔ a < b :=
|
|
-- multiplication
|
|
theorem mul_le_mul_of_nonneg_left (a b c : mynat) : a ≤ b → 0 ≤ c → c * a ≤ c * b :=
|
|
theorem mul_le_mul_of_nonneg_right (a b c : mynat) : a ≤ b → 0 ≤ c → a * c ≤ b * c :=
|
|
theorem mul_lt_mul_of_pos_left (a b c : mynat) : a < b → 0 < c → c * a < c * b :=
|
|
theorem mul_lt_mul_of_pos_right (a b c : mynat) : a < b → 0 < c → a * c < b * c :=
|
|
instance : ordered_semiring mynat :=
|
|
lemma le_mul (a b c d : mynat) : a ≤ b → c ≤ d → a * c ≤ b * d :=
|
|
lemma pow_le (m n a : mynat) : m ≤ n → m ^ a ≤ n ^ a :=
|
|
lemma strong_induction_aux (P : mynat → Prop)
|
|
(IH : ∀ m : mynat, (∀ b : mynat, b < m → P b) → P m)
|
|
(n : mynat) : ∀ c < n, P c :=
|
|
-- is elab_as_eliminator right?
|
|
@[elab_as_eliminator]
|
|
theorem strong_induction (P : mynat → Prop)
|
|
(IH : ∀ m : mynat, (∀ d : mynat, d < m → P d) → P m) :
|
|
∀ n, P n :=
|