easy fermat

Stream: Codewars

[Sam Lichtenstein]

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?

[Sam Lichtenstein]

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

[Alex J. Best]

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.

[Sam Lichtenstein]

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

[Sam Lichtenstein]

thank you!

[Kevin Buzzard]

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.

[Jalex Stark]

(there's :face_palm: by the way)

[Sam Lichtenstein]

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

[Johan Commelin]

You need haveI

[Johan Commelin]

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

[Johan Commelin]

Alternatively, write resetI between the have and exact lines

[Sam Lichtenstein]

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

[Johan Commelin]

No, because they're mathlib only, I think

[Johan Commelin]

But the mathlib docs might have a section on them

[Johan Commelin]

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

[Johan Commelin]

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

[Sam Lichtenstein]

got it, thx\

[Sam Lichtenstein]

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?

[Johan Commelin]

Nope, just use it whenever you need it

[Johan Commelin]

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

[Jalex Stark]

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