35.7. The Mathlib correspondence🔗

HexPermGroupTheory lets a Mathlib user prove facts about a subgroup of Equiv.Perm (Fin n) generated by explicit permutations. The perm_group tactic proves the order of such a subgroup, that a given permutation does or does not lie in it, and that it is the whole symmetric group. Here M11 is the subgroup generated by the two permutations of the introduction:

def M11 : Subgroup (Equiv.Perm (Fin 11)) :=
  Subgroup.closure
    {c[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10],
      c[2, 6, 10, 7] * c[3, 9, 4, 5]}

example : Nat.card M11 = 7920 := by⊢ Nat.card ↥M11 = 7920
  perm_groupAll goals completed! 🐙

example : c[0, 1] ∉ M11 := by⊢ (↑[0, 1]).formPerm ⋯ ∉ M11
  perm_groupAll goals completed! 🐙

example : Subgroup.closure
    ({c[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], c[0, 1]} :
      Set (Equiv.Perm (Fin 11))) = ⊤ := by⊢ Subgroup.closure {(↑[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10]).formPerm ⋯, (↑[0, 1]).formPerm ⋯} = ⊤
  perm_groupAll goals completed! 🐙

Since M11 is transitive on ordered pairs of points, any transposition in it would be conjugate in it to c[0, 1], so the second example shows that M11 contains no transposition. The third shows that an 11-cycle and a transposition of two adjacent points of the cycle generate the symmetric group on 11 points.

Behind the tactic are theorems relating each computation to the subgroup of Equiv.Perm (Fin n) generated by the same permutations, written Hex.PermGroup.closure of the array of generators. Hex.PermGroup.Group.order_card states that the order of a group is Nat.card of that subgroup, and Hex.PermGroup.Group.contains_spec relates membership:

theorem

Hex.PermGroup.Group.contains_spec {n : ℕ} (G : Hex.PermGroup.Group n)
  (p : Hex.Perm n) :
  G.contains p = true ↔ p.toEquiv ∈ Hex.PermGroup.closure G.generators
Hex.PermGroup.Group.contains_spec {n : ℕ}
  (G : Hex.PermGroup.Group n)
  (p : Hex.Perm n) :
  G.contains p = true ↔
    p.toEquiv ∈
      Hex.PermGroup.closure G.generators

Membership and exact order of a checked computational group agree with its Mathlib subgroup, using the original generator presentation.

These theorems hold for every input. The theorems cited in earlier sections from HexPermGroupTheory, such as Hex.PermGroup.Group.blocks_spec and Hex.PermGroup.Group.sample_uniform, translate other computations in the same way.

35.7.1. How `perm_group` works🔗

Applying Hex.PermGroup.Group.order_card to a particular group requires Lean to evaluate Hex.PermGroup.Group.ofGenerators during type checking, and evaluation there is far slower than running compiled code. The perm_group tactic instead builds a Hex.PermGroup.Kernel.Certificate in compiled code, which is cheap to check. It is a stabilizer chain of its own: the first level's generators are the distinct input permutations other than the identity, and each later level's are a few products of Schreier generators of the level above that already generate the stabilizer, usually two or three, so the check has few Schreier generators to reduce. The certificate keeps only the levels whose orbit has more than one point. Each level stores its base point, its generators, its orbit, the representatives and their inverses, and enough bookkeeping to recompute the representatives from the generators. Every permutation is written as a single natural number, with the image of each point in a fixed number of bits. For M11 there are four levels left, with orbits of 11, 10, 9 and 8 points:

open Hex Hex.PermGroup in
def m11Certificate : Kernel.Certificate :=
  let S : Array (Perm 11) :=
    #[Perm.ofEquiv c[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10],
      Perm.ofEquiv (c[2, 6, 10, 7] * c[3, 9, 4, 5])]
  match Kernel.certify S with
  | .ok c => c
  | .error _ => []

[11, 10, 9, 8]#eval m11Certificate.map (·.size)

[11, 10, 9, 8]

7920#eval Hex.PermGroup.Kernel.order m11Certificate

Lean then evaluates Hex.PermGroup.Kernel.check on the certificate during type checking. It checks that the first level is generated by the input permutations, that each level's orbit and representatives are correct, and that every Schreier generator of every level reduces to the identity through the levels after it. Here is the Schreier generator formed from the first generator and the second orbit point of the first level, reducing to the identity:

open Hex.PermGroup.Kernel in
true#eval
  let W := width 11
  match m11Certificate with
  | L :: rest =>
    sift 11 W (ident 11 W) rest (schreier 11 W L 0 1)
  | [] => false

true

When the check succeeds, Hex.PermGroup.Kernel.card_closure gives the order:

theorem

Hex.PermGroup.Kernel.card_closure {n : ℕ} {S : Array (Hex.Perm n)}
  {c : Hex.PermGroup.Kernel.Certificate}
  (h :
    Hex.PermGroup.Kernel.check n
        (List.map Hex.PermGroup.Kernel.pack S.toList) c =
      true) :
  Nat.card ↥(Hex.PermGroup.closure S) = Hex.PermGroup.Kernel.order c
Hex.PermGroup.Kernel.card_closure {n : ℕ}
  {S : Array (Hex.Perm n)}
  {c : Hex.PermGroup.Kernel.Certificate}
  (h :
    Hex.PermGroup.Kernel.check n
        (List.map
          Hex.PermGroup.Kernel.pack
          S.toList)
        c =
      true) :
  Nat.card ↥(Hex.PermGroup.closure S) =
    Hex.PermGroup.Kernel.order c

An accepted certificate gives the cardinality of Mathlib's closure.

So that no single declaration takes too long to check, the tactic splits the check into pieces: one for the input generators, one for each level, and one for each range of Schreier generators. Each piece is a separate declaration proved by evaluation, and the tactic combines them to obtain the hypothesis of card_closure, or of the corresponding theorem for membership.

For M11 the whole perm_group proof takes about 0.1 seconds, most of it spent by the kernel checking the certificate.

35.7. The Mathlib correspondence🔗

35.7.1. How perm_group works🔗

35.7.1. How `perm_group` works🔗