## Stream: Codewars

### Topic: easy fermat

#### 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?

#### 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ℤ?

#### 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.

#### 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)

thank you!

#### 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.

#### Jalex Stark (May 17 2020 at 13:19):

(there's :face_palm: by the way)

#### 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


#### Johan Commelin (May 17 2020 at 16:35):

You need haveI

#### Johan Commelin (May 17 2020 at 16:36):

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

#### Johan Commelin (May 17 2020 at 16:36):

Alternatively, write resetI between the have and exact lines

#### 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?

#### Johan Commelin (May 17 2020 at 16:36):

No, because they're mathlib only, I think

#### Johan Commelin (May 17 2020 at 16:37):

But the mathlib docs might have a section on them

#### Johan Commelin (May 17 2020 at 16:37):

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

#### Johan Commelin (May 17 2020 at 16:38):

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

got it, thx\

#### 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?

#### Johan Commelin (May 17 2020 at 16:42):

Nope, just use it whenever you need it

#### Johan Commelin (May 17 2020 at 16:42):

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

#### 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