Certificate-chain evaluator for BirdDet.birdDet

This file contains an evaulator that computes the ring tactic normal form of Mathlib.LinearAlgebra.Matrix.Determinant.Bird.birdDet via iteratively unfolding its definition, using the ring tactic for ring operations, and caching intermediate certificates.

The structure Cert rα carries the proof certificate and the evaluator builds larger certificates as birdDet is unfolded.

The entrypoint of the evaluator certBirdDet follows the two branches (n=0, n=k+1) of the birdDet function:

certBirdDet (birdDet n A)
  n = 0:
    birdDet n A
      = 1 -- via BirdDet.birdDet_zero
      = ring normal form of 1 -- via certEval
  n = k + 1:
    birdDet n A
      = (-1)^k * iter n A k (get n A) 0 0 -- via BirdDet.birdDet_eq
      = ring normal form of the product -- certMul (certBirdSign k) (certIter k 0 0)

The iter n A k (get n A) i j function branches on k, (k=0, k=t+1) and therefore the certIter function has two branches:

certIter k i j
  k = 0:
    iter n A 0 F i j = F i j -- via BirdDet.iter_zero
                     = ring normal form of A[i][j] -- via certEntry i j
  k = t + 1:
    iter n A (t + 1) F i j
      = -(sumFrom n (i + 1) fun k => iter n A t F k k) * get n A i j
          + sumFrom n (i + 1) fun k => iter n A t F i k * get n A k j
        -- via BirdDet.iter_succ
      = normal form of the first summand + normal form of the second summand
        -- via certAdd
                 (certMul (certNeg (certDiag t (i + 1))) (certEntry i j))
                 (certTail t i j (i + 1))

Then the certDiag and certTail functions certify the two kinds of sumFrom expressions.

The evaulator also memoizes the certIter, certDiag and certEntry functions to improve performance.

Main definitions

• certEntry certifies BirdDet.get.
• certSumFromStop and certSumFromStep certifies BirdDet.sumFrom_stop and BirdDet.sumFrom_step.
• certIter certifies BirdDet.iter_zero and BirdDet.iter_succ.
• certBirdDet certifies BirdDet.birdDet_zero and BirdDet.birdDet_eq.

@[reducible, inline]

abbrev Mathlib.Tactic.Determinant.CertVal {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (e : Q(«$α»)) : Type

The ring tactic normal-form value.

Equations

• Mathlib.Tactic.Determinant.CertVal rα e = Mathlib.Tactic.Ring.Common.ExSum Mathlib.Tactic.Ring.RatCoeff (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα) e

@[reducible, inline]

abbrev Mathlib.Tactic.Determinant.CertResult {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (subject : Q(«$α»)) : Type

The ring tactic result carried by a certificate.

Equations

• Mathlib.Tactic.Determinant.CertResult rα subject = Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Determinant.CertVal rα) subject

def Mathlib.Tactic.Determinant.Ctx.iterP {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (ctx : Ctx rα) (t : ℕ) : Q(ℕ → ℕ → «$α»)

Return an expression for the partially applied function iter n A t (get n A)

Equations

• ctx.iterP t = q(BirdDet.iter unknown_1 unknown_2 «$t» (BirdDet.get unknown_1 unknown_2))

def Mathlib.Tactic.Determinant.Ctx.sumFrom {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (ctx : Ctx rα) (lo : ℕ) (f : Q(ℕ → «$α»)) : Q(«$α»)

Return an expression sumFrom n lo f

Equations

• ctx.sumFrom lo f = q(BirdDet.sumFrom unknown_1 «$lo» «$f»)

structure Mathlib.Tactic.Determinant.Cert {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) : Type

A certificate that proves subject = result.norm via result.proof

• subject : Q(«$α»)

  The expression being certified.

• result : CertResult rα self.subject

  The result of evaluating subject using the ring tactic.

• isZero : Bool

  true when norm is zero, used as a hint to the evaluator.

def Mathlib.Tactic.Determinant.Cert.norm {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (c : Cert rα) : Q(«$α»)

The ring tactic normal form of c.subject

Equations

• c.norm = c.result.expr

def Mathlib.Tactic.Determinant.Cert.val {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (c : Cert rα) : CertVal rα c.norm

The internal ring tactic representation of c.norm

Equations

• c.val = c.result.val

def Mathlib.Tactic.Determinant.Cert.proof {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (c : Cert rα) : have a := c.norm; have a_1 := c.subject; Q(«$a_1» = «$a»)

The proof that c.subject = c.norm

Equations

• c.proof = c.result.proof

def Mathlib.Tactic.Determinant.Cert.chainProof {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} {lhs rhs : Q(«$α»)} (c : Cert rα) (h : Q(«$lhs» = «$rhs»)) : Cert rα

Prepend an equality to an existing normalized certificate.

Given c.proof : s.subject = c.norm and h : lhs = s.subject return a certificate with proof : lhs = c.norm.

Equations

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

structure Mathlib.Tactic.Determinant.CertCache {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) : Type

Cache certificates that are reused by the recursive Bird evaluator.

• entryCache : Std.HashMap (ℕ × ℕ) (Cert rα)

  Cache for entry certificates, keyed by matrix indices.

• iterCache : Std.HashMap (ℕ × ℕ × ℕ) (Cert rα)

  Cache for iter certificates, keyed by recursion index and matrix indices.

• diagCache : Std.HashMap (ℕ × ℕ) (Cert rα)

  Cache for diagonal-tail certificates, keyed by recursion index and lower bound.

@[reducible, inline]

abbrev Mathlib.Tactic.Determinant.CertM {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) : Type → Type

The monad used by the certificate-chaining evaluator

Equations

• Mathlib.Tactic.Determinant.CertM rα = StateT (Mathlib.Tactic.Determinant.CertCache rα) (ReaderT (Mathlib.Tactic.Determinant.Ctx rα) Mathlib.Tactic.AtomM)

def Mathlib.Tactic.Determinant.isZeroVal {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} {e : Q(«$α»)} (val : CertVal rα e) : Bool

Checks if val is zero according to the ring tactic

Equations

• Mathlib.Tactic.Determinant.isZeroVal Mathlib.Tactic.Ring.Common.ExSum.zero = true
• Mathlib.Tactic.Determinant.isZeroVal (Mathlib.Tactic.Ring.Common.ExSum.add a_1 a_2) = false

def Mathlib.Tactic.Determinant.toCert {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} {e : Q(«$α»)} (res : Ring.Common.Result (CertVal rα) e) : Cert rα

Construct a Cert rα from a ring tactic result

Equations

• Mathlib.Tactic.Determinant.toCert res = { subject := e, result := res, isZero := Mathlib.Tactic.Determinant.isZeroVal res.val }

def Mathlib.Tactic.Determinant.zeroCertOfProof {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} {lhs : Q(«$α»)} (h : Q(«$lhs» = 0)) : Cert rα

Build a zero certificate from a proof lhs = 0.

Equations

• Mathlib.Tactic.Determinant.zeroCertOfProof h = { subject := lhs, result := { expr := q(0), val := Mathlib.Tactic.Ring.Common.ExSum.zero, proof := h }, isZero := true }

def Mathlib.Tactic.Determinant.zeroProdCert {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (x : Q(«$α»)) (c : Cert rα) : Lean.MetaM (Cert rα)

If c.norm = 0, return a certificate with proof x * c.subject = 0 without recursively certifying x.

Equations

• Mathlib.Tactic.Determinant.zeroProdCert x c = pure (Mathlib.Tactic.Determinant.zeroCertOfProof q(⋯))

def Mathlib.Tactic.Determinant.certEval {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (e : Q(«$α»)) : CertM rα (Cert rα)

Certify e = norm by evaluating e with the ring normalizer.

Equations

• Mathlib.Tactic.Determinant.certEval e = do let ctx ← read let res ← liftM (Mathlib.Tactic.Ring.Common.eval Mathlib.Tactic.Ring.rcℕ ctx.rc ctx.cα e) pure (Mathlib.Tactic.Determinant.toCert res)

def Mathlib.Tactic.Determinant.certAdd {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (a b : Cert rα) : CertM rα (Cert rα)

Certify a.subject + b.subject from certificates for a and b.

Equations

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

def Mathlib.Tactic.Determinant.certMul {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (a b : Cert rα) : CertM rα (Cert rα)

Certify a.subject * b.subject from certificates for a and b.

Equations

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

def Mathlib.Tactic.Determinant.certNeg {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (a : Cert rα) : CertM rα (Cert rα)

Certify -a.subject from a certificate for a.

Equations

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

def Mathlib.Tactic.Determinant.certBirdSign {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (k : ℕ) : CertM rα (Cert rα)

Certify the sign factor (-1)^k from BirdDet.birdDet_eq.

Equations

• Mathlib.Tactic.Determinant.certBirdSign k = Mathlib.Tactic.Determinant.certEval q((-1) ^ «$k»)

def Mathlib.Tactic.Determinant.certEntry {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (i j : ℕ) : CertM rα (Cert rα)

Certify one matrix entry lookup BirdDet.get n A i j.

Equations

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

def Mathlib.Tactic.Determinant.certSumFromStop {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (lo : ℕ) (f : Q(ℕ → «$α»)) : CertM rα (Cert rα)

Certify the stop branch of BirdDet.sumFrom.

This corresponds to the else 0 branch of:

sumFrom n lo f = if lo < n then f lo + sumFrom n (lo + 1) f else 0

Throws a meta-level error if called with lo such that lo < ctx.dimension.

Equations

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

def Mathlib.Tactic.Determinant.certSumFromStep {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (lo : ℕ) (f : Q(ℕ → «$α»)) (headCert tailCert : CertM rα (Cert rα)) : CertM rα (Cert rα)

Certify the step branch of BirdDet.sumFrom.

This corresponds to the lo < n branch of:

sumFrom n lo f = if lo < n then f lo + sumFrom n (lo + 1) f else 0

Throws a meta-level error if called with lo such that ¬ lo < ctx.dimension.

Equations

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

partial def Mathlib.Tactic.Determinant.certIter {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (t i j : ℕ) : CertM rα (Cert rα)

Certify a BirdDet.iter call.

partial def Mathlib.Tactic.Determinant.certDiag {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (t lo : ℕ) : CertM rα (Cert rα)

Certify the diagonal tail sum from BirdDet.iter_succ:

sumFrom n (i + 1) fun k => iter n A t F k k)

partial def Mathlib.Tactic.Determinant.certTail {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} (t i j lo : ℕ) : CertM rα (Cert rα)

Certify the upper-tail sum from BirdDet.iter_succ:

sumFrom n (i + 1) fun k => iter n A t F i k * get n A k j

def Mathlib.Tactic.Determinant.certBirdDet {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} : CertM rα (Cert rα)

Certify a BirdDet.birdDet n A call.

Equations

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