0<=d<3 implies d=0,1,2

Stream: maths

[Kevin Buzzard]

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]

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

[cbailey]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

(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]

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

[Kevin Buzzard]

I think Lean does not have Omega yet.

[Johan Commelin]

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

[Kenny Lau]

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]

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

[Rob Lewis]

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

[Johan Commelin]

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]

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

[Rob Lewis]

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]

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

[Rob Lewis]

(I didn't implement counterexamples yet.)

[Johan Commelin]

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]

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]

@Kevin Buzzard done

[Rob Lewis]

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]

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]

ah!!! you did zmod

[Kenny Lau]

I was reducing it to nat instead

[Kevin Buzzard]

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

[Kevin Buzzard]

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?