Division in `ZMod p`?

Stream: new members

[Quang Dao]

Is there a tactic besides native_decide that help me prove computations in ZMod p that involves division?

example : (1 : ZMod 29) / 2 = 15 := by sorry

I tried decide, norm_num, reduce_mod_char, grind, simp +arith +decide, ring, etc, but none of them work. Why is that?

[Ruben Van de Velde]

What does it mean to divide in ZMod p?

[Quang Dao]

It is defined as a * b⁻¹. So this reduces to why can't we easily compute inverse. And note that ZMod.inv is defined by way of extended GCD, i.e. Nat.xgcd

[Aaron Liu]

I'm worried

import Mathlib

/-
failed to synthesize
  HDiv (ZMod 29) (ZMod 29) ?m.1006

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
example : ((1 : ZMod 29) / (2 : ZMod 29) : ZMod 29) = (15 : ZMod 29) := by decide +kernel

that shouldn't happen, right? (on the web server)

[Quang Dao]

You need to first prove [Fact (Nat.Prime 29)], via decide for instance

[Quang Dao]

Here's what happens for decide:

tactic 'decide' failed for proposition
  1 / 2 = 15
since its 'Decidable' instance
  ZMod.decidableEq 29 (1 / 2) 15
did not reduce to 'isTrue' or 'isFalse'.

Reduction got stuck at the 'Decidable' instance
  match h : (↑(1 / 2)).beq ↑15 with
  | true => isTrue ⋯
  | false => isFalse ⋯

[Ruben Van de Velde]

import Mathlib
example : (1 : ZMod 29) * 2⁻¹ = 15 := by
  norm_num
  apply ZMod.inv_eq_of_mul_eq_one
  norm_num
  rfl

Looks like there's room for impovement

[Aaron Liu]

Did they get rid of the inv when p is not prime?

[Quang Dao]

No, there is always ZMod.inv and it gives junk values when (i : ZMod p) is not coprime to p. It's just that you can't access division or inversion notation when p is not prime

[Ruben Van de Velde]

Inv and the inversion notation are always defined

[Quang Dao]

Sorry, yes, only division notation is disallowed

[Quang Dao]

What would it take to extend current tactics to cover this example?