Concrete cycle notation

Stream: mathlib4

[Yakov Pechersky]

In mathlib3, we have on-the-fly dec_trivial proofs of nodup in the cycle perm notation:

notation `c[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) :=
  cycle.form_perm ↑l (cycle.nodup_coe_iff.mpr dec_trivial)

while in mathlib4, we somehow lost that:

notation3"c["(l", "* => foldr (h t => List.cons h t) List.nil)"]" =>
  Cycle.formPerm (↑l) (Cycle.nodup_coe_iff.mpr _)

The new notation does not work as expected, the c[ lines don't work below, but my cx[ variant does. @Jeremy Tan @Kyle Miller any thoughts on what's going on here (you've edited these lines). There was no porting note.

import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.GroupTheory.SpecificGroups.Dihedral

notation3 "cx["(l", "* => foldr (h t => List.cons h t) List.nil)"]" =>
  Cycle.formPerm (Cycle.ofList l) (by decide)

def foo : DihedralGroup 4 → Equiv.Perm (Fin 4)
    | .r 0 => Equiv.refl _
    | .r 1 => cx[0, 3, 2, 1]
    | .r 2 => cx[0, 2] * cx[1, 3]
    | .r 3 => cx[0, 1, 2, 3]
    | .sr 0 => cx[1, 3]
    | .sr 1 => cx[0, 1] * cx[2, 3]
    | .sr 2 => cx[0, 2]
    | .sr 3 => cx[0, 3] * cx[1, 2]

def bar : DihedralGroup 4 → Equiv.Perm (Fin 4)
    | .r 0 => Equiv.refl _
    | .r 1 => c[0, 3, 2, 1]
    | .r 2 => c[0, 2] * c[1, 3]
    | .r 3 => c[0, 1, 2, 3]
    | .sr 0 => c[1, 3]
    | .sr 1 => c[0, 1] * c[2, 3]
    | .sr 2 => c[0, 2]
    | .sr 3 => c[0, 3] * c[1, 2]

[Mario Carneiro]

I don't think the mathlib4 version looks like your quote

[Mario Carneiro]

notation3 "c["(l", "* => foldr (h t => List.cons h t) List.nil)"]" =>
  Cycle.formPerm (Cycle.ofList l) (Iff.mpr Cycle.nodup_coe_iff _)

[Yakov Pechersky]

Yes, sorry, I copied the line out of the PR. Semantically, it's the same, the coercion is the Cycle.ofList and the Iff.mpr is said explicitly.

[Mario Carneiro]

why doesn't Cycle.formPerm just use an auto param for the second argument? This seems to work:

def formPerm : ∀ (s : Cycle α) (_ : Nodup s := by decide), Equiv.Perm α := ...

notation3 "c["(l", "* => foldr (h t => List.cons h t) List.nil)"]" =>
  Cycle.formPerm (Cycle.ofList l)

#check (c[0, 3, 2, 1] : Equiv.Perm (Fin 4))
-- Cycle.formPerm ↑[0, 3, 2, 1] : Equiv.Perm (Fin 4)

It does not delaborate properly though, Kyle's change was about making it work with the delaborator

[Yakov Pechersky]

I think that pushing the autoParam into the definition makes sense.