Help with coercions from N to Z to ZMod

Stream: new members

[Stepan Nesterov]

This is kind of a soft question, because I am unsure whether it's really a problem or if things are supposed to just be hard. I was formalizing the fact that the center of the dihedral group is {1, r^(n/2)} for even n and it was extremely difficult because of all the coercions floating around and simp completely giving up when there is division involved.
Is there a better approach to avoid so many coercions? Should I refer to n / 2 as Classical.choose h instead?

import Mathlib.GroupTheory.Subgroup.Centralizer
import Mathlib.GroupTheory.SpecificGroups.Dihedral

def CentralSymmetryGroup (n : ℕ) (h : Even n) (h' : 0 < n) : Subgroup (DihedralGroup n) where
  carrier := {1, DihedralGroup.r (Int.castRingHom (ZMod n) (n / 2))}
  mul_mem' := by
    simp
    intro a b ha hb
    obtain ha | ha := ha <;> obtain hb | hb := hb
    · left
      rw[ha, hb, mul_one]
    · right
      rw[ha, hb, one_mul]
    · right
      rw[ha, hb, mul_one]
    · left
      rw[ha, hb, DihedralGroup.r_mul_r]
      rcases h with ⟨m, hm⟩
      rw[hm]
      have : ((m : ℤ) + m) / 2 = m := Eq.symm (Int.eq_ediv_of_mul_eq_right (by norm_num) (by ring))
      simp
      rw[this, ← Int.cast_add, ← Int.natCast_add, ←hm]
      simp
  one_mem' := by
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff]
    left
    trivial
  inv_mem' := by
    intro x hx
    simp at *
    obtain hx | hx := hx
    · left
      exact hx
    · right
      rw[hx]
      simp
      rcases h with ⟨m, hm⟩
      rw[hm]
      have : ((m : ℤ) + m) / 2 = m := Eq.symm (Int.eq_ediv_of_mul_eq_right (by norm_num) (by ring))
      simp
      rw[this]
      simp
      rw[ZMod.neg_eq_self_iff ↑↑m]
      right
      rw[two_mul]
      suffices (m : ZMod (m + m)).val = m by rw[this]
      apply ZMod.val_natCast_of_lt
      apply Nat.lt_add_of_pos_right
      linarith


theorem exercise2_2_7b (n : ℕ) (h : Even n) (h' : 2 < n) : Subgroup.center (DihedralGroup n) = CentralSymmetryGroup n h (Nat.zero_lt_of_lt h') := by
  ext x
  constructor <;> intro hyp
  · rw[Subgroup.mem_center_iff] at hyp
    contrapose! hyp
    cases x with
      | r i =>
        use DihedralGroup.sr 0
        simp
        change DihedralGroup.r i ∉ ({1, DihedralGroup.r (Int.castRingHom (ZMod n) (n / 2))} : Set (DihedralGroup n)) at hyp
        simp at hyp
        push_neg at hyp
        obtain ⟨hyp1, hyp2⟩ := hyp
        have hyp1' : i ≠ 0 := by exact fun a => hyp1 (congrArg DihedralGroup.r a)
        intro hi
        symm at hi
        rw[ZMod.neg_eq_self_iff i] at hi
        obtain hi | hi := hi
        contradiction
        have : i.val = n / 2 := Nat.eq_div_of_mul_eq_right (by decide) hi
        have : NeZero n := by exact NeZero.of_gt h'
        have : i = ↑(n / 2) := by
          rw[show i = Nat.cast (i.val) by refine Eq.symm (ZMod.natCast_zmod_val i)]
          congr
        apply hyp2
        rw[this]
        have : ↑(n / 2) = (n : ℤ) / 2 := by exact rfl
        rw[← this]
        exact Eq.symm (AddCommGroupWithOne.intCast_ofNat (n / 2))
      | sr i =>
        use DihedralGroup.r 1
        simp
        rw[sub_eq_add_neg]
        intro hy
        apply add_left_cancel at hy
        have : Fact (2 < n) := { out := h' }
        revert hy
        exact ZMod.neg_one_ne_one
  · rw[Subgroup.mem_center_iff]
    intro g
    simp at hyp
    change x ∈ ({1, DihedralGroup.r (Int.castRingHom (ZMod n) (n / 2))} : Set (DihedralGroup n)) at hyp
    simp at hyp
    obtain hyp | hyp := hyp
    rw[hyp, one_mul, mul_one]
    cases g with
      | r i =>
        rw[hyp]
        simp
        rw[add_comm]
      | sr i =>
        rw[hyp]
        simp
        suffices ((Int.cast ((n : ℤ) / 2)) : ZMod n) = -((Int.cast ((n : ℤ) / 2)) : ZMod n) by nth_rewrite 1 [this]; ring
        rw[eq_neg_iff_add_eq_zero, ← Int.cast_add]
        rw[ZMod.intCast_zmod_eq_zero_iff_dvd]
        use 1
        simp
        have : ((n : ℤ) + n) / 2 = n := Eq.symm (Int.eq_ediv_of_mul_eq_right (by norm_num) (by ring))
        nth_rewrite 3 [← this]
        apply Int.eq_ediv_of_mul_eq_right (by decide)
        rw[mul_add]
        suffices 2 * ((n : ℤ) / 2) = n by rw[this]
        apply Int.two_mul_ediv_two_of_even
        rcases h with ⟨m, hm⟩
        use m
        rw[hm]
        simp

[Yongxi Lin (Aaron)]

Have you tried the norm_cast tactic?

[Eric Paul]

I think you would also have an easier time working with 2*n for any n instead of assuming you have an even n. This way you don't have to worry about division.

import Mathlib.GroupTheory.Subgroup.Centralizer
import Mathlib.GroupTheory.SpecificGroups.Dihedral

def CentralSymmetryGroup (n : ℕ) : Subgroup (DihedralGroup (2*n)) := sorry
theorem exercise2_2_7b (n : ℕ) : Subgroup.center (DihedralGroup (2*n)) = CentralSymmetryGroup n := sorry