help using ZMOD

Stream: new members

[JK]

I am at a bit of a loss in how to start using ZMOD. How do I unroll the definition? (Using dsimp did not work.)

As an example, how can I prove the following?

Import Mathlib

example : 11 ≡ 3 [ZMOD 4] := by

[JK]

Hmm...ok, I found that exact rfl works, but I would still like to know how I can unroll the definition

[JK]

(How do I delete a previous post?)

[David Renshaw]

I'm not sure whether it's the best way, but I often do something like this:

example : 11 ≡ 3 [ZMOD 4] := by
  change _ % _ = _ % _

[JK]

Now I have the same question for %. E.g., how do I prove

example {a : ℤ} (h : a % 3 = 1) : ∃ k : ℕ, a=3*k+1 := by

[JK]

Putting this here for future reference: use Int.modEq_iff_dvd.

[Kenny Lau]

JK said:

unroll the definition

that's a bad strategy in general

[JK]

In this example:

Import Mathlib

example {a b : ℤ} (ha : a ≡ 4 [ZMOD 5]) (hb : b ≡ 3 [ZMOD 5]) :
    a * b + b ^ 3 + 3 ≡ 2 [ZMOD 5] :=
  calc
    a * b + b ^ 3 + 3 ≡ 4 * b + b ^ 3 + 3 [ZMOD 5] := by rel [ha]
    _ ≡ 4 * 3 + 3 ^ 3 + 3 [ZMOD 5] := by rel [hb]
    _ ≡ 2 + 5 * 8 [ZMOD 5] := by norm_num
    _ ≡ 2 [ZMOD 5] := by norm_num

I am confused why the first instance of norm_num works but the second doesn't.

[Filippo A. E. Nuccio]

(small typo: import in Lean has a small, not capital, I)

The final goal can be closed by rfl: actually, the third also, but norm_num could also work around it. If you hover on norm_num, you'll see a pop-up with the doc ot the tactic: as it says, it normalizes expressions, and this is not what you need to prove that 2+5*8 is congruent to 2 modulo 5: it just boils down to the definition of ZMOD 5, and this is done by rfl. The norm_num on line 3 is packing-and-unpacking the 4*3+3^3+3 and to see what it is actually doing you can replace by norm_num by by show_term{norm_num}. But :warning: : it won't be nice :smiley: .