SNF tactic

The snf tactic computes and certifies Smith normal form data for a concrete matrix.

User syntax

• snf A

  Adds a local hypothesis named cert:

  cert : CertificateSNF A
  

• snf A as hA

  Adds the same certificate under the chosen name:

  hA : CertificateSNF A
  

The tactic is goal-agnostic: it enriches the local context and leaves the current goal unchanged.

Requirements

The matrix must have type:

Matrix (Fin m) (Fin n) R

where its entries can be serialized through SageSerializable R. The matrix data must be evaluable at elaboration time; fully symbolic matrix variables are not supported.

Dimensions may be non-literal expressions such as cellCount X k. The tactic serializes entries by compiled evaluation, asks Sage for SNF data, reconstructs the matrices in Lean, and builds a CertificateSNF A term checked by Lean.

opaque chainCert.profile : Lean.Option Bool

def ChainCert.profileStep {α : Type} (label : String) (x : Lean.Elab.Tactic.TacticM α) : Lean.Elab.Tactic.TacticM α

Equations

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

structure SnfSageJsonPayload : Type

• U : Lean.Json
• Uinv : Lean.Json
• D : Lean.Json
• V : Lean.Json
• Vinv : Lean.Json

unsafe def evalBoolExpr (e : Lean.Expr) : Lean.MetaM Bool

Equations

• evalBoolExpr e = Lean.Meta.evalExpr Bool (Lean.mkConst `Bool) e

@[implemented_by evalBoolExpr]

opaque evalBoolExprSafe (e : Lean.Expr) : Lean.MetaM Bool

unsafe def evalStringExpr (e : Lean.Expr) : Lean.MetaM String

Equations

• evalStringExpr e = Lean.Meta.evalExpr String (Lean.mkConst `String) e

@[implemented_by evalStringExpr]

opaque evalStringExprSafe (e : Lean.Expr) : Lean.MetaM String

def ChainCert.intRowsToExpr (rows : List (List ℤ)) : Lean.Elab.Tactic.TacticM Lean.Expr

Equations

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

def mkSNFCertExprFromPayload (AExpr : Lean.Expr) (payload : SnfSageJsonPayload) : Lean.Elab.Tactic.TacticM Lean.Expr

Build a CertificateSNF AExpr expression from already available Sage SNF JSON, then elaborate and type-check it.

Equations

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

def declareSNFCertFromPayload (baseName : Lean.Name) (AExpr : Lean.Expr) (payload : SnfSageJsonPayload) : Lean.Elab.TermElabM Lean.Expr

Declare an SNF certificate as a family of named definitions.

This is intended for command elaborators that need a persistent certificate for larger matrices. Naming the witness matrices first keeps Lean from checking one large inlined certificate term.

Equations

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

def mkSNFCertExpr (AExpr : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Build a CertificateSNF AExpr expression from Sage data, then elaborate and type-check it. This is the reusable construction backend for the snf tactic.

Equations

• mkSNFCertExpr AExpr = do let payload ← callSnfSageJson✝ AExpr mkSNFCertExprFromPayload AExpr payload

def snfTac : Lean.ParserDescr

Compute a Smith normal form certificate for A.

Examples:

example : True := by
  snf A
  -- cert : CertificateSNF A
  trivial

example : True := by
  snf A as hA
  -- hA : CertificateSNF A
  trivial

Equations

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

def evalSnfTac : Lean.Elab.Tactic.Tactic

Equations

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