def HexMatrixMathlib.Det.instToExprDetWitness_hexBareissMathlib.toExpr : Hex.Matrix.DetWitness → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• HexMatrixMathlib.Det.instToExprDetWitness_hexBareissMathlib.toExpr (Hex.Matrix.DetWitness.singular a) = (Lean.Expr.const `Hex.Matrix.DetWitness.singular []).app (Lean.toExpr a)

@[instance_reducible]

instance HexMatrixMathlib.Det.instToExprDetWitness_hexBareissMathlib : Lean.ToExpr Hex.Matrix.DetWitness

Equations

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

inductive HexMatrixMathlib.Det.Outcome (α : Type) : Type

The outcome of an attempt, per the matrix-tactic protocol; a failure throws.

• notApplicable {α : Type} : Outcome α

  The goal or input is not in the fragment; the next handler may try.

• declined {α : Type} (msg : Lean.MessageData) : Outcome α

  In the fragment, but a capability is missing; the message names it.

• success {α : Type} (a : α) : Outcome α

  A value and a proof.

def HexMatrixMathlib.Det.detTarget? (target : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Bool)

Recognize a determinant target: the matrix, the other side, and whether the determinant is on the right.

Equations

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

structure HexMatrixMathlib.Det.Cert : Type

The certificate of a square literal: the witness, the row list of the integer matrix it certifies, and for a rational literal the rational row list and the row scales.

• lit : Literal.Recognized

  The recognized literal.

• witness : Hex.Matrix.DetWitness

  The witness of the integer matrix.

• rows : Array (Array ℤ)

  The integer rows.

• rat : Option (Array (Array ℚ) × Array ℕ)

  The rational rows and the positive scale of each, for a rational literal.

def HexMatrixMathlib.Det.Cert.value (c : Cert) : ℚ

The certified determinant as a rational.

Equations

• c.value = match c.rat with | none => ↑c.witness.value | some (fst, s) => ↑c.witness.value / ↑(Array.foldl (fun (x1 x2 : ℕ) => x1 * x2) 1 s)

def HexMatrixMathlib.Det.certify (A : Lean.Expr) : Lean.MetaM (Outcome Cert)

Recognize a closed square integer or rational literal and certify it. A producer whose witness fails its own check is a failure, not a decline.

Equations

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

structure HexMatrixMathlib.Det.Proof : Type

The proof of Matrix.det A = v for the certificate's value v, with the value, the kernel check it rests on, and the row list of the literal.

• value : Lean.Expr

  The certified value, as a numeral.

• proof : Lean.Expr

  The proof term of Matrix.det A = value.

• check : Lean.Expr

  The certificate check the kernel evaluates.

• rowList : Lean.Expr

  The row list the literal is identified with.

def HexMatrixMathlib.Det.build (A : Lean.Expr) (c : Cert) : Lean.MetaM Proof

Build the proof of Matrix.det A = v for the certificate's value v.

Equations

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

def HexMatrixMathlib.Det.diagnose (A : Lean.Expr) (c : Cert) (p : Proof) (e : Lean.Exception) : Lean.MetaM Lean.Exception

Diagnose a proof the kernel rejected: evaluate the certificate check with the kernel and test the identification of the literal with its row list along its route, reporting the first that fails.

Equations

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

def HexMatrixMathlib.Det.checked (A : Lean.Expr) (c : Cert) (p : Proof) (target proof : Lean.Expr) : Lean.MetaM Lean.Expr

Add proof : target as an auxiliary theorem checked synchronously, so that a rejection is reported here, not later, and diagnosed.

Equations

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

def HexMatrixMathlib.Det.proveGoal (target : Lean.Expr) : Lean.MetaM (Outcome Lean.Expr)

Prove a determinant target in either orientation.

Equations

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

def HexMatrixMathlib.Det.certifiedProof (A : Lean.Expr) (c : Cert) : Lean.MetaM Proof

The proof of Matrix.det A = v for the certified value v, checked.

Equations

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

def HexMatrixMathlib.Det.certified (A : Lean.Expr) : Lean.MetaM (Outcome Lean.Expr)

The det% A record: Certified Matrix.det A.

Equations

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

def HexMatrixMathlib.Det.detTerm : Lean.ParserDescr

det% A computes the determinant of a closed integer or rational matrix literal A and returns a HexMatrixMathlib.Certified Matrix.det A record with its value and proof. The !![…] notations are given an integer entry expectation.

Equations

• HexMatrixMathlib.Det.detTerm = Lean.ParserDescr.node `HexMatrixMathlib.Det.detTerm 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "det%") (Lean.ParserDescr.cat `term 1024))

def HexMatrixMathlib.Det.elabDetTerm : Lean.Elab.Term.TermElab

Equations

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

def HexMatrixMathlib.Det.normDet? (e : Lean.Expr) : Lean.MetaM (Option Lean.Meta.Simp.Result)

Rewrite Matrix.det A to its certified value when the Hex frontend applies; none when it declines.

Equations

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

def hex_norm_det : Lean.Meta.Simp.Simproc

The hex_norm_det simproc rewrites the determinant of a closed integer or rational matrix literal to its value through the Hex certificate, and falls back to Mathlib's norm_det when the Hex frontend declines (symbolic entries, other carriers); a producer failure or a certificate the kernel rejects is an error, not a fallback.

Equations

• hex_norm_det e = do let __do_lift ← liftM (HexMatrixMathlib.Det.normDet? e) match __do_lift with | some r => pure (Lean.Meta.Simp.Step.done r) | none => norm_det e

def HexMatrixMathlib.Det.detTac : Lean.ParserDescr

det closes A.det = d and d = A.det for a closed integer or rational matrix literal A, with the kernel checking a determinant certificate; an input outside that fragment is handed to the simp set hex_norm_det, whose fallback is Mathlib's norm_det. The keyword is non-reserved, so det stays usable as an identifier.

Equations

• HexMatrixMathlib.Det.detTac = Lean.ParserDescr.node `HexMatrixMathlib.Det.detTac 1022 (Lean.ParserDescr.nonReservedSymbol "det" false)

def HexMatrixMathlib.Det.evalDetTac : Lean.Elab.Tactic.Tactic

Equations

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