Zulip Chat Archive

Stream: Codewars

Topic: easy fermat


view this post on Zulip Sam Lichtenstein (May 17 2020 at 04:14):

not sure if this type of beginner question belongs here or in #new members -- feel free to tell me to move it.

While working on the Easy Fermat kata I got stuck at on an embarrassingly simple point:

import tactic data.zmod.basic
-- (I am not sure whether I need to open these namespaces or not, but that doesn't seem essential to my question here)
open nat zmod

lemma dumb (a : ) :
  3  a  (a : zmod 3) = 0 :=
begin
split,
{ intro h, cases h with c h, finish, },
{ intro h, fconstructor, from a, ring, hint, sorry,
},
end

Set aside the kata itself. I assume it probably can be done without using zmod at all if one were so inclined. I wanted to use the field zmod 3 so that I could invoke facts like the following:

lemma foo (a b : ) :
  3  a * b  a % 3 = 0  b % 3 = 0 := sorry

which I intended to prove by convincing Lean that this is definitionally equivalent to Z/3 being an integral domain, then invoking the fact that zmod 3 is a field because 3 is prime (by norm_num) and then applying some lemma from the algebra library to the effect that any field is a domain.

Returning to lemma dumb above, I got stuck at the sorry when no hint was available. Perhaps a useful starting point would be to understand why the current tactic state seems to have lost the information of what type a : ℕ is being upcast to (namely zmod 3) in the goal ⊢ ↑a = 0 → 3 ∣ a, when it would seem to me that information is crucial. (My suspicion is that the information hasn't actually been lost, it's just not being printed for some reason, perhaps because usually having all the casts explicit would add too much clutter to be useful.)

Even though I managed to prove the ⊢ 3 ∣ a → ↑a = 0 branch of lemma dumb using finish, I'm not happy with my understanding of that branch either. For one thing, even though finish worked to close the goal, simp did not (so squeeze_simp wasn't helpful). Perhaps I am wrong about this, but I inferred from this that in this case finish must be doing some complicated thing I don't understand involving ematch and congruence closure, whatever those are, which it falls back on when simp fails.

Can someone point me towards enlightenment when it comes to understanding the proof of lemma dumb?

view this post on Zulip Sam Lichtenstein (May 17 2020 at 04:22):

perhaps my mistake above is thinking that writing (a : zmod 3) is the right way to apply the map ℕ ↪ ℤ ↠ ℤ/3ℤ?

view this post on Zulip Alex J. Best (May 17 2020 at 04:28):

I'm not sure if you need more files imported or not, but library_search finds the right lemma for me to make the proof

rw (char_p.cast_eq_zero_iff (zmod 3) 3 a),

I'm using a pretty recent mathlib also.

view this post on Zulip Sam Lichtenstein (May 17 2020 at 04:32):

oh, that's helpful! facepalm for not trying library_search (which is apparently smarter than I'd naively thought it was)

view this post on Zulip Sam Lichtenstein (May 17 2020 at 04:33):

thank you!

view this post on Zulip Kevin Buzzard (May 17 2020 at 08:20):

The general rule is that if it is a natural statement which looks like it might be useful to people other than you, it should be in the library.

view this post on Zulip Jalex Stark (May 17 2020 at 13:19):

(there's :face_palm: by the way)

view this post on Zulip Sam Lichtenstein (May 17 2020 at 16:32):

Why does the following work

variables (p : ) [fact p.prime]
lemma zmodp_domain (a b : (zmod p)) :
    a * b = 0  a = 0  b = 0 :=
begin
exact mul_eq_zero,
end

but not this special case:

lemma zmod3_domain (a b : zmod 3) :
    a * b = 0  a = 0  b = 0 :=
begin
have : fact (3:).prime := by norm_num,
exact mul_eq_zero, -- fails
end

view this post on Zulip Johan Commelin (May 17 2020 at 16:35):

You need haveI

view this post on Zulip Johan Commelin (May 17 2020 at 16:36):

It's unfortunate, but new assumptions are not automatically added to the "instance cache"

view this post on Zulip Johan Commelin (May 17 2020 at 16:36):

Alternatively, write resetI between the have and exact lines

view this post on Zulip Sam Lichtenstein (May 17 2020 at 16:36):

ah, thank you. is there a section in one of the standard references (TPIL &c) that explains haveI and related things?

view this post on Zulip Johan Commelin (May 17 2020 at 16:36):

No, because they're mathlib only, I think

view this post on Zulip Johan Commelin (May 17 2020 at 16:37):

But the mathlib docs might have a section on them

view this post on Zulip Johan Commelin (May 17 2020 at 16:37):

Reading through the "tactics" chapter of the mathlib docs is very much recommended

view this post on Zulip Johan Commelin (May 17 2020 at 16:38):

But haveI is just have + reset instance cache. Similar for letI and exactI

view this post on Zulip Sam Lichtenstein (May 17 2020 at 16:38):

got it, thx\

view this post on Zulip Sam Lichtenstein (May 17 2020 at 16:39):

I suppose a natural question is: if Lean doesn't automatically reset the instance cache because it causes performance problems, do people try to avoid using resetI for the same reason?

view this post on Zulip Johan Commelin (May 17 2020 at 16:42):

Nope, just use it whenever you need it

view this post on Zulip Johan Commelin (May 17 2020 at 16:42):

But only 1 out of 10 proofs need it (just some random guess)

view this post on Zulip Jalex Stark (May 17 2020 at 19:32):

https://leanprover-community.github.io/mathlib_docs/tactics.html#Instance%20cache%20tactics


Last updated: May 08 2021 at 23:10 UTC