# Zulip Chat Archive

## 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_add, add_mul, add_mul, ← add_assoc], rw [mul_assoc, mul_assoc], rw [nat.add_mul_mod_self_left], rw [mul_left_comm (a%c)], rw [nat.add_mul_mod_self_left], rw [nat.add_mul_mod_self_left] 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