structure Hex.PermGroup.Kernel.Tactic.Config : Type

The limits of one perm_group call.

• maxChunkWork : Nat

  Estimated kernel work per emitted declaration, in field operations.

def Hex.PermGroup.Kernel.Tactic.elabPermGroupConfig (cfg : Lean.Syntax) (init : Config := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM Config

Elaborate the (maxChunkWork := k) configuration of one call.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.evalImages (_n : Nat) (g : Lean.Expr) : Lean.MetaM (List Nat)

Evaluate a closed permutation to its image list.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.checkedImages (nE l : Lean.Expr) : Lean.MetaM Bool

Check whether an image-list constructor uses its valid-permutation branch.

Equations

• Hex.PermGroup.Kernel.Tactic.checkedImages nE l = do let __do_lift ← Lean.Meta.mkAppM `Hex.PermGroup.Kernel.imagesOk #[nE, l] Hex.PermGroup.Kernel.Tactic.evalBoolCore✝ __do_lift

def Hex.PermGroup.Kernel.Tactic.parsePerm (n : Nat) (l : List Nat) : Lean.MetaM (Perm n)

A runtime permutation from its image list.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.natListLit (xs : List Nat) : Lean.MetaM Lean.Expr

Equations

• Hex.PermGroup.Kernel.Tactic.natListLit xs = Lean.Meta.mkListLit (Lean.mkConst `Nat) (List.map Lean.mkNatLit xs)

def Hex.PermGroup.Kernel.Tactic.pairLit (p : Nat × Nat) : Lean.Expr

Equations

• Hex.PermGroup.Kernel.Tactic.pairLit p = Lean.mkApp4 (Lean.mkConst `Prod.mk [0, 0]) (Lean.mkConst `Nat) (Lean.mkConst `Nat) (Lean.mkNatLit p.fst) (Lean.mkNatLit p.snd)

partial def Hex.PermGroup.Kernel.Tactic.rarrayLit {α : Type u_1} (ty : Lean.Expr) (f : α → Lean.Expr) : Lean.RArray α → Lean.Expr

def Hex.PermGroup.Kernel.Tactic.levelLit (L : Level) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.auxName (suffix : String) : Lean.Elab.Tactic.TacticM Lean.Name

A fresh auxiliary name below the current declaration.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.addAuxDecl (decl : Lean.Declaration) : Lean.CoreM Unit

Add an auxiliary declaration, kernel-checking it on a dedicated thread and waiting for the result. When Lean checks theorems asynchronously, the kernel's work is not charged to the heartbeats of the elaboration that produced them, and each check has its own maxHeartbeats budget. perm_group waits instead, so that a failed check is reported by the tactic and rolls back its declarations; running the check on another thread keeps the same accounting. The check shares the tactic's cancellation token, and its messages and traces, such as a warning that a declaration uses sorry, are kept.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.addDataDef (name : Lean.Name) (type value : Lean.Expr) : Lean.MetaM Lean.Expr

Add a noncomputable definition holding kernel data.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.addKernelEq (name : Lean.Name) (lhs rhs : Lean.Expr) : Lean.MetaM Lean.Expr

Add a theorem lhs = rhs, proved by Eq.refl so that the kernel performs the evaluation, in its own declaration.

Equations

• One or more equations did not get rendered due to their size.

inductive Hex.PermGroup.Kernel.Tactic.GoalKind : Type

The shape of a supported goal.

• card (N : Nat) : GoalKind
• mem (g : Lean.Expr) : GoalKind
• notMem (g : Lean.Expr) : GoalKind
• all : GoalKind

structure Hex.PermGroup.Kernel.Tactic.Input : Type

A closed Hex permutation, optionally with a kernel-checkable equality to a canonical Hex expression. Canonical expressions only optimize packing.

• term : Lean.Expr
• canonical? : Option (Lean.Expr × Lean.Expr)

@[instance_reducible]

instance Hex.PermGroup.Kernel.Tactic.instInhabitedInput : Inhabited Input

Equations

• Hex.PermGroup.Kernel.Tactic.instInhabitedInput = { default := Hex.PermGroup.Kernel.Tactic.instInhabitedInput.default }

inductive Hex.PermGroup.Kernel.Tactic.Goal : Type

A requested computational conclusion.

• card (N : Nat) : Goal
• mem (g : Input) : Goal
• notMem (g : Input) : Goal
• all : Goal

structure Hex.PermGroup.Kernel.Tactic.Prepared : Type

Prepared, untrusted certificate data shared by replay and source rendering. Every proof-producing operation still checks the packing and certificate.

• config : Config
• degree : Nat
• inputs : List Input
• images : List (List Nat)
• certificate : Certificate
• cached : Bool

  Whether certificate was checked earlier in this file, in which case replay emits none of its level checks and parts is empty.

• parts : List (List (Nat × Nat))

def Hex.PermGroup.Kernel.Tactic.Prepared.order (p : Prepared) : Nat

The order proposed by the prepared certificate.

Equations

• p.order = Hex.PermGroup.Kernel.order p.certificate

structure Hex.PermGroup.Kernel.Tactic.Checked : Type

A certificate already checked by the kernel earlier in the current file. checked proves check degree inputs (mkConst cert) = true, and levels are the data definitions listed by cert.

• certificate : Certificate
• cert : Lean.Name
• levels : Array Lean.Name
• checked : Lean.Name

opaque Hex.PermGroup.Kernel.Tactic.checkedExt : Lean.EnvExtension (Std.HashMap (Nat × List Nat) Checked)

Checked certificates of the current file, keyed by degree and packed generators. Later perm_group calls on the same generators reuse them instead of certifying and checking the chain again. The state is not exported: an importing module cannot unfold the certificate definitions.

def Hex.PermGroup.Kernel.Tactic.findChecked? (n : Nat) (inputs : List Nat) : Lean.MetaM (Option Checked)

The checked certificate for these packed generators, if any.

Equations

• Hex.PermGroup.Kernel.Tactic.findChecked? n inputs = do let __do_lift ← Lean.getEnv pure (Hex.PermGroup.Kernel.Tactic.checkedExt.getState __do_lift)[(n, inputs)]?

def Hex.PermGroup.Kernel.Tactic.prepare (cfg : Config) (n : Nat) (inputs : List Input) : Lean.MetaM Prepared

Evaluate and prepare the generators once. This operation adds no declarations.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.packTie (nE g : Lean.Expr) (x : Nat) (suffix : String) : Lean.Elab.Tactic.TacticM Lean.Expr

A proof that pack g = x. A generator written Perm.ofImages n l is checked in time linear in n. Any other closed permutation is evaluated by the kernel.

Equations

• One or more equations did not get rendered due to their size.

partial def Hex.PermGroup.Kernel.Tactic.arrayElems? (s : Lean.Expr) (fuel : Nat := 32) : Lean.MetaM (Option (List Lean.Expr))

Read an array literal, unfolding definitions without reducing its elements.

def Hex.PermGroup.Kernel.Tactic.degree (S : Lean.Expr) : Lean.MetaM Nat

The degree must be a numeral.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.readGoal? (target : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × GoalKind))

Match the computational generation and order goal forms.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.replay (prepared : Prepared) (goal : Goal) : Lean.Elab.Tactic.TacticM Lean.Expr

Replay a requested conclusion. Packing transport, bounded declarations and final proof checking are owned by Hex, and failures restore all tactic state.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.prove (cfg : Config) (n : Nat) (gens : List Lean.Expr) (kind : GoalKind) (tie : Lean.Expr → Lean.Expr → Nat → String → Lean.Elab.Tactic.TacticM Lean.Expr := packTie) : Lean.Elab.Tactic.TacticM Lean.Expr

Compatibility entry point for consumers of the original replay API.

Equations

• One or more equations did not get rendered due to their size.

structure Hex.PermGroup.Kernel.Tactic.Extension : Type

A perm_group goal handler contributed by a downstream library. A public meta def of this type tagged @[perm_group_extension] extends the same perm_group syntax to that library's goal shapes.

• prove? : Config → Lean.Expr → Lean.Elab.Tactic.TacticM (Option Lean.Expr)

  Handle a goal, returning its proof term, or none when the goal shape is not this extension's.

• certificate? : String → Lean.Expr → Lean.Syntax → Lean.Elab.TermElabM (Option String)

  Print a certificate for this extension's generator representation.

opaque Hex.PermGroup.Kernel.Tactic.extensionExt : Lean.SimplePersistentEnvExtension Lean.Name (Array Lean.Name)

The registered perm_group extensions, in declaration order.

def Hex.PermGroup.Kernel.Tactic.extensions : Lean.MetaM (List Extension)

All extensions present in the current environment, in lookup order.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.permGroup : Lean.ParserDescr

Prove generation, non-generation or exact order from a packed certificate. Correspondence libraries extend this syntax to goals about subgroup closures.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.permGroupTac (cfg : Config) : Lean.Elab.Tactic.TacticM Unit

The shared tactic entry point, also callable by computational consumers.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.evalPermGroup : Lean.Elab.Tactic.Tactic

Equations

• Hex.PermGroup.Kernel.Tactic.evalPermGroup stx = do let __do_lift ← Hex.PermGroup.Kernel.Tactic.elabPermGroupConfig stx[1] Hex.PermGroup.Kernel.Tactic.permGroupTac __do_lift

partial def Hex.PermGroup.Kernel.Tactic.rarraySrc {α : Type u_1} (f : α → String) : Lean.RArray α → String

def Hex.PermGroup.Kernel.Tactic.listSrc {α : Type u_1} (f : α → String) (xs : List α) : String

Equations

• Hex.PermGroup.Kernel.Tactic.listSrc f xs = "[" ++ ", ".intercalate (List.map f xs) ++ "]"

def Hex.PermGroup.Kernel.Tactic.pairSrc (p : Nat × Nat) : String

Equations

• Hex.PermGroup.Kernel.Tactic.pairSrc p = toString "(" ++ toString p.fst ++ toString ", " ++ toString p.snd ++ toString ")"

def Hex.PermGroup.Kernel.Tactic.levelSrc (L : Level) : String

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.render (name : String) (prepared : Prepared) (elemSrc : List String) (sSrc : String) (imagesTie : Lean.Expr → Lean.MetaM (Option String) := fun (g : Lean.Expr) => have __do_jp := fun (__r : Unit) => pure none; if g.isAppOfArity `Hex.Perm.ofImages 2 = true then do let __do_lift ← checkedImages (Lean.mkNatLit prepared.degree) (g.getArg! 1) if __do_lift = true then pure (some "_root_.Hex.PermGroup.Kernel.pack_ofImages") else __do_jp () else __do_jp ()) : Lean.Elab.TermElabM String

Print kernel packing ties and bounded checks for the prepared certificate. Canonical image constructors use their optimized ties; other inputs use kernel evaluation of the original term.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.certificateSource (name : String) (n : Nat) (gens : List Lean.Expr) (elemSrc : List String) (sSrc : String) (imagesTie : Lean.Expr → Lean.MetaM (Option String) := fun (g : Lean.Expr) => have __do_jp := fun (__r : Unit) => pure none; if g.isAppOfArity `Hex.Perm.ofImages 2 = true then do let __do_lift ← checkedImages (Lean.mkNatLit n) (g.getArg! 1) if __do_lift = true then pure (some "_root_.Hex.PermGroup.Kernel.pack_ofImages") else __do_jp () else __do_jp ()) : Lean.Elab.TermElabM String

Compatibility printer for the original generator-expression API.

Equations

• One or more equations did not get rendered due to their size.

partial def Hex.PermGroup.Kernel.Tactic.arraySources? (stx : Lean.Syntax) : Option (Array Lean.Syntax)

Recover authored elements without pretty-printing their proof fields.

def Hex.PermGroup.Kernel.Tactic.permGroupCertificate : Lean.ParserDescr

Print a reusable kernel certificate and its exact-order proof.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Kernel.Tactic.elabPermGroupCertificate : Lean.Elab.Command.CommandElab

Equations

• One or more equations did not get rendered due to their size.