Need help on a simple proof

Stream: new members

[Kevin Cheung]

I am stuck on the following which seems very simple. Could someone give me a hint or two on how to proceed?

import Mathlib

def f (n k : ℕ+) : Fin n → Fin n := fun m ↦ (m - k) % n

example (n k : ℕ+) : Function.Bijective (f n k) := by
  unfold Function.Bijective
  constructor
  . dsimp [Function.Injective, f]
    intro a b
    intro h
    sorry
  . sorry

EDIT: I can fill out the second sorry but not the first.

[Aaron Liu]

simp is pretty powerful, have you tried simping?

[Kevin Cheung]

It says no progress

[Aaron Liu]

simp at h makes progress for me

[Kevin Cheung]

True. But then the hypothesis now has a couple of % 0. I'm not sure what to do with that.

[Aaron Liu]

Do you know what % 0 means?

[Kevin Cheung]

Basically, a % 0 = a. But using rw [Nat.mod_zero] didn't do anything.

[Aaron Liu]

That's because it's Fin mod, not Nat mod.
docs#Fin.instMod

[Kevin Cheung]

I see. But there seems to be no Fin.mod_zero.

[Aaron Liu]

You can use Fin.mod_def and Nat.mod_zero instead until someone adds a Fin.mod_zero.

[Kevin Cheung]

After Fin.mod_def, I now have h : ⟨↑(a - ↑↑k) % ↑0, ⋯⟩ = ⟨↑(b - ↑↑k) % ↑0, ⋯⟩ in the context. How do I use Nat.mod_zero to simplify the stuff inside the angle brackets? rw couldn't seem to get inside.

[Aaron Liu]

You can simp at h again

[Kevin Cheung]

Thanks!

[Kevin Cheung]

So this is what I now have:

example (n k : ℕ+) : Function.Bijective (f n k) := by
  unfold Function.Bijective
  constructor
  . dsimp [Function.Injective, f]
    intro a b
    intro h
    simp at h
    rw [Fin.mod_def, Fin.mod_def] at h
    simp at h
    assumption
  . dsimp [Function.Surjective, f]
    intro b
    use (b + k)
    apply Fin.eq_of_val_eq
    simp

Seems like a lot of code for something that looks so simple. I wonder if there is a much shorter proof.

[Aaron Liu]

import Mathlib

def f (n k : ℕ+) : Fin n → Fin n := fun m ↦ (m - k) % n

example (n k : ℕ+) : Function.Bijective (f n k) := by
  unfold f
  simp_rw [Fin.natCast_self, Fin.mod_def, Fin.val_zero, Nat.mod_zero, Fin.eta]
  constructor
  · intro a b h
    simp_all
  · intro a
    use a + k
    simp

[Kevin Cheung]

Wow. Thank you.

[suhr]

Another proof:

import Mathlib

def f (n k : ℕ+) : Fin n → Fin n := fun m ↦ (m - k) % n

example (n k : ℕ+) : Function.Bijective (f n k) :=
  Equiv.bijective {
    toFun := f n k
    invFun := λm ↦ (m + k) % n
    left_inv i := by simp [f, Fin.mod_def]
    right_inv i := by simp [f, Fin.mod_def]
  }

Type equivalence is generally nicer than bijections.

[Kevin Cheung]

Thank you.

[Kevin Buzzard]

The proof is long because the formalisation of the statement isn't idiomatic.

[Kevin Cheung]

What would be an idiomatic formulation?

[Kevin Buzzard]

Use ZMod not Fin because you're doing arithmetic not combinatorics. Remove the %n because it doesn't do anything. Let n be a natural not a positive natural. Don't prove it's bijective, make the Equiv.

[Kevin Cheung]

suhr said:

Another proof:

import Mathlib

def f (n k : ℕ+) : Fin n → Fin n := fun m ↦ (m - k) % n

example (n k : ℕ+) : Function.Bijective (f n k) :=
  Equiv.bijective {
    toFun := f n k
    invFun := λm ↦ (m + k) % n
    left_inv i := by simp [f, Fin.mod_def]
    right_inv i := by simp [f, Fin.mod_def]
  }

Type equivalence is generally nicer than bijections.

I don't know why I am getting the error unexpected identifier; expected '}' at left_inv i.

[Kevin Cheung]

The following works though:

example (n k : ℕ+) : Function.Bijective (f n k) :=
  Equiv.bijective {
    toFun := f n k
    invFun := λm ↦ (m + k)
    left_inv := by unfold f; simp [Fin.mod_def]; apply leftInverse_add_left_sub
    right_inv := by refine Function.LeftInverse.rightInverse ?h
                    unfold f; simp [Fin.mod_def]; apply leftInverse_sub_add_left
  }

[suhr]

I don't know why I am getting the error unexpected identifier; expected '}' at left_inv i.

Inconsistent indentation? Anyway, with Kevin's suggestion you can just write

import Mathlib

def iso (n k: Nat): ZMod n ≃ ZMod n where
  toFun m := m - k
  invFun m := m + k
  left_inv m := by simp
  right_inv m := by simp

[Kevin Buzzard]

You can let k be an integer there.