9.Β Advanced Multiplication World
Advanced Addition World proved various implications
involving addition, such as x + y = 0 β x = 0 and x + y = x β y = 0.
These lemmas were used to prove basic facts about β€ in β€ World.
In Advanced Multiplication World we prove analogous
facts about multiplication, such as x * y = 1 β x = 1, and
x * y = x β y = 1 (assuming x β 0 in the latter result). This will prepare
us for Divisibility World.
Multiplication World is more complex than Addition World. In the same way, Advanced Multiplication world is more complex than Advanced Addition World. One reason for this is that certain intermediate results are only true under the additional hypothesis that one of the variables is non-zero. This causes some unexpected extra twists.
9.1.Β Level 1: mul_le_mul_right
Let's warm up with an easy one, which works even if t = 0.
theorem mul_le_mul_right (a b t : β) (h : a β€ b) : a * t β€ b * t
My proof:
cases h with d hd use d * t rw [hd, add_mul] rfl
9.2.Β Level 2: mul_left_ne_zero
If you have completed Algorithm World then you can use the contrapose! tactic
here. If not then I'll talk you through a manual approach.
theorem mul_left_ne_zero (a b : β) (h : a * b β 0) : b β 0
9.3.Β Level 3: eq_succ_of_ne_zero
Multiplication usually makes a number bigger, but multiplication by zero can make
it smaller. Thus many lemmas about inequalities and multiplication need the
hypothesis a β 0. Here is a key lemma that enables us to use this hypothesis.
To help us with the proof, we can use the tauto tactic. Click on the tactic's name
on the right to see what it does.
New: tauto
Summary
The tauto tactic will solve any goal which can be solved purely by logic (that is, by
truth tables).
Details
tauto does not do magic! It doesn't know anything about addition or multiplication,
it doesn't even know add_zero. The only things that tauto knows about numbers
are firstly that a = a and secondly that 0 β 1, 0 β 2, 1 β 2 and so on.
What tauto's strength is, is logic. If you have a hypothesis x < 37
and another hypothesis x < 37 β y + z = 42 and your goal is y + z = 42 then tauto will
solve this goal, because to solve that goal you don't need to know any facts
about inequalities or addition, all you need to know is the rules of logic.
Example
If you have False as a hypothesis, then tauto will solve
the goal. This is because a false hypothesis implies any hypothesis.
Example
If your goal is True, then tauto will solve the goal.
Example
If you have two hypotheses h1 : a = 37 and h2 : a β 37 then tauto will
solve the goal because it can prove False from your hypotheses, and thus
prove the goal (as False implies anything).
Example
If you have one hypothesis h : a β a then tauto will solve the goal because
tauto is smart enough to know that a = a is true, which gives the contradiction we seek.
Example
If you have a hypothesis h : 0 = 1 then tauto will solve the goal, because
tauto knows 0 β 1 and this is enough to prove False, which implies any goal.
Example
If you have a hypothesis of the form a = 0 β a * b = 0 and your goal is a * b β 0 β a β 0, then
tauto will solve the goal, because the goal is logically equivalent to the hypothesis.
If you switch the goal and hypothesis in this example, tauto would solve it too.
theorem eq_succ_of_ne_zero (a : β) (ha : a β 0) : β n, a = succ n
9.4.Β Level 4: one_le_of_ne_zero
The previous lemma can be used to prove this one.
theorem one_le_of_ne_zero (a : β) (ha : a β 0) : 1 β€ a
9.5.Β Level 5: le_mul_right
One day this game will have a Prime Number World, with a final boss
of proving that 2 is prime.
To do this, we will have to rule out things like 2 = 37 Γ 42.
We will do this by proving that any factor of 2 is at most 2,
which we will do using this lemma. The proof I have in mind manipulates the hypothesis
until it becomes the goal, using mul_left_ne_zero, one_le_of_ne_zero and
mul_le_mul_right.
theorem le_mul_right (a b : β) (h : a * b β 0) : a β€ a * b
Here's what I was thinking of:
apply mul_left_ne_zero at h apply one_le_of_ne_zero at h apply mul_le_mul_right 1 b a at h rw [one_mul, mul_comm] at h exact h
9.6.Β Level 6: mul_right_eq_one
This level proves x * y = 1 β x = 1, the multiplicative analogue of Advanced Addition
World's x + y = 0 β x = 0. The strategy is to prove that x β€ 1 and then use the
lemma le_one from β€ world.
We'll prove it using a new and very useful tactic called have.
New: have
Summary
The have tactic can be used to add new hypotheses to a level, but of course
you have to prove them.
Example
The simplest usage is like this. If you have a in your context and you execute
have ha : a = 0
then you will get a new goal a = 0 to prove, and after you've proved
it you will have a new hypothesis ha : a = 0 in your original goal.
Example
If you already have a proof of what you want to have, you
can just create it immediately. For example, if you have a and b
number objects, then
have h2 : succ a = succ b β a = b := succ_inj a b
will directly add a new hypothesis h2 : succ a = succ b β a = b
to the context, because you just supplied the proof of it (succ_inj a b).
Example
If you have a proof to hand, then you don't even need to state what you are proving. For example
have h2 := succ_inj a b
will add h2 : succ a = succ b β a = b as a hypothesis.
theorem mul_right_eq_one (x y : β) (h : x * y = 1) : x = 1
9.7.Β Level 7: mul_ne_zero
This level proves that if a β 0 and b β 0 then a * b β 0. One strategy
is to write both a and b as succ of something, deduce that a * b is
also succ of something, and then apply zero_ne_succ.
theorem mul_ne_zero (a b : β) (ha : a β 0) (hb : b β 0) : a * b β 0
9.8.Β Level 8: mul_eq_zero
This level proves that if a * b = 0 then a = 0 or b = 0. It is
logically equivalent to the last level, so there is a very short proof.
theorem mul_eq_zero (a b : β) (h : a * b = 0) : a = 0 β¨ b = 0
Here's the short proof:
have h2 := mul_ne_zero a b tauto
This works because, given mul_ne_zero a b,
the argument is reduced to pure logic.
9.9.Β Level 9: mul_left_cancel
In this level we prove that if a * b = a * c and a β 0 then b = c. It is tricky, for
several reasons. One of these is that
we need to introduce a new idea: we will need to understand the concept of
mathematical induction a little better.
Starting with induction b with d hd is too naive, because in the inductive step
the hypothesis is a * d = a * c β d = c but what we know is a * succ d = a * c,
so the induction hypothesis does not apply!
Assume a β 0 is fixed. The actual statement we want to prove by induction on b is
"for all c, if a * b = a * c then b = c". This can be proved by induction,
because we now have the flexibility to change c.
theorem mul_left_cancel (a b c : β) (ha : a β 0) (h : a * b = a * c) : b = c
9.10.Β Level 10: mul_right_eq_self
The lemma proved in the final level of this world will be helpful in Divisibility World.
theorem mul_right_eq_self (a b : β) (ha : a β 0) (h : a * b = a) : b = 1
A two-line proof is
nth_rewrite 2 [β mul_one a] at h exact mul_left_cancel a b 1 ha h
We now have all the tools necessary to set up the basic theory of divisibility of naturals.