## Stream: maths

### Topic: 0<=d<3 implies d=0,1,2

#### Kevin Buzzard (Aug 30 2018 at 14:09):

theorem easy (d : ℤ) : 0 ≤ d ∧ d < 3 → d = 0 ∨ d = 1 ∨ d = 2 := sorry


I can prove this by cases on d but it's a bit horrible. Is there a tactic which does this painlessly?

#### Kevin Buzzard (Aug 30 2018 at 14:13):

aargh an undergrad just told me that they need this mod 8 :-/

#### cbailey (Aug 30 2018 at 14:15):

If Lean has Omega, that will definitely take care of the original one by itself.

#### Kevin Buzzard (Aug 30 2018 at 14:16):

Apparently what they actually need is example (d : ℤ) : d ^ 2 ≡ 0 [ZMOD 8] ∨ d ^ 2 ≡ 1 [ZMOD 8] ∨ d ^ 2 ≡ 4 [ZMOD 8] := sorry

#### Kevin Buzzard (Aug 30 2018 at 14:17):

which can done by cases on d mod 8 (check it's true for all 8 values)

#### Kevin Buzzard (Aug 30 2018 at 14:18):

(and use the fact that a ≡ b [ZMOD 8] -> a ^ 2 ≡ b ^ 2[ZMOD 8]. @Chris Hughes how far is this from dec_trivial?

#### Johan Commelin (Aug 30 2018 at 14:19):

Would the original one be something that linarith could do? I have no good feeling for this yet...

#### Kevin Buzzard (Aug 30 2018 at 14:20):

I think Lean does not have Omega yet.

#### Johan Commelin (Aug 30 2018 at 14:20):

But it has linarith (but not on my laptop, because compiling Lean takes forever...)

#### Kenny Lau (Aug 30 2018 at 14:21):

import data.int.basic

theorem easy (d : ℤ) : 0 ≤ d ∧ d < 3 → d = 0 ∨ d = 1 ∨ d = 2 :=
begin
intro H,
cases H with H1 H2,
cases d,
{ replace H2 := int.lt_of_coe_nat_lt_coe_nat H2,
clear H1, revert d, from dec_trivial },
exfalso,
exact H1
end


#### Rob Lewis (Aug 30 2018 at 14:21):

No, linarith won't work for a few reasons. In particular, it's only complete for dense orders.

#### Rob Lewis (Aug 30 2018 at 14:21):

It's also not set up to handle disjunctions or proving equality goals right now, although in principle that can happen.

#### Johan Commelin (Aug 30 2018 at 14:29):

No, linarith won't work for a few reasons. In particular, it's only complete for dense orders.

What is a dense order? You had examples with int right?

#### Kenny Lau (Aug 30 2018 at 14:31):

a dense order is one such that for every a and b there is c with a<c<b

#### Rob Lewis (Aug 30 2018 at 14:31):

Something like ∀ x y, x < y → ∃ z, x < z ∧ y < z. It will work on many problems in int, but it isn't complete, meaning there are provable things it will fail on.

#### Rob Lewis (Aug 30 2018 at 14:32):

In theory, over real or rat it will either succeed with a proof or fail with a counterexample.

#### Rob Lewis (Aug 30 2018 at 14:32):

(I didn't implement counterexamples yet.)

#### Johan Commelin (Aug 30 2018 at 14:40):

Right, so dense orders are what I thought they were. And int is not a dense order. So every time linarith succeeds on int we are just being lucky?

#### Kenny Lau (Aug 30 2018 at 14:40):

import data.int.modeq

lemma why_isnt_this_in_mathlib (a b c : ℕ) :
(a * b) % c = (a % c) * (b % c) % c :=
begin
conv in ((a * b) % c) { rw ← nat.mod_add_div a c },
conv in ((_ * b) % c) { rw ← nat.mod_add_div b c },
rw [mul_assoc, mul_assoc],
rw [mul_left_comm (a%c)],
end

example (d : ℤ) : d * d ≡ 0 [ZMOD 8] ∨ d * d ≡ 1 [ZMOD 8] ∨ d * d ≡ 4 [ZMOD 8] :=
begin
rw ← int.nat_abs_mul_self,
generalize : int.nat_abs d = n,
clear d,
change ↑(n * n) ≡ ↑0 [ZMOD ↑8] ∨ ↑(n * n) ≡ ↑1 [ZMOD ↑8] ∨ ↑(n * n) ≡ ↑4 [ZMOD ↑8],
rw int.modeq.coe_nat_modeq_iff,
rw int.modeq.coe_nat_modeq_iff,
rw int.modeq.coe_nat_modeq_iff,
unfold nat.modeq,
rw why_isnt_this_in_mathlib n n,
generalize H : n % 8 = k,
have H1 : k < 8,
{ rw ← H, from nat.mod_lt _ dec_trivial },
clear H n,
revert H1 k,
exact dec_trivial
end


#### Kenny Lau (Aug 30 2018 at 14:40):

@Kevin Buzzard done

#### Rob Lewis (Aug 30 2018 at 14:44):

Right, so dense orders are what I thought they were. And int is not a dense order. So every time linarith succeeds on int we are just being lucky?

Yep. You'll get lucky on any problem that doesn't depend on the discrete-ness of integers.

#### Chris Hughes (Aug 30 2018 at 15:05):

This is my attempt

import data.zmod

example (d : ℤ) : d * d ≡ 0 [ZMOD 8] ∨ d * d ≡ 1 [ZMOD 8] ∨ d * d ≡ 4 [ZMOD 8] :=
have ∀ d : zmod 8, d * d = (0 : ℤ) ∨ d * d = (1 : ℤ) ∨ d * d = (4 : ℤ), from dec_trivial,
by have := this d;
rwa [← int.cast_mul, zmod.eq_iff_modeq_int, zmod.eq_iff_modeq_int, zmod.eq_iff_modeq_int] at this


Although this is not as easy as I'd like it to be.

#### Kenny Lau (Aug 30 2018 at 15:10):

ah!!! you did zmod

#### Kenny Lau (Aug 30 2018 at 15:10):

I was reducing it to nat instead

#### Kevin Buzzard (Aug 30 2018 at 15:37):

Thanks Kenny. I had tried dec_trivial but before applying int.le_of_coe_nat_lt_coe_nat.

#### Kevin Buzzard (Aug 30 2018 at 15:40):

So Chris reduces it to something which is known to be finite. That's another trick. But dec_trivial doesn't work with int? Is this because it could work but there's just some missing code? Is it possible for someone to write some behind-the-scenes code and then after that we have things like example (d : ℤ) : -3 < d ∧ d < 2 → d = -2 ∨ d = -1 ∨ d = 0 ∨ d = 1 := dec_trivial?

Last updated: May 14 2021 at 18:28 UTC