Coercions in integer exponents

Stream: Is there code for X?

[Ashley Blacquiere]

I'm trying to port parts of cryptolib to Lean 4, specifically the proof of bijection between ZMod q and a the subgroup generated by a generator g raised to a power of ZMod q. This is what I have so far:

import Mathlib

variable {G: Type*} [Fintype G] [Group G] [DecidableEq G] [IsCyclic G]
variable (q : ℕ) [Fact (Nat.Prime q)]
variable (G_card_q : Fintype.card G = q)
variable (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)

include G_card_q
include g_gen_G

lemma exp_bij : Function.Bijective fun (z : ZMod q) => g^z.val := by
  apply (Fintype.bijective_iff_surjective_and_card _).mpr
  have h_prime : q.Prime := Fact.out
  have h_card : g ^ q = 1 := by
    rw [←G_card_q]
    apply pow_card_eq_one
  simp [h_card, G_card_q]
  intro y
  obtain ⟨k, hk⟩ := g_gen_G y
  use k
  have h_pow : g^((k : ZMod q).val) = y := by
    subst hk G_card_q
    simp_all only [pow_card_eq_one, zpow_mod_card]
    sorry
  exact h_pow

I'm stuck at the sorry where the goal state is g ^ (↑k).val = g ^ k, but I can't figure out how to either compare the exponents directly (I thought of using docs#zpow_eq_zpow_iff_modEq) or to otherwise manage the coercion. I've tried Loogle, Moogle and LeanSearch, but can't find a solution...

[Kim Morrison]

Looking at your sorry, I started writing ZMod.val_intCast, which seemed to be the missing lemma, only to find it already exists but seemingly says the wrong thing.

It is:

ZMod.val_intCast {n : ℕ} (a : ℤ) [NeZero n] : ↑(a : ZMod n).val = a % ↑n

i.e. it says something not about (a : ZMod n).val, but the coercion of that back to \Int. Not very helpful!

I think it should probably instead say

theorem val_intCast {n : ℕ} (a : ℤ) [NeZero n] : (a : ZMod n).val = Int.natMod a n

and probably also be a simp lemma.

[Kim Morrison]

i.e. something like

@[simp] theorem intCast_natMod (a b : Int) [NeZero b] : (a.natMod b : Int) = a % b := by
  simpa [Int.natMod] using Int.emod_nonneg _ (NeZero.ne b)

@[simp] theorem ZMod.val_intCast' {n : ℕ} (a : ℤ) [NeZero n] : (a : ZMod n).val = Int.natMod a n := by
  apply Int.ofNat.inj
  simp only [Int.ofNat_eq_coe]
  rw [ZMod.val_intCast]
  simp

[Kim Morrison]

There's a lot of API around natMod missing too, I'm not sure when/who added it.

[Kim Morrison]

Also natMod has terrible behaviour at e.g. Int.natMod (-37) 0 = 0, where I think 37 would be more consistent with other division-by-zero behaviour.

[Kim Morrison]

Hmm, I guess that is equally terrible. It seems all theorems about natMod are probably going to need a b \ne 0 hypothesis.

[Kim Morrison]

In any case, you'll want

theorem Int.natMod_eq_sub (x w : Int) (h : w ≠ 0) : Int.natMod x w = x - w * (x / w) := by
  plausible

[Bhavik Mehta]

Kim Morrison said:

There's a lot of API around natMod missing too, I'm not sure when/who added it.

I decided to figure this out out of curiosity - looks like it was added here: https://github.com/leanprover-community/lean/commit/e705d8949002481a118003ea5bee2098226dbd22#diff-28df10e2dbc2fa18af1293c5145788c9983f7e892038b18717a1a80862e976b9R444