Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 30 2018 at 14:13):

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

view this post on Zulip cbailey (Aug 30 2018 at 14:15):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Aug 30 2018 at 14:20):

I think Lean does not have Omega yet.

view this post on Zulip Johan Commelin (Aug 30 2018 at 14:20):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Aug 30 2018 at 14:32):

(I didn't implement counterexamples yet.)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 30 2018 at 14:40):

@Kevin Buzzard done

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 30 2018 at 15:10):

ah!!! you did zmod

view this post on Zulip Kenny Lau (Aug 30 2018 at 15:10):

I was reducing it to nat instead

view this post on Zulip 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.

view this post on Zulip 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