From 834c9cb8c8ccc4a9a19d5f6e6aa11e5c998a86c6 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 00:49:34 +0100 Subject: [PATCH 01/34] add lookup tactic: query LMFDB for counterexamples --- LeanBridge/Lookup/DECISIONS.md | 32 +++++ LeanBridge/Lookup/Demo.lean | 244 +++++++++++++++++++++++++++++++++ 2 files changed, 276 insertions(+) create mode 100644 LeanBridge/Lookup/DECISIONS.md create mode 100644 LeanBridge/Lookup/Demo.lean diff --git a/LeanBridge/Lookup/DECISIONS.md b/LeanBridge/Lookup/DECISIONS.md new file mode 100644 index 00000000..31410e47 --- /dev/null +++ b/LeanBridge/Lookup/DECISIONS.md @@ -0,0 +1,32 @@ +# `lookup` tactic — decisions where the right choice was unclear + +## Clickable LMFDB link (task 2) + +**Unclear:** Lean core `MessageData` has no dedicated hyperlink constructor, so "make the +link clickable in the infoview" is environment-dependent. The VS Code Lean infoview +auto-linkifies bare `http(s)://` URLs in messages, but does *not* linkify a URL wrapped in +parentheses or with trailing punctuation attached. + +- Option A: keep a custom widget / `MessageData.ofWidget` to render an `` tag. Heavy, + and overkill for a one-line link. +- Option B: emit the URL bare on its own line with no surrounding punctuation, relying on + the infoview's auto-linkification. + +**Chosen: Option B.** The previous message put the URL inside `(...)`, which defeats +auto-linkification; isolating it on its own line is the minimal fix and matches how other +Lean tactics surface URLs. If it turns out the infoview still does not linkify it, revisit +with a widget. + +## Reporting signed-discriminant counterexamples (tasks 3 & 7) + +**Unclear:** how to display the discriminant of a counterexample when the query referenced +the *signed* discriminant (`NumberField.discr F`), given the DB stores `disc_sign` and +`disc_abs` separately. + +- Option A: report the two raw columns (`disc_sign = 1, disc_abs = 41`). +- Option B: report the reconstructed signed value (`discriminant = 41`) by selecting the + SQL expression `(disc_sign * disc_abs)`. + +**Chosen: Option B.** It mirrors what the user wrote in Lean (`NumberField.discr F`) and is +less confusing than exposing the storage split. `|NumberField.discr F|` still reports as +`|discriminant|` backed by `disc_abs`. diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean new file mode 100644 index 00000000..08e69861 --- /dev/null +++ b/LeanBridge/Lookup/Demo.lean @@ -0,0 +1,244 @@ +import Mathlib + +-- https://www.lmfdb.org/api/nf_fields/?_format=json&_offset=0 + +open Lean Elab Tactic Meta + + + +/-- Build the request body for an LMFDB `/sql` call. -/ +def sqlRequestBody (sql : String) (limit : Nat := 1000) : Json := + .mkObj [ + ("sql", toJson sql), + ("limit", toJson limit) + ] + +/-- Run a SQL query against the LMFDB `/sql` endpoint and return the decoded result. -/ +def runSql (sql : String) : MetaM Json := do + let sqlUrl := "https://mcp.lmfdb.org/sql" + let curlArgs := #[ + "-sS", + "-X", "POST", sqlUrl, + "-H", "Content-Type: application/json", + "-d", (sqlRequestBody sql).compress + ] + let out ← IO.Process.output { cmd := "curl", args := curlArgs } + if out.exitCode != 0 then + throwError s!"curl failed (exit {out.exitCode}): {out.stderr}" + let .ok result := Json.parse out.stdout + | throwError s!"failed to parse response:\n{out.stdout}" + return result + +-- #eval runSql "SELECT lmfdb_label, conductor, rank FROM ec_curvedata WHERE rank >= 4 AND conductor <= 1000 LIMIT 1" +-- #eval runSql "SELECT label, coeffs, degree FROM nf_fields WHERE degree = 2 LIMIT 1" + +/-! ### The `lookup` tactic + +`lookup` reads the local hypotheses and the goal, translates them into a SQL query +against LMFDB that searches for a *counterexample* (a database object satisfying all the +hypotheses but **violating** the goal), and reports it if one is found. -/ + +namespace Lookup + +initialize registerTraceClass `lookup + +/-- Extract a natural-number literal from `e`, handling `@OfNat.ofNat _ n _`. -/ +def getNatLit? (e : Expr) : Option Nat := + match e.getAppFnArgs with + | (``OfNat.ofNat, #[_, n, _]) => n.rawNatLit? + | _ => e.rawNatLit? + +/-- Extract an integer literal, handling a leading negation `@Neg.neg _ _ n`. -/ +def getIntLit? (e : Expr) : Option Int := + match e.getAppFnArgs with + | (``Neg.neg, #[_, _, a]) => (getNatLit? a).map fun n => -(n : Int) + | _ => (getNatLit? e).map Int.ofNat + +/-- A scalar translated to SQL: the SQL text plus the quantities it references, recorded as +`(displayName, sqlExpr)` pairs so a counterexample's actual values can be reported. -/ +abbrev SqlScalar := String × Array (String × String) + +/-- Translate a scalar Lean expression (applied to the number field) into a SQL scalar over +`nf_fields`: a column expression or a numeric literal. -/ +def toSqlScalar (e : Expr) : Option SqlScalar := + match e.getAppFnArgs with + | (``NumberField.classNumber, _) => + some ("class_number", #[("class number", "class_number")]) + | (``Module.finrank, args) => + -- `Module.finrank ℚ F` is the degree of the number field `F` over `ℚ`. + if h : 0 < args.size then + if args[0].isConstOf ``Rat then some ("degree", #[("degree", "degree")]) else none + else none + | (``abs, args) => args.back?.bind fun x => + -- `|NumberField.discr F|` is the absolute discriminant `disc_abs`. + match x.getAppFnArgs with + | (``NumberField.discr, _) => some ("disc_abs", #[("|discriminant|", "disc_abs")]) + | _ => none + | (``NumberField.discr, _) => + -- The LMFDB stores the discriminant split as a sign and an absolute value. + some ("(disc_sign * disc_abs)", #[("discriminant", "(disc_sign * disc_abs)")]) + | _ => (getIntLit? e).map fun n => (toString n, #[]) + +/-- Match a binary comparison `Prop`, returning the SQL operator and the two sides. -/ +def matchCmp (e : Expr) : Option (String × Expr × Expr) := + match e.getAppFnArgs with + | (``Eq, #[_, a, b]) => some ("=", a, b) + | (``LE.le, #[_, _, a, b]) => some ("<=", a, b) + | (``LT.lt, #[_, _, a, b]) => some ("<", a, b) + | (``GE.ge, #[_, _, a, b]) => some (">=", a, b) + | (``GT.gt, #[_, _, a, b]) => some (">", a, b) + | _ => none + +/-- Translate a comparison `Prop` into a SQL condition together with the referenced +quantities. -/ +def toSqlCond (e : Expr) : Option SqlScalar := do + let (op, a, b) ← matchCmp e + let (sa, ra) ← toSqlScalar a + let (sb, rb) ← toSqlScalar b + return (s!"{sa} {op} {sb}", ra ++ rb) + +/-- The first returned row of an LMFDB `/sql` response, if any. -/ +def firstRow? (j : Json) : Option Json := + match j.getObjVal? "rows" with + | .ok (.arr rs) => rs[0]? + | _ => none + +/-- Read a (text-cast) field of a row as a string. -/ +def rowStr (row : Json) (key : String) : String := + (row.getObjValAs? String key).toOption.getD "?" + +/-- Pretty-print the integer monomial `c * x^e` (its sign is handled by the caller). -/ +def monomial (c : Int) (e : Nat) : String := + if e == 0 then toString c.natAbs + else + let base := if e == 1 then "x" else s!"x^{e}" + if c.natAbs == 1 then base else s!"{c.natAbs}*{base}" + +/-- Format an LMFDB `coeffs` array (e.g. `{-1,-1,1}`, lowest degree first) as a polynomial +in `x`, highest degree first. -/ +def formatPoly (coeffs : String) : String := Id.run do + let stripped := (coeffs.replace "{" "").replace "}" "" + let cs := (stripped.splitOn ",").filterMap String.toInt? + let n := cs.length + let mut out := "" + for i in [0:n] do + let e := n - 1 - i + let c := cs[e]! + if c == 0 then continue + let term := monomial c e + if out.isEmpty then + out := if c < 0 then s!"-{term}" else term + else + out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}") + return if out.isEmpty then "0" else out + +elab "lookup" : tactic => do + let goal ← getMainGoal + goal.withContext do + -- Translate each Prop hypothesis we understand into a SQL condition, collecting the + -- quantities (columns) referenced along the way. + let mut conds : Array String := #[] + let mut refs : Array (String × String) := #[] + for ldecl in ← getLCtx do + if ldecl.isImplementationDetail then continue + let ty ← instantiateMVars ldecl.type + if let some (c, r) := toSqlCond ty then + conds := conds.push c + refs := refs ++ r + -- The goal becomes the *negated* condition: we hunt for a row that breaks it. + let goalTy ← instantiateMVars (← goal.getType) + let some (goalCond, goalRefs) := toSqlCond goalTy + | throwError "lookup: don't know how to translate the goal into a SQL query:\n{goalTy}" + refs := refs ++ goalRefs + -- Deduplicate referenced quantities by their SQL expression, preserving order. + let mut seen : Array String := #[] + let mut items : Array (String × String) := #[] + for (name, expr) in refs do + unless seen.contains expr do + seen := seen.push expr + items := items.push (name, expr) + -- Build the SELECT list: label, defining polynomial coeffs, and each referenced + -- quantity, cast to text (the LMFDB endpoint cannot serialise bignum columns directly). + let mut selects : Array String := #["label", "coeffs::text AS coeffs"] + for i in [0:items.size] do + let (_, expr) := items[i]! + selects := selects.push s!"({expr})::text AS c{i}" + let whereClause := String.intercalate " AND " (conds.toList ++ [s!"NOT ({goalCond})"]) + let query := s!"SELECT {String.intercalate ", " selects.toList} \ + FROM nf_fields WHERE {whereClause} LIMIT 1" + trace[lookup] "query:\n{query}" + let result ← runSql query + match firstRow? result with + | none => + -- No counterexample in the database: report, but do *not* close the goal. + logInfo m!"lookup: no counterexample found in LMFDB \ + (the statement is consistent with the database, but this is not a proof)." + | some row => + let label := rowStr row "label" + let poly := formatPoly (rowStr row "coeffs") + let mut valueLines : Array MessageData := #[] + for i in [0:items.size] do + let (name, _) := items[i]! + let v := rowStr row s!"c{i}" + valueLines := valueLines.push m!"{name} = {v}" + let values := MessageData.joinSep valueLines.toList ", " + throwError m!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ + number field {label}, with minimal polynomial {poly}\n\ + {values}\n\ + https://www.lmfdb.org/NumberField/{label}" + +end Lookup + + +/- +**Elliptic curves over Q:** `SELECT lmfdb_label, ainvs FROM ec_curvedata WHERE...` +* [ec.torsion_subgroup](https://beta.lmfdb.org/knowledge/show/ec.torsion_subgroup) -- `torsion=4` or `torsion_structure='{2,2}'` +* [ec.discriminant](https://beta.lmfdb.org/knowledge/show/ec.discriminant) -- `absD=164025 AND signD=1` +* [ec.rank](https://beta.lmfdb.org/knowledge/show/ec.rank) / [ec.mordell_weil_group]([https://beta.lmfdb.org/knowledge/show/ec.mordell_weil_group) -- `rank=4` + +**Dirichlet characters:** `SELECT label FROM char_dirichlet WHERE...` +* [character.dirichlet.primitive](https://beta.lmfdb.org/knowledge/show/character.dirichlet.primitive) -- `is_primitive='t'` +* [character.dirichlet.order](https://beta.lmfdb.org/knowledge/show/character.dirichlet.order) -- `order=4` +* [character.dirichlet.conductor](https://beta.lmfdb.org/knowledge/show/character.dirichlet.conductor) -- `conductor=4` + +**Number fields:** `SELECT label, coeffs FROM nf_fields WHERE...` +* [nf.degree_mathlib_def](https://beta.lmfdb.org/knowledge/show/nf.degree_mathlib_def) -- `degree=6` +* [nf.ideal_class_group](https://beta.lmfdb.org/knowledge/show/nf.ideal_class_group) -- `class_group='{2,2}'` +* [nf.class_number](https://beta.lmfdb.org/knowledge/show/nf.class_number) -- `class_number=4` +* [nf.discriminant](https://beta.lmfdb.org/knowledge/show/nf.discriminant) -- `disc_abs=41 AND disc_sign=1` + +*Example*: Every number field with class number 1 and degree 2 has absolute discriminant at most 163 + +**Groups:** `SELECT label, tex_name FROM gps_groups WHERE...` +* [group.simple](https://beta.lmfdb.org/knowledge/show/group.simple) -- `simple='t'` +* [group.abelian](https://beta.lmfdb.org/knowledge/show/group.abelian) -- `abelian='t'` + +*Example*: Every simple group is nonabelian +-/ + +-- `ec_curvedata` = (W : WeierstrassCurve.Affine ℚ) +-- `torsion` = Nat.card (AddCommGroup.torsion W.Point) +-- `torsion_structure` ≈ AddCommGroup.torsion W.Point, but note that torsion_structure is the strucutre of the group as a product of cyclics +-- `rank` = Module.finrank ℤ W.Point + +example {F : Type*} [Field F] [NumberField F] + (hF : NumberField.classNumber F = 1) (hF : Module.finrank ℚ F = 2) : + |NumberField.discr F| ≤ 163 := by + lookup + +-- TEMP signed-discriminant test (FALSE: the disc = -163 field is a counterexample) +example {F : Type*} [Field F] [NumberField F] + (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) : + NumberField.discr F ≥ -100 := by + lookup + +-- TEMP signed-discriminant test (TRUE: -163 is the most negative, so no counterexample) +example {F : Type*} [Field F] [NumberField F] + (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) : + NumberField.discr F ≥ -163 := by + lookup + +-- example {W : WeierstrassCurve.Affine ℚ} +-- (hW : 4 ≤ Nat.card (AddCommGroup.torsion W.Point)) : +-- Module.finrank ℤ W.Point ≤ 20 := by +-- sorry From f17990654000bd32fc43a409fd0399b301c74bc4 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 00:52:38 +0100 Subject: [PATCH 02/34] make queries index-friendly, split the tactic into helpers --- LeanBridge/Lookup/Demo.lean | 206 ++++++++++++++++++++++++------------ 1 file changed, 136 insertions(+), 70 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index 08e69861..41e534c1 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -42,6 +42,8 @@ namespace Lookup initialize registerTraceClass `lookup +/-! #### Literals -/ + /-- Extract a natural-number literal from `e`, handling `@OfNat.ofNat _ n _`. -/ def getNatLit? (e : Expr) : Option Nat := match e.getAppFnArgs with @@ -54,48 +56,104 @@ def getIntLit? (e : Expr) : Option Int := | (``Neg.neg, #[_, _, a]) => (getNatLit? a).map fun n => -(n : Int) | _ => (getNatLit? e).map Int.ofNat -/-- A scalar translated to SQL: the SQL text plus the quantities it references, recorded as +/-! #### Comparison operators -/ + +/-- A comparison operator we know how to send to SQL. -/ +inductive Cmp | eq | ne | le | lt | ge | gt + deriving Inhabited, BEq + +namespace Cmp + +/-- The SQL spelling of the operator. -/ +def toSql : Cmp → String + | eq => "=" | ne => "<>" | le => "<=" | lt => "<" | ge => ">=" | gt => ">" + +/-- The operator whose truth value is the logical negation of this one. -/ +def negate : Cmp → Cmp + | eq => ne | ne => eq | le => gt | lt => ge | ge => lt | gt => le + +/-- The operator that holds after swapping the operands (equivalently, after negating both +sides of an order comparison). -/ +def reverse : Cmp → Cmp + | eq => eq | ne => ne | le => ge | lt => gt | ge => le | gt => lt + +end Cmp + +/-! #### Translating Lean expressions to SQL -/ + +/-- A scalar translated to SQL: its text plus the quantities it references, recorded as `(displayName, sqlExpr)` pairs so a counterexample's actual values can be reported. -/ -abbrev SqlScalar := String × Array (String × String) +structure Scalar where + sql : String + refs : Array (String × String) := #[] /-- Translate a scalar Lean expression (applied to the number field) into a SQL scalar over `nf_fields`: a column expression or a numeric literal. -/ -def toSqlScalar (e : Expr) : Option SqlScalar := +def toSqlScalar (e : Expr) : Option Scalar := match e.getAppFnArgs with | (``NumberField.classNumber, _) => - some ("class_number", #[("class number", "class_number")]) + some { sql := "class_number", refs := #[("class number", "class_number")] } | (``Module.finrank, args) => -- `Module.finrank ℚ F` is the degree of the number field `F` over `ℚ`. if h : 0 < args.size then - if args[0].isConstOf ``Rat then some ("degree", #[("degree", "degree")]) else none + if args[0].isConstOf ``Rat then some { sql := "degree", refs := #[("degree", "degree")] } + else none else none | (``abs, args) => args.back?.bind fun x => -- `|NumberField.discr F|` is the absolute discriminant `disc_abs`. match x.getAppFnArgs with - | (``NumberField.discr, _) => some ("disc_abs", #[("|discriminant|", "disc_abs")]) + | (``NumberField.discr, _) => some { sql := "disc_abs", refs := #[("|discriminant|", "disc_abs")] } | _ => none - | (``NumberField.discr, _) => - -- The LMFDB stores the discriminant split as a sign and an absolute value. - some ("(disc_sign * disc_abs)", #[("discriminant", "(disc_sign * disc_abs)")]) - | _ => (getIntLit? e).map fun n => (toString n, #[]) + | _ => (getIntLit? e).map fun n => { sql := toString n } -/-- Match a binary comparison `Prop`, returning the SQL operator and the two sides. -/ -def matchCmp (e : Expr) : Option (String × Expr × Expr) := +/-- Recognise the *signed* discriminant `NumberField.discr F`. -/ +def isDiscr (e : Expr) : Bool := + match e.getAppFnArgs with + | (``NumberField.discr, _) => true + | _ => false + +/-- LMFDB stores the signed discriminant split as `disc_sign * disc_abs`, so translating +`discr OP k` literally as `(disc_sign * disc_abs) OP k` cannot use the indices. Instead we +case-split on the sign into index-friendly comparisons on `disc_abs`: +`discr OP k ⟺ (disc_sign = 1 ∧ disc_abs OP k) ∨ (disc_sign = -1 ∧ disc_abs revOP -k)`. -/ +def discrCond (cmp : Cmp) (k : Int) : Scalar := + { sql := s!"((disc_sign = 1 AND disc_abs {cmp.toSql} {k}) OR \ + (disc_sign = -1 AND disc_abs {cmp.reverse.toSql} {-k}))", + refs := #[("discriminant", "(disc_sign * disc_abs)")] } + +/-- Translate a comparison `cmp a b` into a SQL condition. -/ +def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Scalar := + -- Signed-discriminant comparisons against a literal get the index-friendly treatment. + if isDiscr a then (getIntLit? b).map (discrCond cmp ·) + else if isDiscr b then (getIntLit? a).map (discrCond cmp.reverse ·) + else do + let sa ← toSqlScalar a + let sb ← toSqlScalar b + return { sql := s!"{sa.sql} {cmp.toSql} {sb.sql}", refs := sa.refs ++ sb.refs } + +/-- Match a comparison `Prop`, returning the operator and the two operands. -/ +def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := match e.getAppFnArgs with - | (``Eq, #[_, a, b]) => some ("=", a, b) - | (``LE.le, #[_, _, a, b]) => some ("<=", a, b) - | (``LT.lt, #[_, _, a, b]) => some ("<", a, b) - | (``GE.ge, #[_, _, a, b]) => some (">=", a, b) - | (``GT.gt, #[_, _, a, b]) => some (">", a, b) + | (``Eq, #[_, a, b]) => some (.eq, a, b) + | (``Ne, #[_, a, b]) => some (.ne, a, b) + | (``LE.le, #[_, _, a, b]) => some (.le, a, b) + | (``LT.lt, #[_, _, a, b]) => some (.lt, a, b) + | (``GE.ge, #[_, _, a, b]) => some (.ge, a, b) + | (``GT.gt, #[_, _, a, b]) => some (.gt, a, b) | _ => none -/-- Translate a comparison `Prop` into a SQL condition together with the referenced -quantities. -/ -def toSqlCond (e : Expr) : Option SqlScalar := do - let (op, a, b) ← matchCmp e - let (sa, ra) ← toSqlScalar a - let (sb, rb) ← toSqlScalar b - return (s!"{sa} {op} {sb}", ra ++ rb) +/-- Translate a `Prop` into a SQL condition. -/ +def toSqlCond (e : Expr) : Option Scalar := do + let (cmp, a, b) ← matchCmp e + toSqlCondCmp cmp a b + +/-- Translate the *negation* of a `Prop` into a SQL condition. Negating at the operator level +(rather than wrapping the whole thing in `NOT (...)`) keeps the query index-friendly. -/ +def toSqlCondNeg (e : Expr) : Option Scalar := do + let (cmp, a, b) ← matchCmp e + toSqlCondCmp cmp.negate a b + +/-! #### Reading and rendering a result row -/ /-- The first returned row of an LMFDB `/sql` response, if any. -/ def firstRow? (j : Json) : Option Json := @@ -132,60 +190,68 @@ def formatPoly (coeffs : String) : String := Id.run do out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}") return if out.isEmpty then "0" else out +/-! #### Assembling the query and report -/ + +/-- Deduplicate referenced quantities by their SQL expression, preserving order. -/ +def dedupRefs (refs : Array (String × String)) : Array (String × String) := Id.run do + let mut seen : Array String := #[] + let mut out : Array (String × String) := #[] + for (name, expr) in refs do + unless seen.contains expr do + seen := seen.push expr + out := out.push (name, expr) + return out + +/-- Build the counterexample query: `label`, the defining polynomial, and the actual values +of every referenced quantity (cast to text, since the endpoint cannot serialise bignum +columns directly). -/ +def buildQuery (conds : Array String) (items : Array (String × String)) : String := Id.run do + let mut selects : Array String := #["label", "coeffs::text AS coeffs"] + for i in [0:items.size] do + selects := selects.push s!"({items[i]!.2})::text AS c{i}" + let whereClause := String.intercalate " AND " conds.toList + return s!"SELECT {String.intercalate ", " selects.toList} FROM nf_fields WHERE {whereClause} LIMIT 1" + +/-- Render a counterexample row as a message. -/ +def reportRow (row : Json) (items : Array (String × String)) : MessageData := Id.run do + let label := rowStr row "label" + let mut vals : Array MessageData := #[] + for i in [0:items.size] do + vals := vals.push m!"{items[i]!.1} = {rowStr row s!"c{i}"}" + return m!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ + number field {label}, with minimal polynomial {formatPoly (rowStr row "coeffs")}\n\ + {MessageData.joinSep vals.toList ", "}\n\ + https://www.lmfdb.org/NumberField/{label}" + +/-- Translate the hypotheses in context into SQL conditions, collecting referenced +quantities. -/ +def collectHypotheses : TacticM (Array String × Array (String × String)) := do + let mut conds : Array String := #[] + let mut refs : Array (String × String) := #[] + for ldecl in ← getLCtx do + if ldecl.isImplementationDetail then continue + if let some s := toSqlCond (← instantiateMVars ldecl.type) then + conds := conds.push s.sql + refs := refs ++ s.refs + return (conds, refs) + elab "lookup" : tactic => do let goal ← getMainGoal goal.withContext do - -- Translate each Prop hypothesis we understand into a SQL condition, collecting the - -- quantities (columns) referenced along the way. - let mut conds : Array String := #[] - let mut refs : Array (String × String) := #[] - for ldecl in ← getLCtx do - if ldecl.isImplementationDetail then continue - let ty ← instantiateMVars ldecl.type - if let some (c, r) := toSqlCond ty then - conds := conds.push c - refs := refs ++ r - -- The goal becomes the *negated* condition: we hunt for a row that breaks it. - let goalTy ← instantiateMVars (← goal.getType) - let some (goalCond, goalRefs) := toSqlCond goalTy - | throwError "lookup: don't know how to translate the goal into a SQL query:\n{goalTy}" - refs := refs ++ goalRefs - -- Deduplicate referenced quantities by their SQL expression, preserving order. - let mut seen : Array String := #[] - let mut items : Array (String × String) := #[] - for (name, expr) in refs do - unless seen.contains expr do - seen := seen.push expr - items := items.push (name, expr) - -- Build the SELECT list: label, defining polynomial coeffs, and each referenced - -- quantity, cast to text (the LMFDB endpoint cannot serialise bignum columns directly). - let mut selects : Array String := #["label", "coeffs::text AS coeffs"] - for i in [0:items.size] do - let (_, expr) := items[i]! - selects := selects.push s!"({expr})::text AS c{i}" - let whereClause := String.intercalate " AND " (conds.toList ++ [s!"NOT ({goalCond})"]) - let query := s!"SELECT {String.intercalate ", " selects.toList} \ - FROM nf_fields WHERE {whereClause} LIMIT 1" + let (hypConds, hypRefs) ← collectHypotheses + -- The negated goal is the final condition: we hunt for a row that breaks the goal. + let some goalCond := toSqlCondNeg (← instantiateMVars (← goal.getType)) + | throwError "lookup: don't know how to translate the goal into a SQL query" + let conds := hypConds.push goalCond.sql + let items := dedupRefs (hypRefs ++ goalCond.refs) + let query := buildQuery conds items trace[lookup] "query:\n{query}" - let result ← runSql query - match firstRow? result with + match firstRow? (← runSql query) with | none => -- No counterexample in the database: report, but do *not* close the goal. logInfo m!"lookup: no counterexample found in LMFDB \ (the statement is consistent with the database, but this is not a proof)." - | some row => - let label := rowStr row "label" - let poly := formatPoly (rowStr row "coeffs") - let mut valueLines : Array MessageData := #[] - for i in [0:items.size] do - let (name, _) := items[i]! - let v := rowStr row s!"c{i}" - valueLines := valueLines.push m!"{name} = {v}" - let values := MessageData.joinSep valueLines.toList ", " - throwError m!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ - number field {label}, with minimal polynomial {poly}\n\ - {values}\n\ - https://www.lmfdb.org/NumberField/{label}" + | some row => throwError reportRow row items end Lookup From fdf736a21cdee6bd4dff85d8b60c35f98173cbac Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 01:00:55 +0100 Subject: [PATCH 03/34] generalise to any LMFDB table via a registry --- LeanBridge/Lookup/Demo.lean | 161 +++++++++++++++++++++++++----------- 1 file changed, 113 insertions(+), 48 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index 41e534c1..1393e742 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -81,28 +81,40 @@ end Cmp /-! #### Translating Lean expressions to SQL -/ -/-- A scalar translated to SQL: its text plus the quantities it references, recorded as -`(displayName, sqlExpr)` pairs so a counterexample's actual values can be reported. -/ +/-- A scalar translated to SQL: its text, the quantities it references (recorded as +`(displayName, sqlExpr)` pairs so a counterexample's actual values can be reported), and the +LMFDB table it forces (a literal forces none). -/ structure Scalar where sql : String refs : Array (String × String) := #[] + table : Option String := none -/-- Translate a scalar Lean expression (applied to the number field) into a SQL scalar over -`nf_fields`: a column expression or a numeric literal. -/ +/-- Translate a scalar Lean expression (applied to the LMFDB object) into a SQL scalar: a +column expression tagged with its table, or a numeric literal. -/ def toSqlScalar (e : Expr) : Option Scalar := match e.getAppFnArgs with | (``NumberField.classNumber, _) => - some { sql := "class_number", refs := #[("class number", "class_number")] } + some { sql := "class_number", refs := #[("class number", "class_number")], table := "nf_fields" } | (``Module.finrank, args) => - -- `Module.finrank ℚ F` is the degree of the number field `F` over `ℚ`. + -- `Module.finrank ℚ F` is the degree of a number field; `Module.finrank ℤ W.Point` is + -- the rank of an elliptic curve's Mordell–Weil group. if h : 0 < args.size then - if args[0].isConstOf ``Rat then some { sql := "degree", refs := #[("degree", "degree")] } + if args[0].isConstOf ``Rat then + some { sql := "degree", refs := #[("degree", "degree")], table := "nf_fields" } + else if args[0].isConstOf ``Int then + some { sql := "rank", refs := #[("rank", "rank")], table := "ec_curvedata" } else none else none + | (``Nat.card, args) => + -- `Nat.card ↥(AddCommGroup.torsion W.Point)` is the size of the torsion subgroup. + if args.any fun a => (a.find? (·.isConstOf ``AddCommGroup.torsion)).isSome then + some { sql := "torsion", refs := #[("torsion", "torsion")], table := "ec_curvedata" } + else none | (``abs, args) => args.back?.bind fun x => -- `|NumberField.discr F|` is the absolute discriminant `disc_abs`. match x.getAppFnArgs with - | (``NumberField.discr, _) => some { sql := "disc_abs", refs := #[("|discriminant|", "disc_abs")] } + | (``NumberField.discr, _) => + some { sql := "disc_abs", refs := #[("|discriminant|", "disc_abs")], table := "nf_fields" } | _ => none | _ => (getIntLit? e).map fun n => { sql := toString n } @@ -119,7 +131,7 @@ case-split on the sign into index-friendly comparisons on `disc_abs`: def discrCond (cmp : Cmp) (k : Int) : Scalar := { sql := s!"((disc_sign = 1 AND disc_abs {cmp.toSql} {k}) OR \ (disc_sign = -1 AND disc_abs {cmp.reverse.toSql} {-k}))", - refs := #[("discriminant", "(disc_sign * disc_abs)")] } + refs := #[("discriminant", "(disc_sign * disc_abs)")], table := "nf_fields" } /-- Translate a comparison `cmp a b` into a SQL condition. -/ def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Scalar := @@ -129,7 +141,8 @@ def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Scalar := else do let sa ← toSqlScalar a let sb ← toSqlScalar b - return { sql := s!"{sa.sql} {cmp.toSql} {sb.sql}", refs := sa.refs ++ sb.refs } + return { sql := s!"{sa.sql} {cmp.toSql} {sb.sql}", refs := sa.refs ++ sb.refs, + table := sa.table <|> sb.table } /-- Match a comparison `Prop`, returning the operator and the two operands. -/ def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := @@ -190,6 +203,56 @@ def formatPoly (coeffs : String) : String := Id.run do out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}") return if out.isEmpty then "0" else out +/-! #### LMFDB tables + +Each supported object family corresponds to a table, knowing how to select its label and +descriptive data, render that data, and build a link to the LMFDB page. -/ + +/-- Per-table knowledge needed to query and report a counterexample. -/ +structure TableInfo where + /-- The SQL table name. -/ + table : String + /-- The column holding the LMFDB label (selected `AS label`). -/ + labelCol : String + /-- Extra SELECT fragments for the descriptive data (e.g. the defining polynomial). -/ + descSelects : Array String + /-- Render the descriptive data of a result row. -/ + describe : Json → MessageData + /-- Build the LMFDB page URL from a label. -/ + url : String → String + +/-- LMFDB elliptic-curve labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. -/ +def ecUrl (label : String) : String := + match label.splitOn "." with + | [conductor, iso] => + let letters := iso.takeWhile Char.isAlpha + let number := iso.dropWhile Char.isAlpha + s!"https://www.lmfdb.org/EllipticCurve/Q/{conductor}/{letters}/{number}" + | _ => s!"https://www.lmfdb.org/EllipticCurve/Q/{label}" + +/-- Number fields. -/ +def nfFields : TableInfo where + table := "nf_fields" + labelCol := "label" + descSelects := #["coeffs::text AS coeffs"] + describe row := m!"number field {rowStr row "label"}, with minimal polynomial \ + {formatPoly (rowStr row "coeffs")}" + url label := s!"https://www.lmfdb.org/NumberField/{label}" + +/-- Elliptic curves over `ℚ`. -/ +def ecCurvedata : TableInfo where + table := "ec_curvedata" + labelCol := "lmfdb_label" + descSelects := #["ainvs::text AS ainvs"] + describe row := m!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" + url := ecUrl + +/-- The table configuration for a table name. -/ +def tableInfo? : String → Option TableInfo + | "nf_fields" => some nfFields + | "ec_curvedata" => some ecCurvedata + | _ => none + /-! #### Assembling the query and report -/ /-- Deduplicate referenced quantities by their SQL expression, preserving order. -/ @@ -202,56 +265,62 @@ def dedupRefs (refs : Array (String × String)) : Array (String × String) := Id out := out.push (name, expr) return out -/-- Build the counterexample query: `label`, the defining polynomial, and the actual values -of every referenced quantity (cast to text, since the endpoint cannot serialise bignum -columns directly). -/ -def buildQuery (conds : Array String) (items : Array (String × String)) : String := Id.run do - let mut selects : Array String := #["label", "coeffs::text AS coeffs"] +/-- Build the counterexample query: the label, the descriptive data, and the actual values of +every referenced quantity (cast to text, since the endpoint cannot serialise bignum columns +directly). -/ +def buildQuery (info : TableInfo) (conds : Array String) (items : Array (String × String)) : + String := Id.run do + let mut selects : Array String := #[s!"{info.labelCol} AS label"] ++ info.descSelects for i in [0:items.size] do selects := selects.push s!"({items[i]!.2})::text AS c{i}" let whereClause := String.intercalate " AND " conds.toList - return s!"SELECT {String.intercalate ", " selects.toList} FROM nf_fields WHERE {whereClause} LIMIT 1" + return s!"SELECT {String.intercalate ", " selects.toList} FROM {info.table} \ + WHERE {whereClause} LIMIT 1" /-- Render a counterexample row as a message. -/ -def reportRow (row : Json) (items : Array (String × String)) : MessageData := Id.run do - let label := rowStr row "label" +def reportRow (info : TableInfo) (row : Json) (items : Array (String × String)) : + MessageData := Id.run do let mut vals : Array MessageData := #[] for i in [0:items.size] do vals := vals.push m!"{items[i]!.1} = {rowStr row s!"c{i}"}" return m!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ - number field {label}, with minimal polynomial {formatPoly (rowStr row "coeffs")}\n\ + {info.describe row}\n\ {MessageData.joinSep vals.toList ", "}\n\ - https://www.lmfdb.org/NumberField/{label}" + {info.url (rowStr row "label")}" -/-- Translate the hypotheses in context into SQL conditions, collecting referenced -quantities. -/ -def collectHypotheses : TacticM (Array String × Array (String × String)) := do - let mut conds : Array String := #[] - let mut refs : Array (String × String) := #[] +/-- Translate the hypotheses in context into SQL condition scalars. -/ +def collectHypotheses : TacticM (Array Scalar) := do + let mut out : Array Scalar := #[] for ldecl in ← getLCtx do if ldecl.isImplementationDetail then continue if let some s := toSqlCond (← instantiateMVars ldecl.type) then - conds := conds.push s.sql - refs := refs ++ s.refs - return (conds, refs) + out := out.push s + return out elab "lookup" : tactic => do let goal ← getMainGoal goal.withContext do - let (hypConds, hypRefs) ← collectHypotheses -- The negated goal is the final condition: we hunt for a row that breaks the goal. let some goalCond := toSqlCondNeg (← instantiateMVars (← goal.getType)) | throwError "lookup: don't know how to translate the goal into a SQL query" - let conds := hypConds.push goalCond.sql - let items := dedupRefs (hypRefs ++ goalCond.refs) - let query := buildQuery conds items + let conditions := (← collectHypotheses).push goalCond + -- Every condition must point at the same LMFDB table. + let info ← match (conditions.filterMap (·.table)).toList.dedup with + | [t] => match tableInfo? t with + | some info => pure info + | none => throwError "lookup: no table configuration for `{t}`" + | [] => throwError "lookup: couldn't determine which LMFDB table the goal is about" + | ts => throwError "lookup: the goal mixes multiple LMFDB object types {ts}" + let conds := conditions.map (·.sql) + let items := dedupRefs (conditions.foldl (fun acc s => acc ++ s.refs) #[]) + let query := buildQuery info conds items trace[lookup] "query:\n{query}" match firstRow? (← runSql query) with | none => -- No counterexample in the database: report, but do *not* close the goal. logInfo m!"lookup: no counterexample found in LMFDB \ (the statement is consistent with the database, but this is not a proof)." - | some row => throwError reportRow row items + | some row => throwError reportRow info row items end Lookup @@ -292,19 +361,15 @@ example {F : Type*} [Field F] [NumberField F] |NumberField.discr F| ≤ 163 := by lookup --- TEMP signed-discriminant test (FALSE: the disc = -163 field is a counterexample) -example {F : Type*} [Field F] [NumberField F] - (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) : - NumberField.discr F ≥ -100 := by +-- Signed-discriminant queries are supported too (the DB stores `disc_sign * disc_abs`, +-- and `lookup` case-splits on the sign so the query stays index-friendly): +-- `NumberField.discr F ≥ -100` finds the counterexample `2.0.163.1` (discriminant -163), +-- while `NumberField.discr F ≥ -163` finds none. + +-- A non-number-field example: `lookup` dispatches to the `ec_curvedata` table. This claim is +-- false — e.g. curve `117.a4` has a 4-torsion point yet positive rank — so `lookup` surfaces +-- it (with the curve's a-invariants and a link). The `≤ 20` version instead finds nothing. +example {W : WeierstrassCurve.Affine ℚ} + (hW : 4 ≤ Nat.card (AddCommGroup.torsion W.Point)) : + Module.finrank ℤ W.Point ≤ 0 := by lookup - --- TEMP signed-discriminant test (TRUE: -163 is the most negative, so no counterexample) -example {F : Type*} [Field F] [NumberField F] - (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) : - NumberField.discr F ≥ -163 := by - lookup - --- example {W : WeierstrassCurve.Affine ℚ} --- (hW : 4 ≤ Nat.card (AddCommGroup.torsion W.Point)) : --- Module.finrank ℤ W.Point ≤ 20 := by --- sorry From d28527bc9b293273a2c7d0db41bd0af8cd02769e Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 01:02:58 +0100 Subject: [PATCH 04/34] warn on hypotheses we can't translate --- LeanBridge/Lookup/Demo.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index 1393e742..c51448db 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -288,13 +288,20 @@ def reportRow (info : TableInfo) (row : Json) (items : Array (String × String)) {MessageData.joinSep vals.toList ", "}\n\ {info.url (rowStr row "label")}" -/-- Translate the hypotheses in context into SQL condition scalars. -/ +/-- Translate the hypotheses in context into SQL condition scalars. A hypothesis that *is* a +comparison but that we cannot translate is reported as a warning (and dropped), since silently +ignoring it would weaken any "no counterexample" conclusion. -/ def collectHypotheses : TacticM (Array Scalar) := do let mut out : Array Scalar := #[] for ldecl in ← getLCtx do if ldecl.isImplementationDetail then continue - if let some s := toSqlCond (← instantiateMVars ldecl.type) then - out := out.push s + let ty ← instantiateMVars ldecl.type + match toSqlCond ty with + | some s => out := out.push s + | none => + if (matchCmp ty).isSome then + logWarning m!"lookup: ignoring hypothesis `{ldecl.userName}` : {ty}\n\ + (couldn't translate it to a SQL condition, so the search ignores this constraint)." return out elab "lookup" : tactic => do From 0271b27f9289f03b8ab47f22763b14d030658a3f Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 01:08:19 +0100 Subject: [PATCH 05/34] support finite groups and boolean properties --- LeanBridge/Lookup/Demo.lean | 68 ++++++++++++++++++++++++++++++++----- 1 file changed, 60 insertions(+), 8 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index c51448db..0d0afe2c 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -155,16 +155,53 @@ def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := | (``GT.gt, #[_, _, a, b]) => some (.gt, a, b) | _ => none +/-- The de Bruijn index of a bound variable, if `e` is one. -/ +def bvarIdx? : Expr → Option Nat + | .bvar n => some n + | _ => none + +/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` (i.e. "the group is +abelian"), allowing for the two multiplications to have swapped operands. -/ +def isAbelianPattern (e : Expr) : Bool := Id.run do + let .forallE _ _ (.forallE _ _ body _) _ := e | return false + let (``Eq, #[_, lhs, rhs]) := body.getAppFnArgs | return false + let (``HMul.hMul, la) := lhs.getAppFnArgs | return false + let (``HMul.hMul, ra) := rhs.getAppFnArgs | return false + if la.size < 2 || ra.size < 2 then return false + let some l1 := bvarIdx? la[la.size - 2]! | return false + let some l2 := bvarIdx? la[la.size - 1]! | return false + let some r1 := bvarIdx? ra[ra.size - 2]! | return false + let some r2 := bvarIdx? ra[ra.size - 1]! | return false + return l1 == r2 && l2 == r1 && l1 != l2 + +/-- Translate a boolean-valued property of the object into a SQL boolean-column comparison. +`positive := false` asks for the property to *fail* (`= 'f'`). -/ +def toSqlPredicate (positive : Bool) (e : Expr) : Option Scalar := + let tf := if positive then "'t'" else "'f'" + match e.getAppFnArgs with + | (``IsSimpleGroup, _) => + some { sql := s!"simple = {tf}", refs := #[("simple", "simple")], table := "gps_groups" } + | _ => + if isAbelianPattern e then + some { sql := s!"abelian = {tf}", refs := #[("abelian", "abelian")], table := "gps_groups" } + else none + +/-- Translate a `Prop` into a SQL condition. `positive := false` translates its negation +instead; pushing the negation down to the operator / boolean value (rather than wrapping the +whole condition in SQL `NOT (...)`) keeps the query index-friendly. -/ +partial def toCond (positive : Bool) (e : Expr) : Option Scalar := + match e.getAppFnArgs with + | (``Not, #[p]) => toCond (!positive) p + | _ => + match matchCmp e with + | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b + | none => toSqlPredicate positive e + /-- Translate a `Prop` into a SQL condition. -/ -def toSqlCond (e : Expr) : Option Scalar := do - let (cmp, a, b) ← matchCmp e - toSqlCondCmp cmp a b +def toSqlCond (e : Expr) : Option Scalar := toCond true e -/-- Translate the *negation* of a `Prop` into a SQL condition. Negating at the operator level -(rather than wrapping the whole thing in `NOT (...)`) keeps the query index-friendly. -/ -def toSqlCondNeg (e : Expr) : Option Scalar := do - let (cmp, a, b) ← matchCmp e - toSqlCondCmp cmp.negate a b +/-- Translate the *negation* of a `Prop` into a SQL condition (used for the goal). -/ +def toSqlCondNeg (e : Expr) : Option Scalar := toCond false e /-! #### Reading and rendering a result row -/ @@ -247,10 +284,19 @@ def ecCurvedata : TableInfo where describe row := m!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" url := ecUrl +/-- Finite groups. -/ +def gpsGroups : TableInfo where + table := "gps_groups" + labelCol := "label" + descSelects := #["tex_name::text AS tex_name"] + describe row := m!"group {rowStr row "label"} ({rowStr row "tex_name"})" + url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" + /-- The table configuration for a table name. -/ def tableInfo? : String → Option TableInfo | "nf_fields" => some nfFields | "ec_curvedata" => some ecCurvedata + | "gps_groups" => some gpsGroups | _ => none /-! #### Assembling the query and report -/ @@ -380,3 +426,9 @@ example {W : WeierstrassCurve.Affine ℚ} (hW : 4 ≤ Nat.card (AddCommGroup.torsion W.Point)) : Module.finrank ℤ W.Point ≤ 0 := by lookup + +-- A third object family: `lookup` dispatches boolean properties to `gps_groups`. "Every +-- simple group is nonabelian" is false — the cyclic groups of prime order are simple and +-- abelian — so `lookup` surfaces such a group. +example {G : Type*} [Group G] [IsSimpleGroup G] : ¬ ∀ a b : G, a * b = b * a := by + lookup From bb9fefe086f31ae8fb945ea43638437ee34d782f Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 01:08:38 +0100 Subject: [PATCH 06/34] linkify the counterexample as a markdown link --- LeanBridge/Lookup/DECISIONS.md | 9 +++++---- LeanBridge/Lookup/Demo.lean | 4 +++- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/LeanBridge/Lookup/DECISIONS.md b/LeanBridge/Lookup/DECISIONS.md index 31410e47..09fbe7b5 100644 --- a/LeanBridge/Lookup/DECISIONS.md +++ b/LeanBridge/Lookup/DECISIONS.md @@ -12,10 +12,11 @@ parentheses or with trailing punctuation attached. - Option B: emit the URL bare on its own line with no surrounding punctuation, relying on the infoview's auto-linkification. -**Chosen: Option B.** The previous message put the URL inside `(...)`, which defeats -auto-linkification; isolating it on its own line is the minimal fix and matches how other -Lean tactics surface URLs. If it turns out the infoview still does not linkify it, revisit -with a widget. +**Update — chosen: markdown link.** A bare URL on its own line still did *not* render as a +clickable link in the infoview. The infoview does render message markdown, so the report now +uses an explicit markdown link `[` element and embedded into the +thrown error via `MessageData.ofHtml`, which renders the HTML (clickable anchor) in the +infoview and falls back to a plain-text `alt` everywhere else (e.g. the LSP diagnostic text). +This is distinct from the project's existing `LMFDBWidget` (which the user noted does not +help); it uses only the stock `HtmlDisplay` component that ships with ProofWidgets. ## Reporting signed-discriminant counterexamples (tasks 3 & 7) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index 851be013..c5a1b04a 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -1,4 +1,5 @@ import Mathlib +import ProofWidgets.Component.HtmlDisplay -- https://www.lmfdb.org/api/nf_fields/?_format=json&_offset=0 @@ -253,8 +254,8 @@ structure TableInfo where labelCol : String /-- Extra SELECT fragments for the descriptive data (e.g. the defining polynomial). -/ descSelects : Array String - /-- Render the descriptive data of a result row. -/ - describe : Json → MessageData + /-- Render the descriptive data of a result row as plain text. -/ + describe : Json → String /-- Build the LMFDB page URL from a label. -/ url : String → String @@ -272,7 +273,7 @@ def nfFields : TableInfo where table := "nf_fields" labelCol := "label" descSelects := #["coeffs::text AS coeffs"] - describe row := m!"number field {rowStr row "label"}, with minimal polynomial \ + describe row := s!"number field {rowStr row "label"}, with minimal polynomial \ {formatPoly (rowStr row "coeffs")}" url label := s!"https://www.lmfdb.org/NumberField/{label}" @@ -281,7 +282,7 @@ def ecCurvedata : TableInfo where table := "ec_curvedata" labelCol := "lmfdb_label" descSelects := #["ainvs::text AS ainvs"] - describe row := m!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" + describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" url := ecUrl /-- Finite groups. -/ @@ -289,7 +290,7 @@ def gpsGroups : TableInfo where table := "gps_groups" labelCol := "label" descSelects := #["tex_name::text AS tex_name"] - describe row := m!"group {rowStr row "label"} ({rowStr row "tex_name"})" + describe row := s!"group {rowStr row "label"} ({rowStr row "tex_name"})" url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" /-- The table configuration for a table name. -/ @@ -323,18 +324,35 @@ def buildQuery (info : TableInfo) (conds : Array String) (items : Array (String return s!"SELECT {String.intercalate ", " selects.toList} FROM {info.table} \ WHERE {whereClause} LIMIT 1" -/-- Render a counterexample row as a message. -/ -def reportRow (info : TableInfo) (row : Json) (items : Array (String × String)) : - MessageData := Id.run do - let mut vals : Array MessageData := #[] +/-- The "name = value" strings for the referenced quantities of a result row. -/ +def valueStrs (row : Json) (items : Array (String × String)) : Array String := Id.run do + let mut out : Array String := #[] for i in [0:items.size] do - vals := vals.push m!"{items[i]!.1} = {rowStr row s!"c{i}"}" + out := out.push s!"{items[i]!.1} = {rowStr row s!"c{i}"}" + return out + +open ProofWidgets in +/-- Render a counterexample row as interactive HTML, including a clickable LMFDB link. +A bare or markdown URL in a `MessageData` is not linkified by the infoview, so we build an +actual `` element and embed it via `MessageData.ofHtml`. -/ +def reportHtml (info : TableInfo) (row : Json) (items : Array (String × String)) : Html := let label := rowStr row "label" - -- A markdown link renders as a clickable anchor in the infoview (a bare URL does not). - return m!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ + Html.element "div" #[] #[ + .text "lookup: the statement is FALSE — LMFDB has a counterexample.", + .element "br" #[] #[], + .text (info.describe row), + .element "br" #[] #[], + .text (", ".intercalate (valueStrs row items).toList), + .element "br" #[] #[], + .element "a" #[("href", toJson (info.url label))] #[.text s!"{label} on LMFDB"] + ] + +/-- A plain-text fallback for the counterexample, shown where HTML cannot render. -/ +def reportAlt (info : TableInfo) (row : Json) (items : Array (String × String)) : String := + s!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ {info.describe row}\n\ - {MessageData.joinSep vals.toList ", "}\n\ - [{label} on LMFDB]({info.url label})" + {", ".intercalate (valueStrs row items).toList}\n\ + {info.url (rowStr row "label")}" /-- Translate the hypotheses in context into SQL condition scalars. A hypothesis that *is* a comparison but that we cannot translate is reported as a warning (and dropped), since silently @@ -375,7 +393,8 @@ elab "lookup" : tactic => do -- No counterexample in the database: report, but do *not* close the goal. logInfo m!"lookup: no counterexample found in LMFDB \ (the statement is consistent with the database, but this is not a proof)." - | some row => throwError reportRow info row items + | some row => + throwError (← MessageData.ofHtml (reportHtml info row items) (reportAlt info row items)) end Lookup From 8d71dcc5693eaa55bc8e76043131b8529ecc470e Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 01:23:41 +0100 Subject: [PATCH 08/34] return the smallest counterexample --- LeanBridge/Lookup/Demo.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index c5a1b04a..fb4baecd 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -258,6 +258,8 @@ structure TableInfo where describe : Json → String /-- Build the LMFDB page URL from a label. -/ url : String → String + /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/ + orderBy : String /-- LMFDB elliptic-curve labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. -/ def ecUrl (label : String) : String := @@ -276,6 +278,7 @@ def nfFields : TableInfo where describe row := s!"number field {rowStr row "label"}, with minimal polynomial \ {formatPoly (rowStr row "coeffs")}" url label := s!"https://www.lmfdb.org/NumberField/{label}" + orderBy := "disc_abs" /-- Elliptic curves over `ℚ`. -/ def ecCurvedata : TableInfo where @@ -284,6 +287,7 @@ def ecCurvedata : TableInfo where descSelects := #["ainvs::text AS ainvs"] describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" url := ecUrl + orderBy := "conductor" /-- Finite groups. -/ def gpsGroups : TableInfo where @@ -292,6 +296,8 @@ def gpsGroups : TableInfo where descSelects := #["tex_name::text AS tex_name"] describe row := s!"group {rowStr row "label"} ({rowStr row "tex_name"})" url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" + -- `order` is a SQL reserved word, so it must be quoted. + orderBy := "\"order\"" /-- The table configuration for a table name. -/ def tableInfo? : String → Option TableInfo @@ -322,7 +328,7 @@ def buildQuery (info : TableInfo) (conds : Array String) (items : Array (String selects := selects.push s!"({items[i]!.2})::text AS c{i}" let whereClause := String.intercalate " AND " conds.toList return s!"SELECT {String.intercalate ", " selects.toList} FROM {info.table} \ - WHERE {whereClause} LIMIT 1" + WHERE {whereClause} ORDER BY {info.orderBy} LIMIT 1" /-- The "name = value" strings for the referenced quantities of a result row. -/ def valueStrs (row : Json) (items : Array (String × String)) : Array String := Id.run do From 72aec434e0f440662bad8b81c1b570b84d6ee196 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 01:23:54 +0100 Subject: [PATCH 09/34] demo a rank-2 curve with trivial torsion --- LeanBridge/Lookup/Demo.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index fb4baecd..a0f6ac84 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -454,6 +454,13 @@ example {W : WeierstrassCurve.Affine ℚ} Module.finrank ℤ W.Point ≤ 0 := by lookup +-- "Every elliptic curve over ℚ with rank at least 2 has trivial torsion subgroup." This is +-- false: e.g. curve `1088.a1` has rank 2 and a 2-torsion point. +example {W : WeierstrassCurve.Affine ℚ} + (hW : 2 ≤ Module.finrank ℤ W.Point) : + Nat.card (AddCommGroup.torsion W.Point) = 1 := by + lookup + -- A third object family: `lookup` dispatches boolean properties to `gps_groups`. "Every -- simple group is nonabelian" is false — the cyclic groups of prime order are simple and -- abelian — so `lookup` surfaces such a group. From 1d516edb3558749b849d4d6b462648911464831d Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 01:36:19 +0100 Subject: [PATCH 10/34] support class group and torsion structure --- LeanBridge/Lookup/Demo.lean | 61 +++++++++++++++++++++++++++++++++++-- 1 file changed, 58 insertions(+), 3 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index a0f6ac84..ddbb756d 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -175,13 +175,52 @@ def isAbelianPattern (e : Expr) : Bool := Id.run do let some r2 := bvarIdx? ra[ra.size - 1]! | return false return l1 == r2 && l2 == r1 && l1 != l2 -/-- Translate a boolean-valued property of the object into a SQL boolean-column comparison. -`positive := false` asks for the property to *fail* (`= 'f'`). -/ -def toSqlPredicate (positive : Bool) (e : Expr) : Option Scalar := +/-- Whether `e` mentions the constant `n` anywhere. -/ +def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome + +/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` +wrappers stripped) as its list of moduli, in the order written. -/ +partial def cyclicFactors? (e : Expr) : Option (Array Nat) := + match e.getAppFnArgs with + | (``ZMod, #[n]) => (getNatLit? n).map (#[·]) + | (``Multiplicative, #[a]) => cyclicFactors? a + | (``Prod, #[a, b]) => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) + | _ => none + +/-- LMFDB encodes the torsion structure as a brace array `{2,4}` and the ideal class group as +a JSON bracket array `[2, 2]`. -/ +def fmtBraces (f : Array Nat) : String := "{" ++ ",".intercalate (f.toList.map toString) ++ "}" +def fmtBrackets (f : Array Nat) : String := "[" ++ ", ".intercalate (f.toList.map toString) ++ "]" + +/-- Translate an abelian-group-structure claim `lhs ≃ rhs` (where `rhs` is a product of +cyclics) into an invariant-factor column comparison; `positive := false` negates it (`<>`). -/ +def structCond (positive : Bool) (lhs rhs : Expr) (lhsConst : Name) + (col display table : String) (fmt : Array Nat → String) : Option Scalar := do + guard (containsConst lhs lhsConst) + let factors ← cyclicFactors? rhs + return { sql := s!"{col} {if positive then "=" else "<>"} '{fmt factors}'", + refs := #[(display, col.replace "::text" "")], table := table } + +/-- Translate a property of the object into a SQL condition. Handles boolean flags +(`IsSimpleGroup`, the abelian pattern) and abelian-group-structure isomorphisms (torsion +subgroup via `≃+`, ideal class group via `≃*`), optionally wrapped in `Nonempty`. +`positive := false` asks for the property to *fail*. -/ +partial def toSqlPredicate (positive : Bool) (e : Expr) : Option Scalar := let tf := if positive then "'t'" else "'f'" match e.getAppFnArgs with + | (``Nonempty, #[inner]) => toSqlPredicate positive inner | (``IsSimpleGroup, _) => some { sql := s!"simple = {tf}", refs := #[("simple", "simple")], table := "gps_groups" } + | (``AddEquiv, args) => + if 2 ≤ args.size then + structCond positive args[0]! args[1]! ``AddCommGroup.torsion + "torsion_structure" "torsion structure" "ec_curvedata" fmtBraces + else none + | (``MulEquiv, args) => + if 2 ≤ args.size then + structCond positive args[0]! args[1]! ``ClassGroup + "class_group::text" "class group" "nf_fields" fmtBrackets + else none | _ => if isAbelianPattern e then some { sql := s!"abelian = {tf}", refs := #[("abelian", "abelian")], table := "gps_groups" } @@ -446,6 +485,14 @@ example {F : Type*} [Field F] [NumberField F] -- `NumberField.discr F ≥ -100` finds the counterexample `2.0.163.1` (discriminant -163), -- while `NumberField.discr F ≥ -163` finds none. +-- The ideal class group *structure* (LMFDB's `class_group`) is supported via `≃*`: "every +-- degree-2 field of class number 4 has cyclic class group ℤ/4" is false — some are C₂ × C₂. +-- The class group is multiplicative, so the right-hand side carries `Multiplicative`. +example {F : Type*} [Field F] [NumberField F] + (h1 : NumberField.classNumber F = 4) (h2 : Module.finrank ℚ F = 2) : + Nonempty (ClassGroup (NumberField.RingOfIntegers F) ≃* Multiplicative (ZMod 4)) := by + lookup + -- A non-number-field example: `lookup` dispatches to the `ec_curvedata` table. This claim is -- false — e.g. curve `117.a4` has a 4-torsion point yet positive rank — so `lookup` surfaces -- it (with the curve's a-invariants and a link). The `≤ 20` version instead finds nothing. @@ -461,6 +508,14 @@ example {W : WeierstrassCurve.Affine ℚ} Nat.card (AddCommGroup.torsion W.Point) = 1 := by lookup +-- Group *structure* is supported too (LMFDB's `torsion_structure`): "every curve whose +-- torsion subgroup has order 4 has torsion subgroup ≅ ℤ/4" is false — some are ℤ/2 × ℤ/2. +-- The torsion subgroup is additive, hence `≃+`. +example {W : WeierstrassCurve.Affine ℚ} + (hW : Nat.card (AddCommGroup.torsion W.Point) = 4) : + Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 4) := by + lookup + -- A third object family: `lookup` dispatches boolean properties to `gps_groups`. "Every -- simple group is nonabelian" is false — the cyclic groups of prime order are simple and -- abelian — so `lookup` surfaces such a group. From 4dc8e69f5bd519b128ca13d81203025fcd1c21c0 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 01:56:09 +0100 Subject: [PATCH 11/34] move each table's mappings into its TableInfo --- LeanBridge/Lookup/Demo.lean | 313 +++++++++++++++++++----------------- 1 file changed, 167 insertions(+), 146 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index ddbb756d..a8af84b1 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -47,14 +47,14 @@ initialize registerTraceClass `lookup /-- Extract a natural-number literal from `e`, handling `@OfNat.ofNat _ n _`. -/ def getNatLit? (e : Expr) : Option Nat := - match e.getAppFnArgs with - | (``OfNat.ofNat, #[_, n, _]) => n.rawNatLit? + match_expr e with + | OfNat.ofNat _ n _ => n.rawNatLit? | _ => e.rawNatLit? /-- Extract an integer literal, handling a leading negation `@Neg.neg _ _ n`. -/ def getIntLit? (e : Expr) : Option Int := - match e.getAppFnArgs with - | (``Neg.neg, #[_, _, a]) => (getNatLit? a).map fun n => -(n : Int) + match_expr e with + | Neg.neg _ _ a => (getNatLit? a).map fun n => -(n : Int) | _ => (getNatLit? e).map Int.ofNat /-! #### Comparison operators -/ @@ -80,111 +80,57 @@ def reverse : Cmp → Cmp end Cmp -/-! #### Translating Lean expressions to SQL -/ +/-! #### Translating Lean expressions to SQL -/-- A scalar translated to SQL: its text, the quantities it references (recorded as -`(displayName, sqlExpr)` pairs so a counterexample's actual values can be reported), and the -LMFDB table it forces (a literal forces none). -/ -structure Scalar where +A `Column` is a quantity of an object (an SQL column expression plus a display name); a `Cond` +is a translated SQL boolean condition. The recognisers that map Lean expressions to columns +and conditions live *with each table* in the registry below, so adding a column or property to +a table is a local, one-line change. The generic plumbing here is table-agnostic. -/ + +/-- A scalar quantity of an object: an SQL column expression and a human-readable name. A +quantity stored split as `sign * |·|` records those two columns in `signed?`, so comparisons +against a literal can be made index-friendly. -/ +structure Column where + sql : String + display : String + signed? : Option (String × String) := none + +/-- A translated SQL condition: the boolean SQL, the columns it references (as +`(displayName, selectExpr)` pairs, for reporting), and the LMFDB table it forces. -/ +structure Cond where sql : String refs : Array (String × String) := #[] table : Option String := none -/-- Translate a scalar Lean expression (applied to the LMFDB object) into a SQL scalar: a -column expression tagged with its table, or a numeric literal. -/ -def toSqlScalar (e : Expr) : Option Scalar := - match e.getAppFnArgs with - | (``NumberField.classNumber, _) => - some { sql := "class_number", refs := #[("class number", "class_number")], table := "nf_fields" } - | (``Module.finrank, args) => - -- `Module.finrank ℚ F` is the degree of a number field; `Module.finrank ℤ W.Point` is - -- the rank of an elliptic curve's Mordell–Weil group. - if h : 0 < args.size then - if args[0].isConstOf ``Rat then - some { sql := "degree", refs := #[("degree", "degree")], table := "nf_fields" } - else if args[0].isConstOf ``Int then - some { sql := "rank", refs := #[("rank", "rank")], table := "ec_curvedata" } - else none - else none - | (``Nat.card, args) => - -- `Nat.card ↥(AddCommGroup.torsion W.Point)` is the size of the torsion subgroup. - if args.any fun a => (a.find? (·.isConstOf ``AddCommGroup.torsion)).isSome then - some { sql := "torsion", refs := #[("torsion", "torsion")], table := "ec_curvedata" } - else none - | (``abs, args) => args.back?.bind fun x => - -- `|NumberField.discr F|` is the absolute discriminant `disc_abs`. - match x.getAppFnArgs with - | (``NumberField.discr, _) => - some { sql := "disc_abs", refs := #[("|discriminant|", "disc_abs")], table := "nf_fields" } - | _ => none - | _ => (getIntLit? e).map fun n => { sql := toString n } - -/-- Recognise the *signed* discriminant `NumberField.discr F`. -/ -def isDiscr (e : Expr) : Bool := - match e.getAppFnArgs with - | (``NumberField.discr, _) => true - | _ => false +/-- Build a `Column`. -/ +def col (sql display : String) (signed? : Option (String × String) := none) : Column := + { sql, display, signed? } -/-- LMFDB stores the signed discriminant split as `disc_sign * disc_abs`, so translating -`discr OP k` literally as `(disc_sign * disc_abs) OP k` cannot use the indices. Instead we -case-split on the sign into index-friendly comparisons on `disc_abs`: -`discr OP k ⟺ (disc_sign = 1 ∧ disc_abs OP k) ∨ (disc_sign = -1 ∧ disc_abs revOP -k)`. -/ -def discrCond (cmp : Cmp) (k : Int) : Scalar := - { sql := s!"((disc_sign = 1 AND disc_abs {cmp.toSql} {k}) OR \ - (disc_sign = -1 AND disc_abs {cmp.reverse.toSql} {-k}))", - refs := #[("discriminant", "(disc_sign * disc_abs)")], table := "nf_fields" } - -/-- Translate a comparison `cmp a b` into a SQL condition. -/ -def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Scalar := - -- Signed-discriminant comparisons against a literal get the index-friendly treatment. - if isDiscr a then (getIntLit? b).map (discrCond cmp ·) - else if isDiscr b then (getIntLit? a).map (discrCond cmp.reverse ·) - else do - let sa ← toSqlScalar a - let sb ← toSqlScalar b - return { sql := s!"{sa.sql} {cmp.toSql} {sb.sql}", refs := sa.refs ++ sb.refs, - table := sa.table <|> sb.table } +/-- A boolean-flag condition `column = 't'` (or `column = 'f'` when negated). -/ +def boolCol (positive : Bool) (column : String) : Cond := + { sql := s!"{column} = {if positive then "'t'" else "'f'"}", refs := #[(column, column)] } /-- Match a comparison `Prop`, returning the operator and the two operands. -/ def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := - match e.getAppFnArgs with - | (``Eq, #[_, a, b]) => some (.eq, a, b) - | (``Ne, #[_, a, b]) => some (.ne, a, b) - | (``LE.le, #[_, _, a, b]) => some (.le, a, b) - | (``LT.lt, #[_, _, a, b]) => some (.lt, a, b) - | (``GE.ge, #[_, _, a, b]) => some (.ge, a, b) - | (``GT.gt, #[_, _, a, b]) => some (.gt, a, b) + match_expr e with + | Eq _ a b => some (.eq, a, b) + | Ne _ a b => some (.ne, a, b) + | LE.le _ _ a b => some (.le, a, b) + | LT.lt _ _ a b => some (.lt, a, b) + | GE.ge _ _ a b => some (.ge, a, b) + | GT.gt _ _ a b => some (.gt, a, b) | _ => none -/-- The de Bruijn index of a bound variable, if `e` is one. -/ -def bvarIdx? : Expr → Option Nat - | .bvar n => some n - | _ => none - -/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` (i.e. "the group is -abelian"), allowing for the two multiplications to have swapped operands. -/ -def isAbelianPattern (e : Expr) : Bool := Id.run do - let .forallE _ _ (.forallE _ _ body _) _ := e | return false - let (``Eq, #[_, lhs, rhs]) := body.getAppFnArgs | return false - let (``HMul.hMul, la) := lhs.getAppFnArgs | return false - let (``HMul.hMul, ra) := rhs.getAppFnArgs | return false - if la.size < 2 || ra.size < 2 then return false - let some l1 := bvarIdx? la[la.size - 2]! | return false - let some l2 := bvarIdx? la[la.size - 1]! | return false - let some r1 := bvarIdx? ra[ra.size - 2]! | return false - let some r2 := bvarIdx? ra[ra.size - 1]! | return false - return l1 == r2 && l2 == r1 && l1 != l2 - /-- Whether `e` mentions the constant `n` anywhere. -/ def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome /-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` wrappers stripped) as its list of moduli, in the order written. -/ partial def cyclicFactors? (e : Expr) : Option (Array Nat) := - match e.getAppFnArgs with - | (``ZMod, #[n]) => (getNatLit? n).map (#[·]) - | (``Multiplicative, #[a]) => cyclicFactors? a - | (``Prod, #[a, b]) => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) + match_expr e with + | ZMod n => (getNatLit? n).map (#[·]) + | Multiplicative a => cyclicFactors? a + | Prod a b => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) | _ => none /-- LMFDB encodes the torsion structure as a brace array `{2,4}` and the ideal class group as @@ -192,56 +138,37 @@ a JSON bracket array `[2, 2]`. -/ def fmtBraces (f : Array Nat) : String := "{" ++ ",".intercalate (f.toList.map toString) ++ "}" def fmtBrackets (f : Array Nat) : String := "[" ++ ", ".intercalate (f.toList.map toString) ++ "]" -/-- Translate an abelian-group-structure claim `lhs ≃ rhs` (where `rhs` is a product of -cyclics) into an invariant-factor column comparison; `positive := false` negates it (`<>`). -/ +/-- The de Bruijn index of a bound variable, if `e` is one. -/ +def bvarIdx? : Expr → Option Nat + | .bvar n => some n + | _ => none + +/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` ("the group is abelian"), +allowing the two multiplications to have swapped operands. -/ +def isAbelianPattern (e : Expr) : Bool := + match e with + | .forallE _ _ (.forallE _ _ body _) _ => + match_expr body with + | Eq _ lhs rhs => + match_expr lhs with + | HMul.hMul _ _ _ _ l1 l2 => + match_expr rhs with + | HMul.hMul _ _ _ _ r1 r2 => + (bvarIdx? l1 == bvarIdx? r2) && (bvarIdx? l2 == bvarIdx? r1) && + (bvarIdx? l1).isSome && (bvarIdx? l1 != bvarIdx? l2) + | _ => false + | _ => false + | _ => false + | _ => false + +/-- Translate an abelian-group-structure claim `lhs ≃ rhs` (with `rhs` a product of cyclics) +into an invariant-factor column comparison; `positive := false` negates it (`<>`). -/ def structCond (positive : Bool) (lhs rhs : Expr) (lhsConst : Name) - (col display table : String) (fmt : Array Nat → String) : Option Scalar := do + (column display : String) (fmt : Array Nat → String) : Option Cond := do guard (containsConst lhs lhsConst) let factors ← cyclicFactors? rhs - return { sql := s!"{col} {if positive then "=" else "<>"} '{fmt factors}'", - refs := #[(display, col.replace "::text" "")], table := table } - -/-- Translate a property of the object into a SQL condition. Handles boolean flags -(`IsSimpleGroup`, the abelian pattern) and abelian-group-structure isomorphisms (torsion -subgroup via `≃+`, ideal class group via `≃*`), optionally wrapped in `Nonempty`. -`positive := false` asks for the property to *fail*. -/ -partial def toSqlPredicate (positive : Bool) (e : Expr) : Option Scalar := - let tf := if positive then "'t'" else "'f'" - match e.getAppFnArgs with - | (``Nonempty, #[inner]) => toSqlPredicate positive inner - | (``IsSimpleGroup, _) => - some { sql := s!"simple = {tf}", refs := #[("simple", "simple")], table := "gps_groups" } - | (``AddEquiv, args) => - if 2 ≤ args.size then - structCond positive args[0]! args[1]! ``AddCommGroup.torsion - "torsion_structure" "torsion structure" "ec_curvedata" fmtBraces - else none - | (``MulEquiv, args) => - if 2 ≤ args.size then - structCond positive args[0]! args[1]! ``ClassGroup - "class_group::text" "class group" "nf_fields" fmtBrackets - else none - | _ => - if isAbelianPattern e then - some { sql := s!"abelian = {tf}", refs := #[("abelian", "abelian")], table := "gps_groups" } - else none - -/-- Translate a `Prop` into a SQL condition. `positive := false` translates its negation -instead; pushing the negation down to the operator / boolean value (rather than wrapping the -whole condition in SQL `NOT (...)`) keeps the query index-friendly. -/ -partial def toCond (positive : Bool) (e : Expr) : Option Scalar := - match e.getAppFnArgs with - | (``Not, #[p]) => toCond (!positive) p - | _ => - match matchCmp e with - | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b - | none => toSqlPredicate positive e - -/-- Translate a `Prop` into a SQL condition. -/ -def toSqlCond (e : Expr) : Option Scalar := toCond true e - -/-- Translate the *negation* of a `Prop` into a SQL condition (used for the goal). -/ -def toSqlCondNeg (e : Expr) : Option Scalar := toCond false e + return { sql := s!"{column} {if positive then "=" else "<>"} '{fmt factors}'", + refs := #[(display, column.replace "::text" "")] } /-! #### Reading and rendering a result row -/ @@ -299,6 +226,11 @@ structure TableInfo where url : String → String /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/ orderBy : String + /-- Recognisers for scalar quantities of this object (used inside comparisons). To teach + `lookup` a new column, add a matcher here. -/ + scalars : Array (Expr → Option Column) := #[] + /-- Recognisers for boolean/structure properties of this object at a given polarity. -/ + props : Array (Bool → Expr → Option Cond) := #[] /-- LMFDB elliptic-curve labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. -/ def ecUrl (label : String) : String := @@ -318,6 +250,28 @@ def nfFields : TableInfo where {formatPoly (rowStr row "coeffs")}" url label := s!"https://www.lmfdb.org/NumberField/{label}" orderBy := "disc_abs" + scalars := #[ + fun e => match_expr e with + | NumberField.classNumber _ _ _ => some (col "class_number" "class number") + | _ => none, + fun e => match_expr e with + | Module.finrank r _ _ _ _ => if r.isConstOf ``Rat then some (col "degree" "degree") else none + | _ => none, + -- `|NumberField.discr F|` is `disc_abs`; the bare signed discriminant is split as + -- `disc_sign * disc_abs` (with `signed?` set so comparisons stay index-friendly). + fun e => match_expr e with + | abs _ _ _ x => match_expr x with + | NumberField.discr _ _ _ => some (col "disc_abs" "|discriminant|") + | _ => none + | NumberField.discr _ _ _ => + some (col "(disc_sign * disc_abs)" "discriminant" (some ("disc_sign", "disc_abs"))) + | _ => none] + props := #[ + -- ideal class group structure: `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)`. + fun pos e => match_expr e with + | MulEquiv a b _ _ => + structCond pos a b ``ClassGroup "class_group::text" "class group" fmtBrackets + | _ => none] /-- Elliptic curves over `ℚ`. -/ def ecCurvedata : TableInfo where @@ -327,6 +281,20 @@ def ecCurvedata : TableInfo where describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" url := ecUrl orderBy := "conductor" + scalars := #[ + fun e => match_expr e with + | Module.finrank r _ _ _ _ => if r.isConstOf ``Int then some (col "rank" "rank") else none + | _ => none, + fun e => match_expr e with + | Nat.card g => + if containsConst g ``AddCommGroup.torsion then some (col "torsion" "torsion") else none + | _ => none] + props := #[ + -- torsion subgroup structure: `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)`. + fun pos e => match_expr e with + | AddEquiv a b _ _ => + structCond pos a b ``AddCommGroup.torsion "torsion_structure" "torsion structure" fmtBraces + | _ => none] /-- Finite groups. -/ def gpsGroups : TableInfo where @@ -337,13 +305,66 @@ def gpsGroups : TableInfo where url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" -- `order` is a SQL reserved word, so it must be quoted. orderBy := "\"order\"" + props := #[ + fun pos e => match_expr e with + | IsSimpleGroup _ _ => some (boolCol pos "simple") + | _ => none, + fun pos e => if isAbelianPattern e then some (boolCol pos "abelian") else none] + +/-- All supported object families. To support a new one, add its `TableInfo` here. -/ +def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] /-- The table configuration for a table name. -/ -def tableInfo? : String → Option TableInfo - | "nf_fields" => some nfFields - | "ec_curvedata" => some ecCurvedata - | "gps_groups" => some gpsGroups - | _ => none +def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == name) + +/-! #### Dispatch: translating a `Prop` to a SQL condition -/ + +/-- Find the scalar column an expression denotes (trying every table's recognisers), together +with the table it belongs to. -/ +def findScalar (e : Expr) : Option (Column × String) := + tables.findSome? fun t => (t.scalars.findSome? (· e)).map (·, t.table) + +/-- A column compared against an integer literal. A "signed" column stored as `sign * |·|` is +case-split on the sign, so the comparison hits the indexed absolute-value column rather than +the non-indexable product. -/ +def colVsLit (c : Column) (table : String) (cmp : Cmp) (k : Int) : Cond := + match c.signed? with + | some (signCol, absCol) => + { sql := s!"(({signCol} = 1 AND {absCol} {cmp.toSql} {k}) OR \ + ({signCol} = -1 AND {absCol} {cmp.reverse.toSql} {-k}))", + refs := #[(c.display, c.sql)], table := some table } + | none => + { sql := s!"{c.sql} {cmp.toSql} {k}", refs := #[(c.display, c.sql)], table := some table } + +/-- Translate a comparison `cmp a b` (column vs literal, or column vs column) into a `Cond`. -/ +def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Cond := + match findScalar a, findScalar b with + | some (ca, ta), some (cb, _) => + some { sql := s!"{ca.sql} {cmp.toSql} {cb.sql}", + refs := #[(ca.display, ca.sql), (cb.display, cb.sql)], table := some ta } + | some (ca, ta), none => (getIntLit? b).map (colVsLit ca ta cmp) + | none, some (cb, tb) => (getIntLit? a).map (colVsLit cb tb cmp.reverse) + | none, none => none + +/-- Translate a `Prop` into a SQL condition. `positive := false` translates its negation; +pushing the negation down to the operator / boolean value (rather than wrapping in SQL +`NOT (...)`) keeps the query index-friendly. `Not` flips the polarity; `Nonempty` is +transparent (an isomorphism *exists* iff the structures match). -/ +partial def toCond (positive : Bool) (e : Expr) : Option Cond := + match_expr e with + | Not p => toCond (!positive) p + | Nonempty p => toCond positive p + | _ => + match matchCmp e with + | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b + | none => tables.findSome? fun t => + (t.props.findSome? (· positive e)).map fun c => { c with table := some t.table } + +/-- Translate a `Prop` into a SQL condition. -/ +def toSqlCond (e : Expr) : Option Cond := toCond true e + +/-- Translate the *negation* of a `Prop` into a SQL condition (used for the goal). -/ +def toSqlCondNeg (e : Expr) : Option Cond := toCond false e /-! #### Assembling the query and report -/ @@ -402,8 +423,8 @@ def reportAlt (info : TableInfo) (row : Json) (items : Array (String × String)) /-- Translate the hypotheses in context into SQL condition scalars. A hypothesis that *is* a comparison but that we cannot translate is reported as a warning (and dropped), since silently ignoring it would weaken any "no counterexample" conclusion. -/ -def collectHypotheses : TacticM (Array Scalar) := do - let mut out : Array Scalar := #[] +def collectHypotheses : TacticM (Array Cond) := do + let mut out : Array Cond := #[] for ldecl in ← getLCtx do if ldecl.isImplementationDetail then continue let ty ← instantiateMVars ldecl.type From bb140250a45b3197be8566dba475ae083ccbbcb5 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 09:58:55 +0100 Subject: [PATCH 12/34] split the tactic out from the demo --- LeanBridge/Lookup/Demo.lean | 529 ++-------------------------------- LeanBridge/Lookup/Lookup.lean | 462 +++++++++++++++++++++++++++++ 2 files changed, 483 insertions(+), 508 deletions(-) create mode 100644 LeanBridge/Lookup/Lookup.lean diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index a8af84b1..f67aba46 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -1,508 +1,23 @@ -import Mathlib -import ProofWidgets.Component.HtmlDisplay +import LeanBridge.Lookup.Lookup --- https://www.lmfdb.org/api/nf_fields/?_format=json&_offset=0 +/-! # `lookup` demo -open Lean Elab Tactic Meta +Each example below is a *false* statement; `lookup` finds and reports a counterexample from +LMFDB (the smallest one, with the object's defining data and a clickable link), so each +`example` is expected to error with that report. -/ +open Lookup - -/-- Build the request body for an LMFDB `/sql` call. -/ -def sqlRequestBody (sql : String) (limit : Nat := 1000) : Json := - .mkObj [ - ("sql", toJson sql), - ("limit", toJson limit) - ] - -/-- Run a SQL query against the LMFDB `/sql` endpoint and return the decoded result. -/ -def runSql (sql : String) : MetaM Json := do - let sqlUrl := "https://mcp.lmfdb.org/sql" - let curlArgs := #[ - "-sS", - "-X", "POST", sqlUrl, - "-H", "Content-Type: application/json", - "-d", (sqlRequestBody sql).compress - ] - let out ← IO.Process.output { cmd := "curl", args := curlArgs } - if out.exitCode != 0 then - throwError s!"curl failed (exit {out.exitCode}): {out.stderr}" - let .ok result := Json.parse out.stdout - | throwError s!"failed to parse response:\n{out.stdout}" - return result - --- #eval runSql "SELECT lmfdb_label, conductor, rank FROM ec_curvedata WHERE rank >= 4 AND conductor <= 1000 LIMIT 1" --- #eval runSql "SELECT label, coeffs, degree FROM nf_fields WHERE degree = 2 LIMIT 1" - -/-! ### The `lookup` tactic - -`lookup` reads the local hypotheses and the goal, translates them into a SQL query -against LMFDB that searches for a *counterexample* (a database object satisfying all the -hypotheses but **violating** the goal), and reports it if one is found. -/ - -namespace Lookup - -initialize registerTraceClass `lookup - -/-! #### Literals -/ - -/-- Extract a natural-number literal from `e`, handling `@OfNat.ofNat _ n _`. -/ -def getNatLit? (e : Expr) : Option Nat := - match_expr e with - | OfNat.ofNat _ n _ => n.rawNatLit? - | _ => e.rawNatLit? - -/-- Extract an integer literal, handling a leading negation `@Neg.neg _ _ n`. -/ -def getIntLit? (e : Expr) : Option Int := - match_expr e with - | Neg.neg _ _ a => (getNatLit? a).map fun n => -(n : Int) - | _ => (getNatLit? e).map Int.ofNat - -/-! #### Comparison operators -/ - -/-- A comparison operator we know how to send to SQL. -/ -inductive Cmp | eq | ne | le | lt | ge | gt - deriving Inhabited, BEq - -namespace Cmp - -/-- The SQL spelling of the operator. -/ -def toSql : Cmp → String - | eq => "=" | ne => "<>" | le => "<=" | lt => "<" | ge => ">=" | gt => ">" - -/-- The operator whose truth value is the logical negation of this one. -/ -def negate : Cmp → Cmp - | eq => ne | ne => eq | le => gt | lt => ge | ge => lt | gt => le - -/-- The operator that holds after swapping the operands (equivalently, after negating both -sides of an order comparison). -/ -def reverse : Cmp → Cmp - | eq => eq | ne => ne | le => ge | lt => gt | ge => le | gt => lt - -end Cmp - -/-! #### Translating Lean expressions to SQL - -A `Column` is a quantity of an object (an SQL column expression plus a display name); a `Cond` -is a translated SQL boolean condition. The recognisers that map Lean expressions to columns -and conditions live *with each table* in the registry below, so adding a column or property to -a table is a local, one-line change. The generic plumbing here is table-agnostic. -/ - -/-- A scalar quantity of an object: an SQL column expression and a human-readable name. A -quantity stored split as `sign * |·|` records those two columns in `signed?`, so comparisons -against a literal can be made index-friendly. -/ -structure Column where - sql : String - display : String - signed? : Option (String × String) := none - -/-- A translated SQL condition: the boolean SQL, the columns it references (as -`(displayName, selectExpr)` pairs, for reporting), and the LMFDB table it forces. -/ -structure Cond where - sql : String - refs : Array (String × String) := #[] - table : Option String := none - -/-- Build a `Column`. -/ -def col (sql display : String) (signed? : Option (String × String) := none) : Column := - { sql, display, signed? } - -/-- A boolean-flag condition `column = 't'` (or `column = 'f'` when negated). -/ -def boolCol (positive : Bool) (column : String) : Cond := - { sql := s!"{column} = {if positive then "'t'" else "'f'"}", refs := #[(column, column)] } - -/-- Match a comparison `Prop`, returning the operator and the two operands. -/ -def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := - match_expr e with - | Eq _ a b => some (.eq, a, b) - | Ne _ a b => some (.ne, a, b) - | LE.le _ _ a b => some (.le, a, b) - | LT.lt _ _ a b => some (.lt, a, b) - | GE.ge _ _ a b => some (.ge, a, b) - | GT.gt _ _ a b => some (.gt, a, b) - | _ => none - -/-- Whether `e` mentions the constant `n` anywhere. -/ -def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome - -/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` -wrappers stripped) as its list of moduli, in the order written. -/ -partial def cyclicFactors? (e : Expr) : Option (Array Nat) := - match_expr e with - | ZMod n => (getNatLit? n).map (#[·]) - | Multiplicative a => cyclicFactors? a - | Prod a b => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) - | _ => none - -/-- LMFDB encodes the torsion structure as a brace array `{2,4}` and the ideal class group as -a JSON bracket array `[2, 2]`. -/ -def fmtBraces (f : Array Nat) : String := "{" ++ ",".intercalate (f.toList.map toString) ++ "}" -def fmtBrackets (f : Array Nat) : String := "[" ++ ", ".intercalate (f.toList.map toString) ++ "]" - -/-- The de Bruijn index of a bound variable, if `e` is one. -/ -def bvarIdx? : Expr → Option Nat - | .bvar n => some n - | _ => none - -/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` ("the group is abelian"), -allowing the two multiplications to have swapped operands. -/ -def isAbelianPattern (e : Expr) : Bool := - match e with - | .forallE _ _ (.forallE _ _ body _) _ => - match_expr body with - | Eq _ lhs rhs => - match_expr lhs with - | HMul.hMul _ _ _ _ l1 l2 => - match_expr rhs with - | HMul.hMul _ _ _ _ r1 r2 => - (bvarIdx? l1 == bvarIdx? r2) && (bvarIdx? l2 == bvarIdx? r1) && - (bvarIdx? l1).isSome && (bvarIdx? l1 != bvarIdx? l2) - | _ => false - | _ => false - | _ => false - | _ => false - -/-- Translate an abelian-group-structure claim `lhs ≃ rhs` (with `rhs` a product of cyclics) -into an invariant-factor column comparison; `positive := false` negates it (`<>`). -/ -def structCond (positive : Bool) (lhs rhs : Expr) (lhsConst : Name) - (column display : String) (fmt : Array Nat → String) : Option Cond := do - guard (containsConst lhs lhsConst) - let factors ← cyclicFactors? rhs - return { sql := s!"{column} {if positive then "=" else "<>"} '{fmt factors}'", - refs := #[(display, column.replace "::text" "")] } - -/-! #### Reading and rendering a result row -/ - -/-- The first returned row of an LMFDB `/sql` response, if any. -/ -def firstRow? (j : Json) : Option Json := - match j.getObjVal? "rows" with - | .ok (.arr rs) => rs[0]? - | _ => none - -/-- Read a (text-cast) field of a row as a string. -/ -def rowStr (row : Json) (key : String) : String := - (row.getObjValAs? String key).toOption.getD "?" - -/-- Pretty-print the integer monomial `c * x^e` (its sign is handled by the caller). -/ -def monomial (c : Int) (e : Nat) : String := - if e == 0 then toString c.natAbs - else - let base := if e == 1 then "x" else s!"x^{e}" - if c.natAbs == 1 then base else s!"{c.natAbs}*{base}" - -/-- Format an LMFDB `coeffs` array (e.g. `{-1,-1,1}`, lowest degree first) as a polynomial -in `x`, highest degree first. -/ -def formatPoly (coeffs : String) : String := Id.run do - let stripped := (coeffs.replace "{" "").replace "}" "" - let cs := (stripped.splitOn ",").filterMap String.toInt? - let n := cs.length - let mut out := "" - for i in [0:n] do - let e := n - 1 - i - let c := cs[e]! - if c == 0 then continue - let term := monomial c e - if out.isEmpty then - out := if c < 0 then s!"-{term}" else term - else - out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}") - return if out.isEmpty then "0" else out - -/-! #### LMFDB tables - -Each supported object family corresponds to a table, knowing how to select its label and -descriptive data, render that data, and build a link to the LMFDB page. -/ - -/-- Per-table knowledge needed to query and report a counterexample. -/ -structure TableInfo where - /-- The SQL table name. -/ - table : String - /-- The column holding the LMFDB label (selected `AS label`). -/ - labelCol : String - /-- Extra SELECT fragments for the descriptive data (e.g. the defining polynomial). -/ - descSelects : Array String - /-- Render the descriptive data of a result row as plain text. -/ - describe : Json → String - /-- Build the LMFDB page URL from a label. -/ - url : String → String - /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/ - orderBy : String - /-- Recognisers for scalar quantities of this object (used inside comparisons). To teach - `lookup` a new column, add a matcher here. -/ - scalars : Array (Expr → Option Column) := #[] - /-- Recognisers for boolean/structure properties of this object at a given polarity. -/ - props : Array (Bool → Expr → Option Cond) := #[] - -/-- LMFDB elliptic-curve labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. -/ -def ecUrl (label : String) : String := - match label.splitOn "." with - | [conductor, iso] => - let letters := iso.takeWhile Char.isAlpha - let number := iso.dropWhile Char.isAlpha - s!"https://www.lmfdb.org/EllipticCurve/Q/{conductor}/{letters}/{number}" - | _ => s!"https://www.lmfdb.org/EllipticCurve/Q/{label}" - -/-- Number fields. -/ -def nfFields : TableInfo where - table := "nf_fields" - labelCol := "label" - descSelects := #["coeffs::text AS coeffs"] - describe row := s!"number field {rowStr row "label"}, with minimal polynomial \ - {formatPoly (rowStr row "coeffs")}" - url label := s!"https://www.lmfdb.org/NumberField/{label}" - orderBy := "disc_abs" - scalars := #[ - fun e => match_expr e with - | NumberField.classNumber _ _ _ => some (col "class_number" "class number") - | _ => none, - fun e => match_expr e with - | Module.finrank r _ _ _ _ => if r.isConstOf ``Rat then some (col "degree" "degree") else none - | _ => none, - -- `|NumberField.discr F|` is `disc_abs`; the bare signed discriminant is split as - -- `disc_sign * disc_abs` (with `signed?` set so comparisons stay index-friendly). - fun e => match_expr e with - | abs _ _ _ x => match_expr x with - | NumberField.discr _ _ _ => some (col "disc_abs" "|discriminant|") - | _ => none - | NumberField.discr _ _ _ => - some (col "(disc_sign * disc_abs)" "discriminant" (some ("disc_sign", "disc_abs"))) - | _ => none] - props := #[ - -- ideal class group structure: `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)`. - fun pos e => match_expr e with - | MulEquiv a b _ _ => - structCond pos a b ``ClassGroup "class_group::text" "class group" fmtBrackets - | _ => none] - -/-- Elliptic curves over `ℚ`. -/ -def ecCurvedata : TableInfo where - table := "ec_curvedata" - labelCol := "lmfdb_label" - descSelects := #["ainvs::text AS ainvs"] - describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" - url := ecUrl - orderBy := "conductor" - scalars := #[ - fun e => match_expr e with - | Module.finrank r _ _ _ _ => if r.isConstOf ``Int then some (col "rank" "rank") else none - | _ => none, - fun e => match_expr e with - | Nat.card g => - if containsConst g ``AddCommGroup.torsion then some (col "torsion" "torsion") else none - | _ => none] - props := #[ - -- torsion subgroup structure: `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)`. - fun pos e => match_expr e with - | AddEquiv a b _ _ => - structCond pos a b ``AddCommGroup.torsion "torsion_structure" "torsion structure" fmtBraces - | _ => none] - -/-- Finite groups. -/ -def gpsGroups : TableInfo where - table := "gps_groups" - labelCol := "label" - descSelects := #["tex_name::text AS tex_name"] - describe row := s!"group {rowStr row "label"} ({rowStr row "tex_name"})" - url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" - -- `order` is a SQL reserved word, so it must be quoted. - orderBy := "\"order\"" - props := #[ - fun pos e => match_expr e with - | IsSimpleGroup _ _ => some (boolCol pos "simple") - | _ => none, - fun pos e => if isAbelianPattern e then some (boolCol pos "abelian") else none] - -/-- All supported object families. To support a new one, add its `TableInfo` here. -/ -def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] - -/-- The table configuration for a table name. -/ -def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == name) - -/-! #### Dispatch: translating a `Prop` to a SQL condition -/ - -/-- Find the scalar column an expression denotes (trying every table's recognisers), together -with the table it belongs to. -/ -def findScalar (e : Expr) : Option (Column × String) := - tables.findSome? fun t => (t.scalars.findSome? (· e)).map (·, t.table) - -/-- A column compared against an integer literal. A "signed" column stored as `sign * |·|` is -case-split on the sign, so the comparison hits the indexed absolute-value column rather than -the non-indexable product. -/ -def colVsLit (c : Column) (table : String) (cmp : Cmp) (k : Int) : Cond := - match c.signed? with - | some (signCol, absCol) => - { sql := s!"(({signCol} = 1 AND {absCol} {cmp.toSql} {k}) OR \ - ({signCol} = -1 AND {absCol} {cmp.reverse.toSql} {-k}))", - refs := #[(c.display, c.sql)], table := some table } - | none => - { sql := s!"{c.sql} {cmp.toSql} {k}", refs := #[(c.display, c.sql)], table := some table } - -/-- Translate a comparison `cmp a b` (column vs literal, or column vs column) into a `Cond`. -/ -def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Cond := - match findScalar a, findScalar b with - | some (ca, ta), some (cb, _) => - some { sql := s!"{ca.sql} {cmp.toSql} {cb.sql}", - refs := #[(ca.display, ca.sql), (cb.display, cb.sql)], table := some ta } - | some (ca, ta), none => (getIntLit? b).map (colVsLit ca ta cmp) - | none, some (cb, tb) => (getIntLit? a).map (colVsLit cb tb cmp.reverse) - | none, none => none - -/-- Translate a `Prop` into a SQL condition. `positive := false` translates its negation; -pushing the negation down to the operator / boolean value (rather than wrapping in SQL -`NOT (...)`) keeps the query index-friendly. `Not` flips the polarity; `Nonempty` is -transparent (an isomorphism *exists* iff the structures match). -/ -partial def toCond (positive : Bool) (e : Expr) : Option Cond := - match_expr e with - | Not p => toCond (!positive) p - | Nonempty p => toCond positive p - | _ => - match matchCmp e with - | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b - | none => tables.findSome? fun t => - (t.props.findSome? (· positive e)).map fun c => { c with table := some t.table } - -/-- Translate a `Prop` into a SQL condition. -/ -def toSqlCond (e : Expr) : Option Cond := toCond true e - -/-- Translate the *negation* of a `Prop` into a SQL condition (used for the goal). -/ -def toSqlCondNeg (e : Expr) : Option Cond := toCond false e - -/-! #### Assembling the query and report -/ - -/-- Deduplicate referenced quantities by their SQL expression, preserving order. -/ -def dedupRefs (refs : Array (String × String)) : Array (String × String) := Id.run do - let mut seen : Array String := #[] - let mut out : Array (String × String) := #[] - for (name, expr) in refs do - unless seen.contains expr do - seen := seen.push expr - out := out.push (name, expr) - return out - -/-- Build the counterexample query: the label, the descriptive data, and the actual values of -every referenced quantity (cast to text, since the endpoint cannot serialise bignum columns -directly). -/ -def buildQuery (info : TableInfo) (conds : Array String) (items : Array (String × String)) : - String := Id.run do - let mut selects : Array String := #[s!"{info.labelCol} AS label"] ++ info.descSelects - for i in [0:items.size] do - selects := selects.push s!"({items[i]!.2})::text AS c{i}" - let whereClause := String.intercalate " AND " conds.toList - return s!"SELECT {String.intercalate ", " selects.toList} FROM {info.table} \ - WHERE {whereClause} ORDER BY {info.orderBy} LIMIT 1" - -/-- The "name = value" strings for the referenced quantities of a result row. -/ -def valueStrs (row : Json) (items : Array (String × String)) : Array String := Id.run do - let mut out : Array String := #[] - for i in [0:items.size] do - out := out.push s!"{items[i]!.1} = {rowStr row s!"c{i}"}" - return out - -open ProofWidgets in -/-- Render a counterexample row as interactive HTML, including a clickable LMFDB link. -A bare or markdown URL in a `MessageData` is not linkified by the infoview, so we build an -actual `` element and embed it via `MessageData.ofHtml`. -/ -def reportHtml (info : TableInfo) (row : Json) (items : Array (String × String)) : Html := - let label := rowStr row "label" - Html.element "div" #[] #[ - .text "lookup: the statement is FALSE — LMFDB has a counterexample.", - .element "br" #[] #[], - .text (info.describe row), - .element "br" #[] #[], - .text (", ".intercalate (valueStrs row items).toList), - .element "br" #[] #[], - .element "a" #[("href", toJson (info.url label))] #[.text s!"{label} on LMFDB"] - ] - -/-- A plain-text fallback for the counterexample, shown where HTML cannot render. -/ -def reportAlt (info : TableInfo) (row : Json) (items : Array (String × String)) : String := - s!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ - {info.describe row}\n\ - {", ".intercalate (valueStrs row items).toList}\n\ - {info.url (rowStr row "label")}" - -/-- Translate the hypotheses in context into SQL condition scalars. A hypothesis that *is* a -comparison but that we cannot translate is reported as a warning (and dropped), since silently -ignoring it would weaken any "no counterexample" conclusion. -/ -def collectHypotheses : TacticM (Array Cond) := do - let mut out : Array Cond := #[] - for ldecl in ← getLCtx do - if ldecl.isImplementationDetail then continue - let ty ← instantiateMVars ldecl.type - match toSqlCond ty with - | some s => out := out.push s - | none => - if (matchCmp ty).isSome then - logWarning m!"lookup: ignoring hypothesis `{ldecl.userName}` : {ty}\n\ - (couldn't translate it to a SQL condition, so the search ignores this constraint)." - return out - -elab "lookup" : tactic => do - let goal ← getMainGoal - goal.withContext do - -- The negated goal is the final condition: we hunt for a row that breaks the goal. - let some goalCond := toSqlCondNeg (← instantiateMVars (← goal.getType)) - | throwError "lookup: don't know how to translate the goal into a SQL query" - let conditions := (← collectHypotheses).push goalCond - -- Every condition must point at the same LMFDB table. - let info ← match (conditions.filterMap (·.table)).toList.dedup with - | [t] => match tableInfo? t with - | some info => pure info - | none => throwError "lookup: no table configuration for `{t}`" - | [] => throwError "lookup: couldn't determine which LMFDB table the goal is about" - | ts => throwError "lookup: the goal mixes multiple LMFDB object types {ts}" - let conds := conditions.map (·.sql) - let items := dedupRefs (conditions.foldl (fun acc s => acc ++ s.refs) #[]) - let query := buildQuery info conds items - trace[lookup] "query:\n{query}" - match firstRow? (← runSql query) with - | none => - -- No counterexample in the database: report, but do *not* close the goal. - logInfo m!"lookup: no counterexample found in LMFDB \ - (the statement is consistent with the database, but this is not a proof)." - | some row => - throwError (← MessageData.ofHtml (reportHtml info row items) (reportAlt info row items)) - -end Lookup - - -/- -**Elliptic curves over Q:** `SELECT lmfdb_label, ainvs FROM ec_curvedata WHERE...` -* [ec.torsion_subgroup](https://beta.lmfdb.org/knowledge/show/ec.torsion_subgroup) -- `torsion=4` or `torsion_structure='{2,2}'` -* [ec.discriminant](https://beta.lmfdb.org/knowledge/show/ec.discriminant) -- `absD=164025 AND signD=1` -* [ec.rank](https://beta.lmfdb.org/knowledge/show/ec.rank) / [ec.mordell_weil_group]([https://beta.lmfdb.org/knowledge/show/ec.mordell_weil_group) -- `rank=4` - -**Dirichlet characters:** `SELECT label FROM char_dirichlet WHERE...` -* [character.dirichlet.primitive](https://beta.lmfdb.org/knowledge/show/character.dirichlet.primitive) -- `is_primitive='t'` -* [character.dirichlet.order](https://beta.lmfdb.org/knowledge/show/character.dirichlet.order) -- `order=4` -* [character.dirichlet.conductor](https://beta.lmfdb.org/knowledge/show/character.dirichlet.conductor) -- `conductor=4` - -**Number fields:** `SELECT label, coeffs FROM nf_fields WHERE...` -* [nf.degree_mathlib_def](https://beta.lmfdb.org/knowledge/show/nf.degree_mathlib_def) -- `degree=6` -* [nf.ideal_class_group](https://beta.lmfdb.org/knowledge/show/nf.ideal_class_group) -- `class_group='{2,2}'` -* [nf.class_number](https://beta.lmfdb.org/knowledge/show/nf.class_number) -- `class_number=4` -* [nf.discriminant](https://beta.lmfdb.org/knowledge/show/nf.discriminant) -- `disc_abs=41 AND disc_sign=1` - -*Example*: Every number field with class number 1 and degree 2 has absolute discriminant at most 163 - -**Groups:** `SELECT label, tex_name FROM gps_groups WHERE...` -* [group.simple](https://beta.lmfdb.org/knowledge/show/group.simple) -- `simple='t'` -* [group.abelian](https://beta.lmfdb.org/knowledge/show/group.abelian) -- `abelian='t'` - -*Example*: Every simple group is nonabelian --/ - --- `ec_curvedata` = (W : WeierstrassCurve.Affine ℚ) --- `torsion` = Nat.card (AddCommGroup.torsion W.Point) --- `torsion_structure` ≈ AddCommGroup.torsion W.Point, but note that torsion_structure is the strucutre of the group as a product of cyclics --- `rank` = Module.finrank ℤ W.Point - +-- Number fields. "Every number field of class number 1 and degree 2 has |discriminant| ≤ 163" +-- is false (the bound is the *imaginary* quadratic class-number-1 theorem; real quadratic +-- fields have unbounded discriminant). `lookup` surfaces `2.2.172.1`. example {F : Type*} [Field F] [NumberField F] - (hF : NumberField.classNumber F = 1) (hF : Module.finrank ℚ F = 2) : + (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) : |NumberField.discr F| ≤ 163 := by lookup --- Signed-discriminant queries are supported too (the DB stores `disc_sign * disc_abs`, --- and `lookup` case-splits on the sign so the query stays index-friendly): +-- Signed-discriminant queries are supported too (the DB stores `disc_sign * disc_abs`, and +-- `lookup` case-splits on the sign so the query stays index-friendly): -- `NumberField.discr F ≥ -100` finds the counterexample `2.0.163.1` (discriminant -163), -- while `NumberField.discr F ≥ -163` finds none. @@ -514,31 +29,29 @@ example {F : Type*} [Field F] [NumberField F] Nonempty (ClassGroup (NumberField.RingOfIntegers F) ≃* Multiplicative (ZMod 4)) := by lookup --- A non-number-field example: `lookup` dispatches to the `ec_curvedata` table. This claim is --- false — e.g. curve `117.a4` has a 4-torsion point yet positive rank — so `lookup` surfaces --- it (with the curve's a-invariants and a link). The `≤ 20` version instead finds nothing. +-- Elliptic curves: `lookup` dispatches to `ec_curvedata`. "Every curve with a 4-torsion point +-- has rank ≤ 0" is false — e.g. `117.a3` has a 4-torsion point and positive rank. example {W : WeierstrassCurve.Affine ℚ} (hW : 4 ≤ Nat.card (AddCommGroup.torsion W.Point)) : Module.finrank ℤ W.Point ≤ 0 := by lookup --- "Every elliptic curve over ℚ with rank at least 2 has trivial torsion subgroup." This is --- false: e.g. curve `1088.a1` has rank 2 and a 2-torsion point. +-- "Every elliptic curve over ℚ with rank at least 2 has trivial torsion subgroup" is false: +-- e.g. `1088.a1` has rank 2 and a 2-torsion point. example {W : WeierstrassCurve.Affine ℚ} (hW : 2 ≤ Module.finrank ℤ W.Point) : Nat.card (AddCommGroup.torsion W.Point) = 1 := by lookup --- Group *structure* is supported too (LMFDB's `torsion_structure`): "every curve whose --- torsion subgroup has order 4 has torsion subgroup ≅ ℤ/4" is false — some are ℤ/2 × ℤ/2. --- The torsion subgroup is additive, hence `≃+`. +-- Torsion subgroup *structure* (LMFDB's `torsion_structure`): "every curve whose torsion +-- subgroup has order 4 has torsion subgroup ≅ ℤ/4" is false — some are ℤ/2 × ℤ/2. The torsion +-- subgroup is additive, hence `≃+`. example {W : WeierstrassCurve.Affine ℚ} (hW : Nat.card (AddCommGroup.torsion W.Point) = 4) : Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 4) := by lookup --- A third object family: `lookup` dispatches boolean properties to `gps_groups`. "Every --- simple group is nonabelian" is false — the cyclic groups of prime order are simple and --- abelian — so `lookup` surfaces such a group. +-- Groups: `lookup` dispatches boolean properties to `gps_groups`. "Every simple group is +-- nonabelian" is false — the cyclic groups of prime order are simple and abelian. example {G : Type*} [Group G] [IsSimpleGroup G] : ¬ ∀ a b : G, a * b = b * a := by lookup diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean new file mode 100644 index 00000000..55cb9673 --- /dev/null +++ b/LeanBridge/Lookup/Lookup.lean @@ -0,0 +1,462 @@ +import Mathlib +import ProofWidgets.Component.HtmlDisplay + +/-! # The `lookup` tactic + +`lookup` reads the local hypotheses and the goal, translates them into a SQL query against +LMFDB that searches for a *counterexample* (a database object satisfying all the hypotheses but +**violating** the goal), and reports it if one is found. It never closes the goal: a hit shows +the statement is false, and a miss is only evidence (the database is not exhaustive). + +To support a new object family, add a `TableInfo` to `tables`. To teach an existing family a +new column or property, add a recogniser to that table's `scalars`/`props`. -/ + +open Lean Elab Tactic Meta + +namespace Lookup + +initialize registerTraceClass `lookup + +/-! #### Querying LMFDB -/ + +/-- Build the request body for an LMFDB `/sql` call. -/ +def sqlRequestBody (sql : String) (limit : Nat := 1000) : Json := + .mkObj [("sql", toJson sql), ("limit", toJson limit)] + +/-- Run a SQL query against the LMFDB `/sql` endpoint and return the decoded result. -/ +def runSql (sql : String) : MetaM Json := do + let sqlUrl := "https://mcp.lmfdb.org/sql" + let curlArgs := #[ + "-sS", + "-X", "POST", sqlUrl, + "-H", "Content-Type: application/json", + "-d", (sqlRequestBody sql).compress + ] + let out ← IO.Process.output { cmd := "curl", args := curlArgs } + if out.exitCode != 0 then + throwError s!"curl failed (exit {out.exitCode}): {out.stderr}" + let .ok result := Json.parse out.stdout + | throwError s!"failed to parse response:\n{out.stdout}" + return result + +/-! #### Literals -/ + +/-- Extract a natural-number literal from `e`, handling `@OfNat.ofNat _ n _`. -/ +def getNatLit? (e : Expr) : Option Nat := + match_expr e with + | OfNat.ofNat _ n _ => n.rawNatLit? + | _ => e.rawNatLit? + +/-- Extract an integer literal, handling a leading negation `@Neg.neg _ _ n`. -/ +def getIntLit? (e : Expr) : Option Int := + match_expr e with + | Neg.neg _ _ a => (getNatLit? a).map fun n => -(n : Int) + | _ => (getNatLit? e).map Int.ofNat + +/-! #### Comparison operators -/ + +/-- A comparison operator we know how to send to SQL. -/ +inductive Cmp | eq | ne | le | lt | ge | gt + deriving Inhabited, BEq + +namespace Cmp + +/-- The SQL spelling of the operator. -/ +def toSql : Cmp → String + | eq => "=" | ne => "<>" | le => "<=" | lt => "<" | ge => ">=" | gt => ">" + +/-- The operator whose truth value is the logical negation of this one. -/ +def negate : Cmp → Cmp + | eq => ne | ne => eq | le => gt | lt => ge | ge => lt | gt => le + +/-- The operator that holds after swapping the operands (equivalently, after negating both +sides of an order comparison). -/ +def reverse : Cmp → Cmp + | eq => eq | ne => ne | le => ge | lt => gt | ge => le | gt => lt + +end Cmp + +/-! #### Translating Lean expressions to SQL + +A `Column` is a quantity of an object (an SQL column expression plus a display name); a `Cond` +is a translated SQL boolean condition. The recognisers that map Lean expressions to columns +and conditions live *with each table* in the registry below, so adding a column or property to +a table is a local, one-line change. The generic plumbing here is table-agnostic. -/ + +/-- A scalar quantity of an object: an SQL column expression and a human-readable name. A +quantity stored split as `sign * |·|` records those two columns in `signed?`, so comparisons +against a literal can be made index-friendly. -/ +structure Column where + sql : String + display : String + signed? : Option (String × String) := none + +/-- A translated SQL condition: the boolean SQL, the columns it references (as +`(displayName, selectExpr)` pairs, for reporting), and the LMFDB table it forces. -/ +structure Cond where + sql : String + refs : Array (String × String) := #[] + table : Option String := none + +/-- Build a `Column`. -/ +def col (sql display : String) (signed? : Option (String × String) := none) : Column := + { sql, display, signed? } + +/-- A boolean-flag condition `column = 't'` (or `column = 'f'` when negated). -/ +def boolCol (positive : Bool) (column : String) : Cond := + { sql := s!"{column} = {if positive then "'t'" else "'f'"}", refs := #[(column, column)] } + +/-- Match a comparison `Prop`, returning the operator and the two operands. -/ +def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := + match_expr e with + | Eq _ a b => some (.eq, a, b) + | Ne _ a b => some (.ne, a, b) + | LE.le _ _ a b => some (.le, a, b) + | LT.lt _ _ a b => some (.lt, a, b) + | GE.ge _ _ a b => some (.ge, a, b) + | GT.gt _ _ a b => some (.gt, a, b) + | _ => none + +/-- Whether `e` mentions the constant `n` anywhere. -/ +def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome + +/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` +wrappers stripped) as its list of moduli, in the order written. -/ +partial def cyclicFactors? (e : Expr) : Option (Array Nat) := + match_expr e with + | ZMod n => (getNatLit? n).map (#[·]) + | Multiplicative a => cyclicFactors? a + | Prod a b => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) + | _ => none + +/-- LMFDB encodes the torsion structure as a brace array `{2,4}` and the ideal class group as +a JSON bracket array `[2, 2]`. -/ +def fmtBraces (f : Array Nat) : String := "{" ++ ",".intercalate (f.toList.map toString) ++ "}" +def fmtBrackets (f : Array Nat) : String := "[" ++ ", ".intercalate (f.toList.map toString) ++ "]" + +/-- The de Bruijn index of a bound variable, if `e` is one. -/ +def bvarIdx? : Expr → Option Nat + | .bvar n => some n + | _ => none + +/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` ("the group is abelian"), +allowing the two multiplications to have swapped operands. -/ +def isAbelianPattern (e : Expr) : Bool := + match e with + | .forallE _ _ (.forallE _ _ body _) _ => + match_expr body with + | Eq _ lhs rhs => + match_expr lhs with + | HMul.hMul _ _ _ _ l1 l2 => + match_expr rhs with + | HMul.hMul _ _ _ _ r1 r2 => + (bvarIdx? l1 == bvarIdx? r2) && (bvarIdx? l2 == bvarIdx? r1) && + (bvarIdx? l1).isSome && (bvarIdx? l1 != bvarIdx? l2) + | _ => false + | _ => false + | _ => false + | _ => false + +/-- Translate an abelian-group-structure claim `lhs ≃ rhs` (with `rhs` a product of cyclics) +into an invariant-factor column comparison; `positive := false` negates it (`<>`). -/ +def structCond (positive : Bool) (lhs rhs : Expr) (lhsConst : Name) + (column display : String) (fmt : Array Nat → String) : Option Cond := do + guard (containsConst lhs lhsConst) + let factors ← cyclicFactors? rhs + return { sql := s!"{column} {if positive then "=" else "<>"} '{fmt factors}'", + refs := #[(display, column.replace "::text" "")] } + +/-! #### Reading and rendering a result row -/ + +/-- The first returned row of an LMFDB `/sql` response, if any. -/ +def firstRow? (j : Json) : Option Json := + match j.getObjVal? "rows" with + | .ok (.arr rs) => rs[0]? + | _ => none + +/-- Read a (text-cast) field of a row as a string. -/ +def rowStr (row : Json) (key : String) : String := + (row.getObjValAs? String key).toOption.getD "?" + +/-- Pretty-print the integer monomial `c * x^e` (its sign is handled by the caller). -/ +def monomial (c : Int) (e : Nat) : String := + if e == 0 then toString c.natAbs + else + let base := if e == 1 then "x" else s!"x^{e}" + if c.natAbs == 1 then base else s!"{c.natAbs}*{base}" + +/-- Format an LMFDB `coeffs` array (e.g. `{-1,-1,1}`, lowest degree first) as a polynomial +in `x`, highest degree first. -/ +def formatPoly (coeffs : String) : String := Id.run do + let stripped := (coeffs.replace "{" "").replace "}" "" + let cs := (stripped.splitOn ",").filterMap String.toInt? + let n := cs.length + let mut out := "" + for i in [0:n] do + let e := n - 1 - i + let c := cs[e]! + if c == 0 then continue + let term := monomial c e + if out.isEmpty then + out := if c < 0 then s!"-{term}" else term + else + out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}") + return if out.isEmpty then "0" else out + +/-! #### LMFDB tables + +Each supported object family corresponds to a table, knowing how to select its label and +descriptive data, render that data, build a link to the LMFDB page, and recognise the Lean +expressions that map into its columns. -/ + +/-- Per-table knowledge needed to query and report a counterexample. -/ +structure TableInfo where + /-- The SQL table name. -/ + table : String + /-- The column holding the LMFDB label (selected `AS label`). -/ + labelCol : String + /-- Extra SELECT fragments for the descriptive data (e.g. the defining polynomial). -/ + descSelects : Array String + /-- Render the descriptive data of a result row as plain text. -/ + describe : Json → String + /-- Build the LMFDB page URL from a label. -/ + url : String → String + /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/ + orderBy : String + /-- Recognisers for scalar quantities of this object (used inside comparisons). To teach + `lookup` a new column, add a matcher here. -/ + scalars : Array (Expr → Option Column) := #[] + /-- Recognisers for boolean/structure properties of this object at a given polarity. -/ + props : Array (Bool → Expr → Option Cond) := #[] + +/-- LMFDB elliptic-curve labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. -/ +def ecUrl (label : String) : String := + match label.splitOn "." with + | [conductor, iso] => + let letters := iso.takeWhile Char.isAlpha + let number := iso.dropWhile Char.isAlpha + s!"https://www.lmfdb.org/EllipticCurve/Q/{conductor}/{letters}/{number}" + | _ => s!"https://www.lmfdb.org/EllipticCurve/Q/{label}" + +/-- Number fields. -/ +def nfFields : TableInfo where + table := "nf_fields" + labelCol := "label" + descSelects := #["coeffs::text AS coeffs"] + describe row := s!"number field {rowStr row "label"}, with minimal polynomial \ + {formatPoly (rowStr row "coeffs")}" + url label := s!"https://www.lmfdb.org/NumberField/{label}" + orderBy := "disc_abs" + scalars := #[ + fun e => match_expr e with + | NumberField.classNumber _ _ _ => some (col "class_number" "class number") + | _ => none, + fun e => match_expr e with + | Module.finrank r _ _ _ _ => if r.isConstOf ``Rat then some (col "degree" "degree") else none + | _ => none, + -- `|NumberField.discr F|` is `disc_abs`; the bare signed discriminant is split as + -- `disc_sign * disc_abs` (with `signed?` set so comparisons stay index-friendly). + fun e => match_expr e with + | abs _ _ _ x => match_expr x with + | NumberField.discr _ _ _ => some (col "disc_abs" "|discriminant|") + | _ => none + | NumberField.discr _ _ _ => + some (col "(disc_sign * disc_abs)" "discriminant" (some ("disc_sign", "disc_abs"))) + | _ => none] + props := #[ + -- ideal class group structure: `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)`. + fun pos e => match_expr e with + | MulEquiv a b _ _ => + structCond pos a b ``ClassGroup "class_group::text" "class group" fmtBrackets + | _ => none] + +/-- Elliptic curves over `ℚ`. -/ +def ecCurvedata : TableInfo where + table := "ec_curvedata" + labelCol := "lmfdb_label" + descSelects := #["ainvs::text AS ainvs"] + describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" + url := ecUrl + orderBy := "conductor" + scalars := #[ + fun e => match_expr e with + | Module.finrank r _ _ _ _ => if r.isConstOf ``Int then some (col "rank" "rank") else none + | _ => none, + fun e => match_expr e with + | Nat.card g => + if containsConst g ``AddCommGroup.torsion then some (col "torsion" "torsion") else none + | _ => none] + props := #[ + -- torsion subgroup structure: `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)`. + fun pos e => match_expr e with + | AddEquiv a b _ _ => + structCond pos a b ``AddCommGroup.torsion "torsion_structure" "torsion structure" fmtBraces + | _ => none] + +/-- Finite groups. -/ +def gpsGroups : TableInfo where + table := "gps_groups" + labelCol := "label" + descSelects := #["tex_name::text AS tex_name"] + describe row := s!"group {rowStr row "label"} ({rowStr row "tex_name"})" + url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" + -- `order` is a SQL reserved word, so it must be quoted. + orderBy := "\"order\"" + props := #[ + fun pos e => match_expr e with + | IsSimpleGroup _ _ => some (boolCol pos "simple") + | _ => none, + fun pos e => if isAbelianPattern e then some (boolCol pos "abelian") else none] + +/-- All supported object families. To support a new one, add its `TableInfo` here. -/ +def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] + +/-- The table configuration for a table name. -/ +def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == name) + +/-! #### Dispatch: translating a `Prop` to a SQL condition -/ + +/-- Find the scalar column an expression denotes (trying every table's recognisers), together +with the table it belongs to. -/ +def findScalar (e : Expr) : Option (Column × String) := + tables.findSome? fun t => (t.scalars.findSome? (· e)).map (·, t.table) + +/-- A column compared against an integer literal. A "signed" column stored as `sign * |·|` is +case-split on the sign, so the comparison hits the indexed absolute-value column rather than +the non-indexable product. -/ +def colVsLit (c : Column) (table : String) (cmp : Cmp) (k : Int) : Cond := + match c.signed? with + | some (signCol, absCol) => + { sql := s!"(({signCol} = 1 AND {absCol} {cmp.toSql} {k}) OR \ + ({signCol} = -1 AND {absCol} {cmp.reverse.toSql} {-k}))", + refs := #[(c.display, c.sql)], table := some table } + | none => + { sql := s!"{c.sql} {cmp.toSql} {k}", refs := #[(c.display, c.sql)], table := some table } + +/-- Translate a comparison `cmp a b` (column vs literal, or column vs column) into a `Cond`. -/ +def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Cond := + match findScalar a, findScalar b with + | some (ca, ta), some (cb, _) => + some { sql := s!"{ca.sql} {cmp.toSql} {cb.sql}", + refs := #[(ca.display, ca.sql), (cb.display, cb.sql)], table := some ta } + | some (ca, ta), none => (getIntLit? b).map (colVsLit ca ta cmp) + | none, some (cb, tb) => (getIntLit? a).map (colVsLit cb tb cmp.reverse) + | none, none => none + +/-- Translate a `Prop` into a SQL condition. `positive := false` translates its negation; +pushing the negation down to the operator / boolean value (rather than wrapping in SQL +`NOT (...)`) keeps the query index-friendly. `Not` flips the polarity; `Nonempty` is +transparent (an isomorphism *exists* iff the structures match). -/ +partial def toCond (positive : Bool) (e : Expr) : Option Cond := + match_expr e with + | Not p => toCond (!positive) p + | Nonempty p => toCond positive p + | _ => + match matchCmp e with + | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b + | none => tables.findSome? fun t => + (t.props.findSome? (· positive e)).map fun c => { c with table := some t.table } + +/-- Translate a `Prop` into a SQL condition. -/ +def toSqlCond (e : Expr) : Option Cond := toCond true e + +/-- Translate the *negation* of a `Prop` into a SQL condition (used for the goal). -/ +def toSqlCondNeg (e : Expr) : Option Cond := toCond false e + +/-! #### Assembling the query and report -/ + +/-- Deduplicate referenced quantities by their SQL expression, preserving order. -/ +def dedupRefs (refs : Array (String × String)) : Array (String × String) := Id.run do + let mut seen : Array String := #[] + let mut out : Array (String × String) := #[] + for (name, expr) in refs do + unless seen.contains expr do + seen := seen.push expr + out := out.push (name, expr) + return out + +/-- Build the counterexample query: the label, the descriptive data, and the actual values of +every referenced quantity (cast to text, since the endpoint cannot serialise bignum columns +directly). -/ +def buildQuery (info : TableInfo) (conds : Array String) (items : Array (String × String)) : + String := Id.run do + let mut selects : Array String := #[s!"{info.labelCol} AS label"] ++ info.descSelects + for i in [0:items.size] do + selects := selects.push s!"({items[i]!.2})::text AS c{i}" + let whereClause := String.intercalate " AND " conds.toList + return s!"SELECT {String.intercalate ", " selects.toList} FROM {info.table} \ + WHERE {whereClause} ORDER BY {info.orderBy} LIMIT 1" + +/-- The "name = value" strings for the referenced quantities of a result row. -/ +def valueStrs (row : Json) (items : Array (String × String)) : Array String := Id.run do + let mut out : Array String := #[] + for i in [0:items.size] do + out := out.push s!"{items[i]!.1} = {rowStr row s!"c{i}"}" + return out + +open ProofWidgets in +/-- Render a counterexample row as interactive HTML, including a clickable LMFDB link. +A bare or markdown URL in a `MessageData` is not linkified by the infoview, so we build an +actual `` element and embed it via `MessageData.ofHtml`. -/ +def reportHtml (info : TableInfo) (row : Json) (items : Array (String × String)) : Html := + let label := rowStr row "label" + Html.element "div" #[] #[ + .text "lookup: the statement is FALSE — LMFDB has a counterexample.", + .element "br" #[] #[], + .text (info.describe row), + .element "br" #[] #[], + .text (", ".intercalate (valueStrs row items).toList), + .element "br" #[] #[], + .element "a" #[("href", toJson (info.url label))] #[.text s!"{label} on LMFDB"] + ] + +/-- A plain-text fallback for the counterexample, shown where HTML cannot render. -/ +def reportAlt (info : TableInfo) (row : Json) (items : Array (String × String)) : String := + s!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ + {info.describe row}\n\ + {", ".intercalate (valueStrs row items).toList}\n\ + {info.url (rowStr row "label")}" + +/-- Translate the hypotheses in context into SQL conditions. A hypothesis that *is* a +comparison but that we cannot translate is reported as a warning (and dropped), since silently +ignoring it would weaken any "no counterexample" conclusion. -/ +def collectHypotheses : TacticM (Array Cond) := do + let mut out : Array Cond := #[] + for ldecl in ← getLCtx do + if ldecl.isImplementationDetail then continue + let ty ← instantiateMVars ldecl.type + match toSqlCond ty with + | some s => out := out.push s + | none => + if (matchCmp ty).isSome then + logWarning m!"lookup: ignoring hypothesis `{ldecl.userName}` : {ty}\n\ + (couldn't translate it to a SQL condition, so the search ignores this constraint)." + return out + +elab "lookup" : tactic => do + let goal ← getMainGoal + goal.withContext do + -- The negated goal is the final condition: we hunt for a row that breaks the goal. + let some goalCond := toSqlCondNeg (← instantiateMVars (← goal.getType)) + | throwError "lookup: don't know how to translate the goal into a SQL query" + let conditions := (← collectHypotheses).push goalCond + -- Every condition must point at the same LMFDB table. + let info ← match (conditions.filterMap (·.table)).toList.dedup with + | [t] => match tableInfo? t with + | some info => pure info + | none => throwError "lookup: no table configuration for `{t}`" + | [] => throwError "lookup: couldn't determine which LMFDB table the goal is about" + | ts => throwError "lookup: the goal mixes multiple LMFDB object types {ts}" + let conds := conditions.map (·.sql) + let items := dedupRefs (conditions.foldl (fun acc s => acc ++ s.refs) #[]) + let query := buildQuery info conds items + trace[lookup] "query:\n{query}" + match firstRow? (← runSql query) with + | none => + -- No counterexample in the database: report, but do *not* close the goal. + logInfo m!"lookup: no counterexample found in LMFDB \ + (the statement is consistent with the database, but this is not a proof)." + | some row => + throwError (← MessageData.ofHtml (reportHtml info row items) (reportAlt info row items)) + +end Lookup From 303fb8657c45cc2a66c4e0706297d618e7cecb7b Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:02:12 +0100 Subject: [PATCH 13/34] make recognisers declarative data --- LeanBridge/Lookup/Lookup.lean | 128 ++++++++++++++++++++++------------ 1 file changed, 84 insertions(+), 44 deletions(-) diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index 55cb9673..e0b06845 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -166,6 +166,73 @@ def structCond (positive : Bool) (lhs rhs : Expr) (lhsConst : Name) return { sql := s!"{column} {if positive then "=" else "<>"} '{fmt factors}'", refs := #[(display, column.replace "::text" "")] } +/-- Recognise an isomorphism `A ≃+ B` or `A ≃* B`, returning the equiv's head constant and the +two sides. -/ +def matchEquiv (e : Expr) : Option (Name × Expr × Expr) := + match_expr e with + | AddEquiv a b _ _ => some (``AddEquiv, a, b) + | MulEquiv a b _ _ => some (``MulEquiv, a, b) + | _ => none + +/-! #### Declarative recognisers + +Each table's columns and properties are described by *data* — `ScalarRule`/`PropRule` values. +All the `Expr`-matching metacode lives in the `match?` interpreters here, so teaching a table a +new column or property means adding a data constructor to its list (below), not writing a +matcher. -/ + +/-- How to recognise a scalar quantity of an object in a Lean expression. -/ +inductive ScalarRule where + /-- Head constant `c` applied to anything ↦ column `sql` (shown as `display`). -/ + | const (c : Name) (sql display : String) + /-- `Module.finrank` over base ring `ring` ↦ column (e.g. `ℚ` for degree, `ℤ` for rank). -/ + | finrank (ring : Name) (sql display : String) + /-- `Nat.card` of a type mentioning `inner` ↦ column (e.g. `AddCommGroup.torsion`). -/ + | cardOf (inner : Name) (sql display : String) + /-- `|c …|` (absolute value of a `c`-headed term) ↦ column. -/ + | absOf (c : Name) (sql display : String) + /-- Bare `c …` ↦ a signed quantity stored split as `signCol * absCol`. -/ + | signed (c : Name) (signCol absCol display : String) + +/-- Interpret a `ScalarRule` as a recogniser `Expr → Option Column`. -/ +def ScalarRule.match? : ScalarRule → Expr → Option Column + | .const c sql display, e => if e.isAppOf c then some (col sql display) else none + | .finrank ring sql display, e => + match_expr e with + | Module.finrank r _ _ _ _ => if r.isConstOf ring then some (col sql display) else none + | _ => none + | .cardOf inner sql display, e => + match_expr e with + | Nat.card g => if containsConst g inner then some (col sql display) else none + | _ => none + | .absOf c sql display, e => + match_expr e with + | abs _ _ _ x => if x.isAppOf c then some (col sql display) else none + | _ => none + | .signed c signCol absCol display, e => + if e.isAppOf c then some (col s!"({signCol} * {absCol})" display (some (signCol, absCol))) + else none + +/-- How to recognise a boolean/structure property of an object. -/ +inductive PropRule where + /-- Head constant `c` ↦ boolean column `column` (`= 't'`, or `= 'f'` when negated). -/ + | flag (c : Name) (column : String) + /-- The commutativity pattern `∀ a b, a * b = b * a` ↦ boolean column. -/ + | abelian (column : String) + /-- An isomorphism `lhs ≃ (∏ ZMod nᵢ)` via `equiv` (``AddEquiv``/``MulEquiv``), with `lhs` + mentioning `lhsConst`, compared against the invariant-factor `column`. `bracketed` chooses + the JSON `[…]` encoding (ideal class group) over the array `{…}` encoding (torsion). -/ + | iso (equiv lhsConst : Name) (column display : String) (bracketed : Bool) + +/-- Interpret a `PropRule` as a recogniser at a given polarity. -/ +def PropRule.match? : PropRule → Bool → Expr → Option Cond + | .flag c column, pos, e => if e.isAppOf c then some (boolCol pos column) else none + | .abelian column, pos, e => if isAbelianPattern e then some (boolCol pos column) else none + | .iso equiv lhsConst column display bracketed, pos, e => do + let (h, a, b) ← matchEquiv e + guard (h == equiv) + structCond pos a b lhsConst column display (if bracketed then fmtBrackets else fmtBraces) + /-! #### Reading and rendering a result row -/ /-- The first returned row of an LMFDB `/sql` response, if any. -/ @@ -224,10 +291,10 @@ structure TableInfo where /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/ orderBy : String /-- Recognisers for scalar quantities of this object (used inside comparisons). To teach - `lookup` a new column, add a matcher here. -/ - scalars : Array (Expr → Option Column) := #[] + `lookup` a new column, add a `ScalarRule` here. -/ + scalars : Array ScalarRule := #[] /-- Recognisers for boolean/structure properties of this object at a given polarity. -/ - props : Array (Bool → Expr → Option Cond) := #[] + props : Array PropRule := #[] /-- LMFDB elliptic-curve labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. -/ def ecUrl (label : String) : String := @@ -248,27 +315,13 @@ def nfFields : TableInfo where url label := s!"https://www.lmfdb.org/NumberField/{label}" orderBy := "disc_abs" scalars := #[ - fun e => match_expr e with - | NumberField.classNumber _ _ _ => some (col "class_number" "class number") - | _ => none, - fun e => match_expr e with - | Module.finrank r _ _ _ _ => if r.isConstOf ``Rat then some (col "degree" "degree") else none - | _ => none, - -- `|NumberField.discr F|` is `disc_abs`; the bare signed discriminant is split as - -- `disc_sign * disc_abs` (with `signed?` set so comparisons stay index-friendly). - fun e => match_expr e with - | abs _ _ _ x => match_expr x with - | NumberField.discr _ _ _ => some (col "disc_abs" "|discriminant|") - | _ => none - | NumberField.discr _ _ _ => - some (col "(disc_sign * disc_abs)" "discriminant" (some ("disc_sign", "disc_abs"))) - | _ => none] - props := #[ - -- ideal class group structure: `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)`. - fun pos e => match_expr e with - | MulEquiv a b _ _ => - structCond pos a b ``ClassGroup "class_group::text" "class group" fmtBrackets - | _ => none] + .const ``NumberField.classNumber "class_number" "class number", + .finrank ``Rat "degree" "degree", + -- `|discr F|` is `disc_abs`; the bare signed discriminant is split as `disc_sign·disc_abs`. + .absOf ``NumberField.discr "disc_abs" "|discriminant|", + .signed ``NumberField.discr "disc_sign" "disc_abs" "discriminant"] + -- ideal class group structure: `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)`. + props := #[.iso ``MulEquiv ``ClassGroup "class_group::text" "class group" true] /-- Elliptic curves over `ℚ`. -/ def ecCurvedata : TableInfo where @@ -279,19 +332,10 @@ def ecCurvedata : TableInfo where url := ecUrl orderBy := "conductor" scalars := #[ - fun e => match_expr e with - | Module.finrank r _ _ _ _ => if r.isConstOf ``Int then some (col "rank" "rank") else none - | _ => none, - fun e => match_expr e with - | Nat.card g => - if containsConst g ``AddCommGroup.torsion then some (col "torsion" "torsion") else none - | _ => none] - props := #[ - -- torsion subgroup structure: `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)`. - fun pos e => match_expr e with - | AddEquiv a b _ _ => - structCond pos a b ``AddCommGroup.torsion "torsion_structure" "torsion structure" fmtBraces - | _ => none] + .finrank ``Int "rank" "rank", + .cardOf ``AddCommGroup.torsion "torsion" "torsion"] + -- torsion subgroup structure: `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)`. + props := #[.iso ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false] /-- Finite groups. -/ def gpsGroups : TableInfo where @@ -302,11 +346,7 @@ def gpsGroups : TableInfo where url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" -- `order` is a SQL reserved word, so it must be quoted. orderBy := "\"order\"" - props := #[ - fun pos e => match_expr e with - | IsSimpleGroup _ _ => some (boolCol pos "simple") - | _ => none, - fun pos e => if isAbelianPattern e then some (boolCol pos "abelian") else none] + props := #[.flag ``IsSimpleGroup "simple", .abelian "abelian"] /-- All supported object families. To support a new one, add its `TableInfo` here. -/ def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] @@ -319,7 +359,7 @@ def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == n /-- Find the scalar column an expression denotes (trying every table's recognisers), together with the table it belongs to. -/ def findScalar (e : Expr) : Option (Column × String) := - tables.findSome? fun t => (t.scalars.findSome? (· e)).map (·, t.table) + tables.findSome? fun t => (t.scalars.findSome? (·.match? e)).map (·, t.table) /-- A column compared against an integer literal. A "signed" column stored as `sign * |·|` is case-split on the sign, so the comparison hits the indexed absolute-value column rather than @@ -355,7 +395,7 @@ partial def toCond (positive : Bool) (e : Expr) : Option Cond := match matchCmp e with | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b | none => tables.findSome? fun t => - (t.props.findSome? (· positive e)).map fun c => { c with table := some t.table } + (t.props.findSome? (·.match? positive e)).map fun c => { c with table := some t.table } /-- Translate a `Prop` into a SQL condition. -/ def toSqlCond (e : Expr) : Option Cond := toCond true e From b14a1aeebbcbe039ca7c62d08a59dde3ccb46bf0 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:07:58 +0100 Subject: [PATCH 14/34] drop the rule DSL for plain functions --- LeanBridge/Lookup/Lookup.lean | 169 +++++++++++++++++----------------- 1 file changed, 84 insertions(+), 85 deletions(-) diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index e0b06845..247e7bce 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -174,64 +174,66 @@ def matchEquiv (e : Expr) : Option (Name × Expr × Expr) := | MulEquiv a b _ _ => some (``MulEquiv, a, b) | _ => none -/-! #### Declarative recognisers - -Each table's columns and properties are described by *data* — `ScalarRule`/`PropRule` values. -All the `Expr`-matching metacode lives in the `match?` interpreters here, so teaching a table a -new column or property means adding a data constructor to its list (below), not writing a -matcher. -/ - -/-- How to recognise a scalar quantity of an object in a Lean expression. -/ -inductive ScalarRule where - /-- Head constant `c` applied to anything ↦ column `sql` (shown as `display`). -/ - | const (c : Name) (sql display : String) - /-- `Module.finrank` over base ring `ring` ↦ column (e.g. `ℚ` for degree, `ℤ` for rank). -/ - | finrank (ring : Name) (sql display : String) - /-- `Nat.card` of a type mentioning `inner` ↦ column (e.g. `AddCommGroup.torsion`). -/ - | cardOf (inner : Name) (sql display : String) - /-- `|c …|` (absolute value of a `c`-headed term) ↦ column. -/ - | absOf (c : Name) (sql display : String) - /-- Bare `c …` ↦ a signed quantity stored split as `signCol * absCol`. -/ - | signed (c : Name) (signCol absCol display : String) - -/-- Interpret a `ScalarRule` as a recogniser `Expr → Option Column`. -/ -def ScalarRule.match? : ScalarRule → Expr → Option Column - | .const c sql display, e => if e.isAppOf c then some (col sql display) else none - | .finrank ring sql display, e => - match_expr e with - | Module.finrank r _ _ _ _ => if r.isConstOf ring then some (col sql display) else none - | _ => none - | .cardOf inner sql display, e => - match_expr e with - | Nat.card g => if containsConst g inner then some (col sql display) else none - | _ => none - | .absOf c sql display, e => - match_expr e with - | abs _ _ _ x => if x.isAppOf c then some (col sql display) else none - | _ => none - | .signed c signCol absCol display, e => - if e.isAppOf c then some (col s!"({signCol} * {absCol})" display (some (signCol, absCol))) - else none - -/-- How to recognise a boolean/structure property of an object. -/ -inductive PropRule where - /-- Head constant `c` ↦ boolean column `column` (`= 't'`, or `= 'f'` when negated). -/ - | flag (c : Name) (column : String) - /-- The commutativity pattern `∀ a b, a * b = b * a` ↦ boolean column. -/ - | abelian (column : String) - /-- An isomorphism `lhs ≃ (∏ ZMod nᵢ)` via `equiv` (``AddEquiv``/``MulEquiv``), with `lhs` - mentioning `lhsConst`, compared against the invariant-factor `column`. `bracketed` chooses - the JSON `[…]` encoding (ideal class group) over the array `{…}` encoding (torsion). -/ - | iso (equiv lhsConst : Name) (column display : String) (bracketed : Bool) - -/-- Interpret a `PropRule` as a recogniser at a given polarity. -/ -def PropRule.match? : PropRule → Bool → Expr → Option Cond - | .flag c column, pos, e => if e.isAppOf c then some (boolCol pos column) else none - | .abelian column, pos, e => if isAbelianPattern e then some (boolCol pos column) else none - | .iso equiv lhsConst column display bracketed, pos, e => do - let (h, a, b) ← matchEquiv e - guard (h == equiv) - structCond pos a b lhsConst column display (if bracketed then fmtBrackets else fmtBraces) +/-! #### Recogniser combinators + +A column recogniser is just a function `Expr → Option Column`; a property recogniser is +`Bool → Expr → Option Cond` (the `Bool` is the wanted polarity). Each table below lists these +functions directly. The helpers here build the common shapes so the lists stay readable — +anything unusual is just a lambda of the same type. -/ + +/-- `headIs c "col" "name"`: matches any application of the constant `c` (e.g. +`NumberField.classNumber F`) to the column `col`, displayed as `name`. -/ +def headIs (c : Name) (sql display : String) : Expr → Option Column := + fun e => if e.isAppOf c then some (col sql display) else none + +/-- `finrankOver R "col" "name"`: matches `Module.finrank R _` (e.g. `R = ℚ` for a number +field's degree, `R = ℤ` for an elliptic curve's rank). -/ +def finrankOver (R : Name) (sql display : String) : Expr → Option Column := + fun e => match_expr e with + | Module.finrank r _ _ _ _ => if r.isConstOf R then some (col sql display) else none + | _ => none + +/-- `cardMentions c "col" "name"`: matches `Nat.card t` where the type `t` mentions `c` +(e.g. `Nat.card (AddCommGroup.torsion W.Point)`). -/ +def cardMentions (c : Name) (sql display : String) : Expr → Option Column := + fun e => match_expr e with + | Nat.card t => if containsConst t c then some (col sql display) else none + | _ => none + +/-- `absOf c "col" "name"`: matches `|x|` where `x` is an application of `c` +(e.g. `|NumberField.discr F|`). -/ +def absOf (c : Name) (sql display : String) : Expr → Option Column := + fun e => match_expr e with + | abs _ _ _ x => if x.isAppOf c then some (col sql display) else none + | _ => none + +/-- `signedValue c "signCol" "absCol" "name"`: matches an application of `c` whose value LMFDB +stores split as `signCol * absCol` (e.g. the signed discriminant). Recording the two columns +lets comparisons against a literal case-split on the sign and stay index-friendly. -/ +def signedValue (c : Name) (signCol absCol display : String) : Expr → Option Column := + fun e => if e.isAppOf c then + some (col s!"({signCol} * {absCol})" display (some (signCol, absCol))) else none + +/-- `flagIs c "col"`: matches any application of `c` (e.g. `IsSimpleGroup G`) to the boolean +column `col` (`= 't'`, or `= 'f'` when negated). -/ +def flagIs (c : Name) (column : String) : Bool → Expr → Option Cond := + fun pos e => if e.isAppOf c then some (boolCol pos column) else none + +/-- `isAbelian "col"`: matches the commutativity statement `∀ a b, a * b = b * a` to the +boolean column `col`. -/ +def isAbelian (column : String) : Bool → Expr → Option Cond := + fun pos e => if isAbelianPattern e then some (boolCol pos column) else none + +/-- `isoStructure equiv c "col" "name" bracketed`: matches an isomorphism `lhs ≃ (∏ ZMod nᵢ)` +written with `equiv` (``AddEquiv`` or ``MulEquiv``) and `lhs` mentioning `c`, comparing the +invariant factors against `col`. `bracketed` selects the JSON `[…]` encoding (ideal class +group) over the array `{…}` encoding (torsion structure). -/ +def isoStructure (equiv c : Name) (column display : String) (bracketed : Bool) : + Bool → Expr → Option Cond := + fun pos e => do + let (h, a, b) ← matchEquiv e + guard (h == equiv) + structCond pos a b c column display (if bracketed then fmtBrackets else fmtBraces) /-! #### Reading and rendering a result row -/ @@ -290,20 +292,11 @@ structure TableInfo where url : String → String /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/ orderBy : String - /-- Recognisers for scalar quantities of this object (used inside comparisons). To teach - `lookup` a new column, add a `ScalarRule` here. -/ - scalars : Array ScalarRule := #[] - /-- Recognisers for boolean/structure properties of this object at a given polarity. -/ - props : Array PropRule := #[] - -/-- LMFDB elliptic-curve labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. -/ -def ecUrl (label : String) : String := - match label.splitOn "." with - | [conductor, iso] => - let letters := iso.takeWhile Char.isAlpha - let number := iso.dropWhile Char.isAlpha - s!"https://www.lmfdb.org/EllipticCurve/Q/{conductor}/{letters}/{number}" - | _ => s!"https://www.lmfdb.org/EllipticCurve/Q/{label}" + /-- Recognisers for scalar quantities of this object (used inside comparisons). Each is an + `Expr → Option Column`; build them with `headIs`/`finrankOver`/… or write a lambda. -/ + scalars : Array (Expr → Option Column) := #[] + /-- Recognisers for boolean/structure properties (the `Bool` is the wanted polarity). -/ + props : Array (Bool → Expr → Option Cond) := #[] /-- Number fields. -/ def nfFields : TableInfo where @@ -315,13 +308,13 @@ def nfFields : TableInfo where url label := s!"https://www.lmfdb.org/NumberField/{label}" orderBy := "disc_abs" scalars := #[ - .const ``NumberField.classNumber "class_number" "class number", - .finrank ``Rat "degree" "degree", - -- `|discr F|` is `disc_abs`; the bare signed discriminant is split as `disc_sign·disc_abs`. - .absOf ``NumberField.discr "disc_abs" "|discriminant|", - .signed ``NumberField.discr "disc_sign" "disc_abs" "discriminant"] + headIs ``NumberField.classNumber "class_number" "class number", + finrankOver ``Rat "degree" "degree", + -- `|discr F|` is `disc_abs`; the bare signed discriminant is split as `disc_sign · disc_abs`. + absOf ``NumberField.discr "disc_abs" "|discriminant|", + signedValue ``NumberField.discr "disc_sign" "disc_abs" "discriminant"] -- ideal class group structure: `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)`. - props := #[.iso ``MulEquiv ``ClassGroup "class_group::text" "class group" true] + props := #[isoStructure ``MulEquiv ``ClassGroup "class_group::text" "class group" true] /-- Elliptic curves over `ℚ`. -/ def ecCurvedata : TableInfo where @@ -329,13 +322,19 @@ def ecCurvedata : TableInfo where labelCol := "lmfdb_label" descSelects := #["ainvs::text AS ainvs"] describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" - url := ecUrl + -- LMFDB EC labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. + url label := + match label.splitOn "." with + | [conductor, iso] => + s!"https://www.lmfdb.org/EllipticCurve/Q/{conductor}/\ + {iso.takeWhile Char.isAlpha}/{iso.dropWhile Char.isAlpha}" + | _ => s!"https://www.lmfdb.org/EllipticCurve/Q/{label}" orderBy := "conductor" scalars := #[ - .finrank ``Int "rank" "rank", - .cardOf ``AddCommGroup.torsion "torsion" "torsion"] + finrankOver ``Int "rank" "rank", + cardMentions ``AddCommGroup.torsion "torsion" "torsion"] -- torsion subgroup structure: `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)`. - props := #[.iso ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false] + props := #[isoStructure ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false] /-- Finite groups. -/ def gpsGroups : TableInfo where @@ -346,7 +345,7 @@ def gpsGroups : TableInfo where url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" -- `order` is a SQL reserved word, so it must be quoted. orderBy := "\"order\"" - props := #[.flag ``IsSimpleGroup "simple", .abelian "abelian"] + props := #[flagIs ``IsSimpleGroup "simple", isAbelian "abelian"] /-- All supported object families. To support a new one, add its `TableInfo` here. -/ def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] @@ -359,7 +358,7 @@ def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == n /-- Find the scalar column an expression denotes (trying every table's recognisers), together with the table it belongs to. -/ def findScalar (e : Expr) : Option (Column × String) := - tables.findSome? fun t => (t.scalars.findSome? (·.match? e)).map (·, t.table) + tables.findSome? fun t => (t.scalars.findSome? (· e)).map (·, t.table) /-- A column compared against an integer literal. A "signed" column stored as `sign * |·|` is case-split on the sign, so the comparison hits the indexed absolute-value column rather than @@ -395,7 +394,7 @@ partial def toCond (positive : Bool) (e : Expr) : Option Cond := match matchCmp e with | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b | none => tables.findSome? fun t => - (t.props.findSome? (·.match? positive e)).map fun c => { c with table := some t.table } + (t.props.findSome? (· positive e)).map fun c => { c with table := some t.table } /-- Translate a `Prop` into a SQL condition. -/ def toSqlCond (e : Expr) : Option Cond := toCond true e From b1112ac48d4d64f499c8797c778682accff5551b Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:23:27 +0100 Subject: [PATCH 15/34] split into Basic / Tables / Lookup --- LeanBridge/Lookup/Basic.lean | 269 ++++++++++++++++++++++++++++ LeanBridge/Lookup/Lookup.lean | 328 +--------------------------------- LeanBridge/Lookup/Tables.lean | 79 ++++++++ 3 files changed, 356 insertions(+), 320 deletions(-) create mode 100644 LeanBridge/Lookup/Basic.lean create mode 100644 LeanBridge/Lookup/Tables.lean diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean new file mode 100644 index 00000000..5c8521fd --- /dev/null +++ b/LeanBridge/Lookup/Basic.lean @@ -0,0 +1,269 @@ +import Mathlib + +/-! # `lookup` vocabulary + +The table-agnostic building blocks shared by the rest of the tactic: the value types +(`Column`, `Cond`, `Cmp`), low-level `Expr` matchers, the recogniser combinators used to +describe a table's columns/properties, small result-row utilities, and the `TableInfo` record. + +The concrete tables live in `LeanBridge.Lookup.Tables`; the tactic itself in +`LeanBridge.Lookup.Lookup`. -/ + +open Lean Meta + +namespace Lookup + +/-! ## Literals -/ + +/-- Extract a natural-number literal from `e`, handling `@OfNat.ofNat _ n _`. -/ +def getNatLit? (e : Expr) : Option Nat := + match_expr e with + | OfNat.ofNat _ n _ => n.rawNatLit? + | _ => e.rawNatLit? + +/-- Extract an integer literal, handling a leading negation `@Neg.neg _ _ n`. -/ +def getIntLit? (e : Expr) : Option Int := + match_expr e with + | Neg.neg _ _ a => (getNatLit? a).map fun n => -(n : Int) + | _ => (getNatLit? e).map Int.ofNat + +/-! ## Comparison operators -/ + +/-- A comparison operator we know how to send to SQL. -/ +inductive Cmp | eq | ne | le | lt | ge | gt + deriving Inhabited, BEq + +namespace Cmp + +/-- The SQL spelling of the operator. -/ +def toSql : Cmp → String + | eq => "=" | ne => "<>" | le => "<=" | lt => "<" | ge => ">=" | gt => ">" + +/-- The operator whose truth value is the logical negation of this one. -/ +def negate : Cmp → Cmp + | eq => ne | ne => eq | le => gt | lt => ge | ge => lt | gt => le + +/-- The operator that holds after swapping the operands (equivalently, after negating both +sides of an order comparison). -/ +def reverse : Cmp → Cmp + | eq => eq | ne => ne | le => ge | lt => gt | ge => le | gt => lt + +end Cmp + +/-! ## Columns and conditions -/ + +/-- A scalar quantity of an object: an SQL column expression and a human-readable name. A +quantity stored split as `sign * |·|` records those two columns in `signed?`, so comparisons +against a literal can be made index-friendly. -/ +structure Column where + sql : String + display : String + signed? : Option (String × String) := none + +/-- A translated SQL condition: the boolean SQL, the columns it references (as +`(displayName, selectExpr)` pairs, for reporting), and the LMFDB table it forces. -/ +structure Cond where + sql : String + refs : Array (String × String) := #[] + table : Option String := none + +/-- Build a `Column`. -/ +def col (sql display : String) (signed? : Option (String × String) := none) : Column := + { sql, display, signed? } + +/-- A boolean-flag condition `column = 't'` (or `column = 'f'` when negated). -/ +def boolCol (positive : Bool) (column : String) : Cond := + { sql := s!"{column} = {if positive then "'t'" else "'f'"}", refs := #[(column, column)] } + +/-! ## Low-level `Expr` matchers -/ + +/-- Match a comparison `Prop`, returning the operator and the two operands. -/ +def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := + match_expr e with + | Eq _ a b => some (.eq, a, b) + | Ne _ a b => some (.ne, a, b) + | LE.le _ _ a b => some (.le, a, b) + | LT.lt _ _ a b => some (.lt, a, b) + | GE.ge _ _ a b => some (.ge, a, b) + | GT.gt _ _ a b => some (.gt, a, b) + | _ => none + +/-- Whether `e` mentions the constant `n` anywhere. -/ +def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome + +/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` +wrappers stripped) as its list of moduli, in the order written. -/ +partial def cyclicFactors? (e : Expr) : Option (Array Nat) := + match_expr e with + | ZMod n => (getNatLit? n).map (#[·]) + | Multiplicative a => cyclicFactors? a + | Prod a b => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) + | _ => none + +/-- LMFDB encodes the torsion structure as a brace array `{2,4}` and the ideal class group as +a JSON bracket array `[2, 2]`. -/ +def fmtBraces (f : Array Nat) : String := "{" ++ ",".intercalate (f.toList.map toString) ++ "}" +def fmtBrackets (f : Array Nat) : String := "[" ++ ", ".intercalate (f.toList.map toString) ++ "]" + +/-- The de Bruijn index of a bound variable, if `e` is one. -/ +def bvarIdx? : Expr → Option Nat + | .bvar n => some n + | _ => none + +/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` ("the group is abelian"), +allowing the two multiplications to have swapped operands. -/ +def isAbelianPattern (e : Expr) : Bool := + match e with + | .forallE _ _ (.forallE _ _ body _) _ => + match_expr body with + | Eq _ lhs rhs => + match_expr lhs with + | HMul.hMul _ _ _ _ l1 l2 => + match_expr rhs with + | HMul.hMul _ _ _ _ r1 r2 => + (bvarIdx? l1 == bvarIdx? r2) && (bvarIdx? l2 == bvarIdx? r1) && + (bvarIdx? l1).isSome && (bvarIdx? l1 != bvarIdx? l2) + | _ => false + | _ => false + | _ => false + | _ => false + +/-- Translate an abelian-group-structure claim `lhs ≃ rhs` (with `rhs` a product of cyclics) +into an invariant-factor column comparison; `positive := false` negates it (`<>`). -/ +def structCond (positive : Bool) (lhs rhs : Expr) (lhsConst : Name) + (column display : String) (fmt : Array Nat → String) : Option Cond := do + guard (containsConst lhs lhsConst) + let factors ← cyclicFactors? rhs + return { sql := s!"{column} {if positive then "=" else "<>"} '{fmt factors}'", + refs := #[(display, column.replace "::text" "")] } + +/-- Recognise an isomorphism `A ≃+ B` or `A ≃* B`, returning the equiv's head constant and the +two sides. -/ +def matchEquiv (e : Expr) : Option (Name × Expr × Expr) := + match_expr e with + | AddEquiv a b _ _ => some (``AddEquiv, a, b) + | MulEquiv a b _ _ => some (``MulEquiv, a, b) + | _ => none + +/-! ## Recogniser combinators + +A column recogniser is a function `Expr → Option Column`; a property recogniser is +`Bool → Expr → Option Cond` (the `Bool` is the wanted polarity). A table lists these functions +directly; the helpers below build the common shapes, and anything unusual is just a lambda of +the same type. -/ + +/-- `headIs c "col" "name"`: matches any application of the constant `c` (e.g. +`NumberField.classNumber F`) to the column `col`, displayed as `name`. -/ +def headIs (c : Name) (sql display : String) : Expr → Option Column := + fun e => if e.isAppOf c then some (col sql display) else none + +/-- `finrankOver R "col" "name"`: matches `Module.finrank R _` (e.g. `R = ℚ` for a number +field's degree, `R = ℤ` for an elliptic curve's rank). -/ +def finrankOver (R : Name) (sql display : String) : Expr → Option Column := + fun e => match_expr e with + | Module.finrank r _ _ _ _ => if r.isConstOf R then some (col sql display) else none + | _ => none + +/-- `cardMentions c "col" "name"`: matches `Nat.card t` where the type `t` mentions `c` +(e.g. `Nat.card (AddCommGroup.torsion W.Point)`). -/ +def cardMentions (c : Name) (sql display : String) : Expr → Option Column := + fun e => match_expr e with + | Nat.card t => if containsConst t c then some (col sql display) else none + | _ => none + +/-- `absOf c "col" "name"`: matches `|x|` where `x` is an application of `c` +(e.g. `|NumberField.discr F|`). -/ +def absOf (c : Name) (sql display : String) : Expr → Option Column := + fun e => match_expr e with + | abs _ _ _ x => if x.isAppOf c then some (col sql display) else none + | _ => none + +/-- `signedValue c "signCol" "absCol" "name"`: matches an application of `c` whose value LMFDB +stores split as `signCol * absCol` (e.g. the signed discriminant). Recording the two columns +lets comparisons against a literal case-split on the sign and stay index-friendly. -/ +def signedValue (c : Name) (signCol absCol display : String) : Expr → Option Column := + fun e => if e.isAppOf c then + some (col s!"({signCol} * {absCol})" display (some (signCol, absCol))) else none + +/-- `flagIs c "col"`: matches any application of `c` (e.g. `IsSimpleGroup G`) to the boolean +column `col` (`= 't'`, or `= 'f'` when negated). -/ +def flagIs (c : Name) (column : String) : Bool → Expr → Option Cond := + fun pos e => if e.isAppOf c then some (boolCol pos column) else none + +/-- `isAbelian "col"`: matches the commutativity statement `∀ a b, a * b = b * a` to the +boolean column `col`. -/ +def isAbelian (column : String) : Bool → Expr → Option Cond := + fun pos e => if isAbelianPattern e then some (boolCol pos column) else none + +/-- `isoStructure equiv c "col" "name" bracketed`: matches an isomorphism `lhs ≃ (∏ ZMod nᵢ)` +written with `equiv` (``AddEquiv`` or ``MulEquiv``) and `lhs` mentioning `c`, comparing the +invariant factors against `col`. `bracketed` selects the JSON `[…]` encoding (ideal class +group) over the array `{…}` encoding (torsion structure). -/ +def isoStructure (equiv c : Name) (column display : String) (bracketed : Bool) : + Bool → Expr → Option Cond := + fun pos e => do + let (h, a, b) ← matchEquiv e + guard (h == equiv) + structCond pos a b c column display (if bracketed then fmtBrackets else fmtBraces) + +/-! ## Result rows -/ + +/-- The first returned row of an LMFDB `/sql` response, if any. -/ +def firstRow? (j : Json) : Option Json := + match j.getObjVal? "rows" with + | .ok (.arr rs) => rs[0]? + | _ => none + +/-- Read a (text-cast) field of a row as a string. -/ +def rowStr (row : Json) (key : String) : String := + (row.getObjValAs? String key).toOption.getD "?" + +/-- Pretty-print the integer monomial `c * x^e` (its sign is handled by the caller). -/ +def monomial (c : Int) (e : Nat) : String := + if e == 0 then toString c.natAbs + else + let base := if e == 1 then "x" else s!"x^{e}" + if c.natAbs == 1 then base else s!"{c.natAbs}*{base}" + +/-- Format an LMFDB `coeffs` array (e.g. `{-1,-1,1}`, lowest degree first) as a polynomial +in `x`, highest degree first. -/ +def formatPoly (coeffs : String) : String := Id.run do + let stripped := (coeffs.replace "{" "").replace "}" "" + let cs := (stripped.splitOn ",").filterMap String.toInt? + let n := cs.length + let mut out := "" + for i in [0:n] do + let e := n - 1 - i + let c := cs[e]! + if c == 0 then continue + let term := monomial c e + if out.isEmpty then + out := if c < 0 then s!"-{term}" else term + else + out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}") + return if out.isEmpty then "0" else out + +/-! ## LMFDB tables -/ + +/-- Everything needed to query one LMFDB table and recognise the Lean expressions that map into +its columns. The concrete instances live in `LeanBridge.Lookup.Tables`. -/ +structure TableInfo where + /-- The SQL table name. -/ + table : String + /-- The column holding the LMFDB label (selected `AS label`). -/ + labelCol : String + /-- Extra SELECT fragments for the descriptive data (e.g. the defining polynomial). -/ + descSelects : Array String + /-- Render the descriptive data of a result row as plain text. -/ + describe : Json → String + /-- Build the LMFDB page URL from a label. -/ + url : String → String + /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/ + orderBy : String + /-- Recognisers for scalar quantities of this object (used inside comparisons). Each is an + `Expr → Option Column`; build them with `headIs`/`finrankOver`/… or write a lambda. -/ + scalars : Array (Expr → Option Column) := #[] + /-- Recognisers for boolean/structure properties (the `Bool` is the wanted polarity). -/ + props : Array (Bool → Expr → Option Cond) := #[] + +end Lookup diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index 247e7bce..994c242f 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -1,4 +1,4 @@ -import Mathlib +import LeanBridge.Lookup.Tables import ProofWidgets.Component.HtmlDisplay /-! # The `lookup` tactic @@ -8,8 +8,8 @@ LMFDB that searches for a *counterexample* (a database object satisfying all the **violating** the goal), and reports it if one is found. It never closes the goal: a hit shows the statement is false, and a miss is only evidence (the database is not exhaustive). -To support a new object family, add a `TableInfo` to `tables`. To teach an existing family a -new column or property, add a recogniser to that table's `scalars`/`props`. -/ +The vocabulary lives in `LeanBridge.Lookup.Basic` and the table registry in +`LeanBridge.Lookup.Tables`; this file wires them into the query, the report, and the tactic. -/ open Lean Elab Tactic Meta @@ -17,7 +17,7 @@ namespace Lookup initialize registerTraceClass `lookup -/-! #### Querying LMFDB -/ +/-! ## Querying LMFDB -/ /-- Build the request body for an LMFDB `/sql` call. -/ def sqlRequestBody (sql : String) (limit : Nat := 1000) : Json := @@ -39,321 +39,7 @@ def runSql (sql : String) : MetaM Json := do | throwError s!"failed to parse response:\n{out.stdout}" return result -/-! #### Literals -/ - -/-- Extract a natural-number literal from `e`, handling `@OfNat.ofNat _ n _`. -/ -def getNatLit? (e : Expr) : Option Nat := - match_expr e with - | OfNat.ofNat _ n _ => n.rawNatLit? - | _ => e.rawNatLit? - -/-- Extract an integer literal, handling a leading negation `@Neg.neg _ _ n`. -/ -def getIntLit? (e : Expr) : Option Int := - match_expr e with - | Neg.neg _ _ a => (getNatLit? a).map fun n => -(n : Int) - | _ => (getNatLit? e).map Int.ofNat - -/-! #### Comparison operators -/ - -/-- A comparison operator we know how to send to SQL. -/ -inductive Cmp | eq | ne | le | lt | ge | gt - deriving Inhabited, BEq - -namespace Cmp - -/-- The SQL spelling of the operator. -/ -def toSql : Cmp → String - | eq => "=" | ne => "<>" | le => "<=" | lt => "<" | ge => ">=" | gt => ">" - -/-- The operator whose truth value is the logical negation of this one. -/ -def negate : Cmp → Cmp - | eq => ne | ne => eq | le => gt | lt => ge | ge => lt | gt => le - -/-- The operator that holds after swapping the operands (equivalently, after negating both -sides of an order comparison). -/ -def reverse : Cmp → Cmp - | eq => eq | ne => ne | le => ge | lt => gt | ge => le | gt => lt - -end Cmp - -/-! #### Translating Lean expressions to SQL - -A `Column` is a quantity of an object (an SQL column expression plus a display name); a `Cond` -is a translated SQL boolean condition. The recognisers that map Lean expressions to columns -and conditions live *with each table* in the registry below, so adding a column or property to -a table is a local, one-line change. The generic plumbing here is table-agnostic. -/ - -/-- A scalar quantity of an object: an SQL column expression and a human-readable name. A -quantity stored split as `sign * |·|` records those two columns in `signed?`, so comparisons -against a literal can be made index-friendly. -/ -structure Column where - sql : String - display : String - signed? : Option (String × String) := none - -/-- A translated SQL condition: the boolean SQL, the columns it references (as -`(displayName, selectExpr)` pairs, for reporting), and the LMFDB table it forces. -/ -structure Cond where - sql : String - refs : Array (String × String) := #[] - table : Option String := none - -/-- Build a `Column`. -/ -def col (sql display : String) (signed? : Option (String × String) := none) : Column := - { sql, display, signed? } - -/-- A boolean-flag condition `column = 't'` (or `column = 'f'` when negated). -/ -def boolCol (positive : Bool) (column : String) : Cond := - { sql := s!"{column} = {if positive then "'t'" else "'f'"}", refs := #[(column, column)] } - -/-- Match a comparison `Prop`, returning the operator and the two operands. -/ -def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := - match_expr e with - | Eq _ a b => some (.eq, a, b) - | Ne _ a b => some (.ne, a, b) - | LE.le _ _ a b => some (.le, a, b) - | LT.lt _ _ a b => some (.lt, a, b) - | GE.ge _ _ a b => some (.ge, a, b) - | GT.gt _ _ a b => some (.gt, a, b) - | _ => none - -/-- Whether `e` mentions the constant `n` anywhere. -/ -def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome - -/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` -wrappers stripped) as its list of moduli, in the order written. -/ -partial def cyclicFactors? (e : Expr) : Option (Array Nat) := - match_expr e with - | ZMod n => (getNatLit? n).map (#[·]) - | Multiplicative a => cyclicFactors? a - | Prod a b => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) - | _ => none - -/-- LMFDB encodes the torsion structure as a brace array `{2,4}` and the ideal class group as -a JSON bracket array `[2, 2]`. -/ -def fmtBraces (f : Array Nat) : String := "{" ++ ",".intercalate (f.toList.map toString) ++ "}" -def fmtBrackets (f : Array Nat) : String := "[" ++ ", ".intercalate (f.toList.map toString) ++ "]" - -/-- The de Bruijn index of a bound variable, if `e` is one. -/ -def bvarIdx? : Expr → Option Nat - | .bvar n => some n - | _ => none - -/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` ("the group is abelian"), -allowing the two multiplications to have swapped operands. -/ -def isAbelianPattern (e : Expr) : Bool := - match e with - | .forallE _ _ (.forallE _ _ body _) _ => - match_expr body with - | Eq _ lhs rhs => - match_expr lhs with - | HMul.hMul _ _ _ _ l1 l2 => - match_expr rhs with - | HMul.hMul _ _ _ _ r1 r2 => - (bvarIdx? l1 == bvarIdx? r2) && (bvarIdx? l2 == bvarIdx? r1) && - (bvarIdx? l1).isSome && (bvarIdx? l1 != bvarIdx? l2) - | _ => false - | _ => false - | _ => false - | _ => false - -/-- Translate an abelian-group-structure claim `lhs ≃ rhs` (with `rhs` a product of cyclics) -into an invariant-factor column comparison; `positive := false` negates it (`<>`). -/ -def structCond (positive : Bool) (lhs rhs : Expr) (lhsConst : Name) - (column display : String) (fmt : Array Nat → String) : Option Cond := do - guard (containsConst lhs lhsConst) - let factors ← cyclicFactors? rhs - return { sql := s!"{column} {if positive then "=" else "<>"} '{fmt factors}'", - refs := #[(display, column.replace "::text" "")] } - -/-- Recognise an isomorphism `A ≃+ B` or `A ≃* B`, returning the equiv's head constant and the -two sides. -/ -def matchEquiv (e : Expr) : Option (Name × Expr × Expr) := - match_expr e with - | AddEquiv a b _ _ => some (``AddEquiv, a, b) - | MulEquiv a b _ _ => some (``MulEquiv, a, b) - | _ => none - -/-! #### Recogniser combinators - -A column recogniser is just a function `Expr → Option Column`; a property recogniser is -`Bool → Expr → Option Cond` (the `Bool` is the wanted polarity). Each table below lists these -functions directly. The helpers here build the common shapes so the lists stay readable — -anything unusual is just a lambda of the same type. -/ - -/-- `headIs c "col" "name"`: matches any application of the constant `c` (e.g. -`NumberField.classNumber F`) to the column `col`, displayed as `name`. -/ -def headIs (c : Name) (sql display : String) : Expr → Option Column := - fun e => if e.isAppOf c then some (col sql display) else none - -/-- `finrankOver R "col" "name"`: matches `Module.finrank R _` (e.g. `R = ℚ` for a number -field's degree, `R = ℤ` for an elliptic curve's rank). -/ -def finrankOver (R : Name) (sql display : String) : Expr → Option Column := - fun e => match_expr e with - | Module.finrank r _ _ _ _ => if r.isConstOf R then some (col sql display) else none - | _ => none - -/-- `cardMentions c "col" "name"`: matches `Nat.card t` where the type `t` mentions `c` -(e.g. `Nat.card (AddCommGroup.torsion W.Point)`). -/ -def cardMentions (c : Name) (sql display : String) : Expr → Option Column := - fun e => match_expr e with - | Nat.card t => if containsConst t c then some (col sql display) else none - | _ => none - -/-- `absOf c "col" "name"`: matches `|x|` where `x` is an application of `c` -(e.g. `|NumberField.discr F|`). -/ -def absOf (c : Name) (sql display : String) : Expr → Option Column := - fun e => match_expr e with - | abs _ _ _ x => if x.isAppOf c then some (col sql display) else none - | _ => none - -/-- `signedValue c "signCol" "absCol" "name"`: matches an application of `c` whose value LMFDB -stores split as `signCol * absCol` (e.g. the signed discriminant). Recording the two columns -lets comparisons against a literal case-split on the sign and stay index-friendly. -/ -def signedValue (c : Name) (signCol absCol display : String) : Expr → Option Column := - fun e => if e.isAppOf c then - some (col s!"({signCol} * {absCol})" display (some (signCol, absCol))) else none - -/-- `flagIs c "col"`: matches any application of `c` (e.g. `IsSimpleGroup G`) to the boolean -column `col` (`= 't'`, or `= 'f'` when negated). -/ -def flagIs (c : Name) (column : String) : Bool → Expr → Option Cond := - fun pos e => if e.isAppOf c then some (boolCol pos column) else none - -/-- `isAbelian "col"`: matches the commutativity statement `∀ a b, a * b = b * a` to the -boolean column `col`. -/ -def isAbelian (column : String) : Bool → Expr → Option Cond := - fun pos e => if isAbelianPattern e then some (boolCol pos column) else none - -/-- `isoStructure equiv c "col" "name" bracketed`: matches an isomorphism `lhs ≃ (∏ ZMod nᵢ)` -written with `equiv` (``AddEquiv`` or ``MulEquiv``) and `lhs` mentioning `c`, comparing the -invariant factors against `col`. `bracketed` selects the JSON `[…]` encoding (ideal class -group) over the array `{…}` encoding (torsion structure). -/ -def isoStructure (equiv c : Name) (column display : String) (bracketed : Bool) : - Bool → Expr → Option Cond := - fun pos e => do - let (h, a, b) ← matchEquiv e - guard (h == equiv) - structCond pos a b c column display (if bracketed then fmtBrackets else fmtBraces) - -/-! #### Reading and rendering a result row -/ - -/-- The first returned row of an LMFDB `/sql` response, if any. -/ -def firstRow? (j : Json) : Option Json := - match j.getObjVal? "rows" with - | .ok (.arr rs) => rs[0]? - | _ => none - -/-- Read a (text-cast) field of a row as a string. -/ -def rowStr (row : Json) (key : String) : String := - (row.getObjValAs? String key).toOption.getD "?" - -/-- Pretty-print the integer monomial `c * x^e` (its sign is handled by the caller). -/ -def monomial (c : Int) (e : Nat) : String := - if e == 0 then toString c.natAbs - else - let base := if e == 1 then "x" else s!"x^{e}" - if c.natAbs == 1 then base else s!"{c.natAbs}*{base}" - -/-- Format an LMFDB `coeffs` array (e.g. `{-1,-1,1}`, lowest degree first) as a polynomial -in `x`, highest degree first. -/ -def formatPoly (coeffs : String) : String := Id.run do - let stripped := (coeffs.replace "{" "").replace "}" "" - let cs := (stripped.splitOn ",").filterMap String.toInt? - let n := cs.length - let mut out := "" - for i in [0:n] do - let e := n - 1 - i - let c := cs[e]! - if c == 0 then continue - let term := monomial c e - if out.isEmpty then - out := if c < 0 then s!"-{term}" else term - else - out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}") - return if out.isEmpty then "0" else out - -/-! #### LMFDB tables - -Each supported object family corresponds to a table, knowing how to select its label and -descriptive data, render that data, build a link to the LMFDB page, and recognise the Lean -expressions that map into its columns. -/ - -/-- Per-table knowledge needed to query and report a counterexample. -/ -structure TableInfo where - /-- The SQL table name. -/ - table : String - /-- The column holding the LMFDB label (selected `AS label`). -/ - labelCol : String - /-- Extra SELECT fragments for the descriptive data (e.g. the defining polynomial). -/ - descSelects : Array String - /-- Render the descriptive data of a result row as plain text. -/ - describe : Json → String - /-- Build the LMFDB page URL from a label. -/ - url : String → String - /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/ - orderBy : String - /-- Recognisers for scalar quantities of this object (used inside comparisons). Each is an - `Expr → Option Column`; build them with `headIs`/`finrankOver`/… or write a lambda. -/ - scalars : Array (Expr → Option Column) := #[] - /-- Recognisers for boolean/structure properties (the `Bool` is the wanted polarity). -/ - props : Array (Bool → Expr → Option Cond) := #[] - -/-- Number fields. -/ -def nfFields : TableInfo where - table := "nf_fields" - labelCol := "label" - descSelects := #["coeffs::text AS coeffs"] - describe row := s!"number field {rowStr row "label"}, with minimal polynomial \ - {formatPoly (rowStr row "coeffs")}" - url label := s!"https://www.lmfdb.org/NumberField/{label}" - orderBy := "disc_abs" - scalars := #[ - headIs ``NumberField.classNumber "class_number" "class number", - finrankOver ``Rat "degree" "degree", - -- `|discr F|` is `disc_abs`; the bare signed discriminant is split as `disc_sign · disc_abs`. - absOf ``NumberField.discr "disc_abs" "|discriminant|", - signedValue ``NumberField.discr "disc_sign" "disc_abs" "discriminant"] - -- ideal class group structure: `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)`. - props := #[isoStructure ``MulEquiv ``ClassGroup "class_group::text" "class group" true] - -/-- Elliptic curves over `ℚ`. -/ -def ecCurvedata : TableInfo where - table := "ec_curvedata" - labelCol := "lmfdb_label" - descSelects := #["ainvs::text AS ainvs"] - describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" - -- LMFDB EC labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. - url label := - match label.splitOn "." with - | [conductor, iso] => - s!"https://www.lmfdb.org/EllipticCurve/Q/{conductor}/\ - {iso.takeWhile Char.isAlpha}/{iso.dropWhile Char.isAlpha}" - | _ => s!"https://www.lmfdb.org/EllipticCurve/Q/{label}" - orderBy := "conductor" - scalars := #[ - finrankOver ``Int "rank" "rank", - cardMentions ``AddCommGroup.torsion "torsion" "torsion"] - -- torsion subgroup structure: `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)`. - props := #[isoStructure ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false] - -/-- Finite groups. -/ -def gpsGroups : TableInfo where - table := "gps_groups" - labelCol := "label" - descSelects := #["tex_name::text AS tex_name"] - describe row := s!"group {rowStr row "label"} ({rowStr row "tex_name"})" - url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" - -- `order` is a SQL reserved word, so it must be quoted. - orderBy := "\"order\"" - props := #[flagIs ``IsSimpleGroup "simple", isAbelian "abelian"] - -/-- All supported object families. To support a new one, add its `TableInfo` here. -/ -def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] - -/-- The table configuration for a table name. -/ -def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == name) - -/-! #### Dispatch: translating a `Prop` to a SQL condition -/ +/-! ## Dispatch: translating a `Prop` to a SQL condition -/ /-- Find the scalar column an expression denotes (trying every table's recognisers), together with the table it belongs to. -/ @@ -402,7 +88,7 @@ def toSqlCond (e : Expr) : Option Cond := toCond true e /-- Translate the *negation* of a `Prop` into a SQL condition (used for the goal). -/ def toSqlCondNeg (e : Expr) : Option Cond := toCond false e -/-! #### Assembling the query and report -/ +/-! ## Assembling the query and report -/ /-- Deduplicate referenced quantities by their SQL expression, preserving order. -/ def dedupRefs (refs : Array (String × String)) : Array (String × String) := Id.run do @@ -456,6 +142,8 @@ def reportAlt (info : TableInfo) (row : Json) (items : Array (String × String)) {", ".intercalate (valueStrs row items).toList}\n\ {info.url (rowStr row "label")}" +/-! ## The tactic -/ + /-- Translate the hypotheses in context into SQL conditions. A hypothesis that *is* a comparison but that we cannot translate is reported as a warning (and dropped), since silently ignoring it would weaken any "no counterexample" conclusion. -/ diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean new file mode 100644 index 00000000..0861c701 --- /dev/null +++ b/LeanBridge/Lookup/Tables.lean @@ -0,0 +1,79 @@ +import LeanBridge.Lookup.Basic + +/-! # LMFDB table registry + +The object families `lookup` knows about. **To support a new family, add a `TableInfo` here** +(and list it in `tables`); **to teach an existing family a new column or property, add a +recogniser** to its `scalars`/`props` using the combinators from `LeanBridge.Lookup.Basic`. -/ + +open Lean + +namespace Lookup + +/-- Number fields. -/ +def nfFields : TableInfo where + table := "nf_fields" + labelCol := "label" + descSelects := #["coeffs::text AS coeffs"] + describe row := s!"number field {rowStr row "label"}, with minimal polynomial \ + {formatPoly (rowStr row "coeffs")}" + url label := s!"https://www.lmfdb.org/NumberField/{label}" + orderBy := "disc_abs" + scalars := #[ + -- `NumberField.classNumber F` ↦ class_number + headIs ``NumberField.classNumber "class_number" "class number", + -- `Module.finrank ℚ F` ↦ degree + finrankOver ``Rat "degree" "degree", + -- `|NumberField.discr F|` ↦ disc_abs + absOf ``NumberField.discr "disc_abs" "|discriminant|", + -- `NumberField.discr F` ↦ disc_sign · disc_abs (signed, sign-split on comparison) + signedValue ``NumberField.discr "disc_sign" "disc_abs" "discriminant"] + props := #[ + -- `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)` ↦ class_group = [n₁, …] + isoStructure ``MulEquiv ``ClassGroup "class_group::text" "class group" true] + +/-- Elliptic curves over `ℚ`. -/ +def ecCurvedata : TableInfo where + table := "ec_curvedata" + labelCol := "lmfdb_label" + descSelects := #["ainvs::text AS ainvs"] + describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" + -- LMFDB EC labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. + url label := + match label.splitOn "." with + | [conductor, iso] => + s!"https://www.lmfdb.org/EllipticCurve/Q/{conductor}/\ + {iso.takeWhile Char.isAlpha}/{iso.dropWhile Char.isAlpha}" + | _ => s!"https://www.lmfdb.org/EllipticCurve/Q/{label}" + orderBy := "conductor" + scalars := #[ + -- `Module.finrank ℤ W.Point` ↦ rank + finrankOver ``Int "rank" "rank", + -- `Nat.card (AddCommGroup.torsion W.Point)` ↦ torsion + cardMentions ``AddCommGroup.torsion "torsion" "torsion"] + props := #[ + -- `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)` ↦ torsion_structure = {n₁, …} + isoStructure ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false] + +/-- Finite groups. -/ +def gpsGroups : TableInfo where + table := "gps_groups" + labelCol := "label" + descSelects := #["tex_name::text AS tex_name"] + describe row := s!"group {rowStr row "label"} ({rowStr row "tex_name"})" + url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" + -- `order` is a SQL reserved word, so it must be quoted. + orderBy := "\"order\"" + props := #[ + -- `IsSimpleGroup G` ↦ simple = 't' + flagIs ``IsSimpleGroup "simple", + -- `∀ a b : G, a * b = b * a` ↦ abelian = 't' + isAbelian "abelian"] + +/-- All supported object families. To support a new one, add its `TableInfo` here. -/ +def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] + +/-- The table configuration for a table name. -/ +def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == name) + +end Lookup From 10fa7e1eedb10ba05d54ae18981b1097b6e4aa59 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:30:20 +0100 Subject: [PATCH 16/34] accept the additive class-group spelling --- LeanBridge/Lookup/Basic.lean | 5 +++-- LeanBridge/Lookup/Demo.lean | 26 -------------------------- LeanBridge/Lookup/Tables.lean | 4 +++- 3 files changed, 6 insertions(+), 29 deletions(-) diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean index 5c8521fd..93e039eb 100644 --- a/LeanBridge/Lookup/Basic.lean +++ b/LeanBridge/Lookup/Basic.lean @@ -91,12 +91,13 @@ def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := /-- Whether `e` mentions the constant `n` anywhere. -/ def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome -/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` -wrappers stripped) as its list of moduli, in the order written. -/ +/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` or +`Additive` wrappers stripped) as its list of moduli, in the order written. -/ partial def cyclicFactors? (e : Expr) : Option (Array Nat) := match_expr e with | ZMod n => (getNatLit? n).map (#[·]) | Multiplicative a => cyclicFactors? a + | Additive a => cyclicFactors? a | Prod a b => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) | _ => none diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index f67aba46..01522f33 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -1,57 +1,31 @@ import LeanBridge.Lookup.Lookup -/-! # `lookup` demo - -Each example below is a *false* statement; `lookup` finds and reports a counterexample from -LMFDB (the smallest one, with the object's defining data and a clickable link), so each -`example` is expected to error with that report. -/ - open Lookup --- Number fields. "Every number field of class number 1 and degree 2 has |discriminant| ≤ 163" --- is false (the bound is the *imaginary* quadratic class-number-1 theorem; real quadratic --- fields have unbounded discriminant). `lookup` surfaces `2.2.172.1`. example {F : Type*} [Field F] [NumberField F] (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) : |NumberField.discr F| ≤ 163 := by lookup --- Signed-discriminant queries are supported too (the DB stores `disc_sign * disc_abs`, and --- `lookup` case-splits on the sign so the query stays index-friendly): --- `NumberField.discr F ≥ -100` finds the counterexample `2.0.163.1` (discriminant -163), --- while `NumberField.discr F ≥ -163` finds none. - --- The ideal class group *structure* (LMFDB's `class_group`) is supported via `≃*`: "every --- degree-2 field of class number 4 has cyclic class group ℤ/4" is false — some are C₂ × C₂. --- The class group is multiplicative, so the right-hand side carries `Multiplicative`. example {F : Type*} [Field F] [NumberField F] (h1 : NumberField.classNumber F = 4) (h2 : Module.finrank ℚ F = 2) : Nonempty (ClassGroup (NumberField.RingOfIntegers F) ≃* Multiplicative (ZMod 4)) := by lookup --- Elliptic curves: `lookup` dispatches to `ec_curvedata`. "Every curve with a 4-torsion point --- has rank ≤ 0" is false — e.g. `117.a3` has a 4-torsion point and positive rank. example {W : WeierstrassCurve.Affine ℚ} (hW : 4 ≤ Nat.card (AddCommGroup.torsion W.Point)) : Module.finrank ℤ W.Point ≤ 0 := by lookup --- "Every elliptic curve over ℚ with rank at least 2 has trivial torsion subgroup" is false: --- e.g. `1088.a1` has rank 2 and a 2-torsion point. example {W : WeierstrassCurve.Affine ℚ} (hW : 2 ≤ Module.finrank ℤ W.Point) : Nat.card (AddCommGroup.torsion W.Point) = 1 := by lookup --- Torsion subgroup *structure* (LMFDB's `torsion_structure`): "every curve whose torsion --- subgroup has order 4 has torsion subgroup ≅ ℤ/4" is false — some are ℤ/2 × ℤ/2. The torsion --- subgroup is additive, hence `≃+`. example {W : WeierstrassCurve.Affine ℚ} (hW : Nat.card (AddCommGroup.torsion W.Point) = 4) : Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 4) := by lookup --- Groups: `lookup` dispatches boolean properties to `gps_groups`. "Every simple group is --- nonabelian" is false — the cyclic groups of prime order are simple and abelian. example {G : Type*} [Group G] [IsSimpleGroup G] : ¬ ∀ a b : G, a * b = b * a := by lookup diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean index 0861c701..d1f9319a 100644 --- a/LeanBridge/Lookup/Tables.lean +++ b/LeanBridge/Lookup/Tables.lean @@ -30,7 +30,9 @@ def nfFields : TableInfo where signedValue ``NumberField.discr "disc_sign" "disc_abs" "discriminant"] props := #[ -- `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)` ↦ class_group = [n₁, …] - isoStructure ``MulEquiv ``ClassGroup "class_group::text" "class group" true] + isoStructure ``MulEquiv ``ClassGroup "class_group::text" "class group" true, + -- additive spelling: `Additive (ClassGroup (𝓞 F)) ≃+ (∏ ZMod nᵢ)` ↦ class_group = [n₁, …] + isoStructure ``AddEquiv ``ClassGroup "class_group::text" "class group" true] /-- Elliptic curves over `ℚ`. -/ def ecCurvedata : TableInfo where From 5a94a94e6cfe169e3dab2b61db45097d97aad3a6 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:42:03 +0100 Subject: [PATCH 17/34] print the Weierstrass equation for curves --- LeanBridge/Lookup/Basic.lean | 20 ++++++++++++++++++++ LeanBridge/Lookup/Tables.lean | 2 +- 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean index 93e039eb..a7008b65 100644 --- a/LeanBridge/Lookup/Basic.lean +++ b/LeanBridge/Lookup/Basic.lean @@ -244,6 +244,26 @@ def formatPoly (coeffs : String) : String := Id.run do out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}") return if out.isEmpty then "0" else out +/-- Append `c * mono` (with its sign) to a running sum `acc`, skipping a zero coefficient. +`mono = ""` is the constant term. -/ +def addTerm (acc : String) (c : Int) (mono : String) : String := + if c == 0 then acc + else + let mag := if mono.isEmpty then toString c.natAbs + else if c.natAbs == 1 then mono else s!"{c.natAbs}*{mono}" + acc ++ (if c < 0 then " - " else " + ") ++ mag + +/-- Format an LMFDB `ainvs` array `{a₁,a₂,a₃,a₄,a₆}` as the Weierstrass equation +`y² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆`. -/ +def formatWeierstrass (ainvs : String) : String := Id.run do + let stripped := (ainvs.replace "{" "").replace "}" "" + let cs := (stripped.splitOn ",").filterMap String.toInt? + if cs.length != 5 then return ainvs + let (a1, a2, a3, a4, a6) := (cs[0]!, cs[1]!, cs[2]!, cs[3]!, cs[4]!) + let lhs := addTerm (addTerm "y^2" a1 "x*y") a3 "y" + let rhs := addTerm (addTerm (addTerm "x^3" a2 "x^2") a4 "x") a6 "" + return s!"{lhs} = {rhs}" + /-! ## LMFDB tables -/ /-- Everything needed to query one LMFDB table and recognise the Lean expressions that map into diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean index d1f9319a..09bd93d7 100644 --- a/LeanBridge/Lookup/Tables.lean +++ b/LeanBridge/Lookup/Tables.lean @@ -39,7 +39,7 @@ def ecCurvedata : TableInfo where table := "ec_curvedata" labelCol := "lmfdb_label" descSelects := #["ainvs::text AS ainvs"] - describe row := s!"elliptic curve {rowStr row "label"} with a-invariants {rowStr row "ainvs"}" + describe row := s!"elliptic curve {rowStr row "label"}: {formatWeierstrass (rowStr row "ainvs")}" -- LMFDB EC labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`. url label := match label.splitOn "." with From 972a3d6de2b9f8057f81c21ec9f5adb446d409dd Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 11:08:50 +0100 Subject: [PATCH 18/34] remove DECISIONS.md --- LeanBridge/Lookup/DECISIONS.md | 37 ---------------------------------- 1 file changed, 37 deletions(-) delete mode 100644 LeanBridge/Lookup/DECISIONS.md diff --git a/LeanBridge/Lookup/DECISIONS.md b/LeanBridge/Lookup/DECISIONS.md deleted file mode 100644 index bf7ce72a..00000000 --- a/LeanBridge/Lookup/DECISIONS.md +++ /dev/null @@ -1,37 +0,0 @@ -# `lookup` tactic — decisions where the right choice was unclear - -## Clickable LMFDB link (task 2) - -**Unclear:** Lean core `MessageData` has no dedicated hyperlink constructor, so "make the -link clickable in the infoview" is environment-dependent. The VS Code Lean infoview -auto-linkifies bare `http(s)://` URLs in messages, but does *not* linkify a URL wrapped in -parentheses or with trailing punctuation attached. - -- Option A: keep a custom widget / `MessageData.ofWidget` to render an `` tag. Heavy, - and overkill for a one-line link. -- Option B: emit the URL bare on its own line with no surrounding punctuation, relying on - the infoview's auto-linkification. - -**Update — markdown link also failed.** Neither a bare URL nor a markdown link `[text](url)` -is linkified by the infoview for a tactic message. - -**Final — ProofWidgets HTML embedded in the message.** The report is now built as a -`ProofWidgets.Html` value containing a real `` element and embedded into the -thrown error via `MessageData.ofHtml`, which renders the HTML (clickable anchor) in the -infoview and falls back to a plain-text `alt` everywhere else (e.g. the LSP diagnostic text). -This is distinct from the project's existing `LMFDBWidget` (which the user noted does not -help); it uses only the stock `HtmlDisplay` component that ships with ProofWidgets. - -## Reporting signed-discriminant counterexamples (tasks 3 & 7) - -**Unclear:** how to display the discriminant of a counterexample when the query referenced -the *signed* discriminant (`NumberField.discr F`), given the DB stores `disc_sign` and -`disc_abs` separately. - -- Option A: report the two raw columns (`disc_sign = 1, disc_abs = 41`). -- Option B: report the reconstructed signed value (`discriminant = 41`) by selecting the - SQL expression `(disc_sign * disc_abs)`. - -**Chosen: Option B.** It mirrors what the user wrote in Lean (`NumberField.discr F`) and is -less confusing than exposing the storage split. `|NumberField.discr F|` still reports as -`|discriminant|` backed by `disc_abs`. From 55111b3a0dceab7874dcb82b415ad0e87f73f442 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 11:13:03 +0100 Subject: [PATCH 19/34] restrict curve examples to elliptic curves --- LeanBridge/Lookup/Demo.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index 01522f33..a53c337c 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -12,17 +12,17 @@ example {F : Type*} [Field F] [NumberField F] Nonempty (ClassGroup (NumberField.RingOfIntegers F) ≃* Multiplicative (ZMod 4)) := by lookup -example {W : WeierstrassCurve.Affine ℚ} +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] (hW : 4 ≤ Nat.card (AddCommGroup.torsion W.Point)) : Module.finrank ℤ W.Point ≤ 0 := by lookup -example {W : WeierstrassCurve.Affine ℚ} +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] (hW : 2 ≤ Module.finrank ℤ W.Point) : Nat.card (AddCommGroup.torsion W.Point) = 1 := by lookup -example {W : WeierstrassCurve.Affine ℚ} +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] (hW : Nat.card (AddCommGroup.torsion W.Point) = 4) : Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 4) := by lookup From 037116e4d73d15fabc49b768886701651cb25fa8 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:23:30 +0000 Subject: [PATCH 20/34] add more number-field, curve, and group columns --- .gitignore | 3 +- LeanBridge/Lookup/Basic.lean | 17 ++++++++++ LeanBridge/Lookup/Tables.lean | 59 ++++++++++++++++++++++++++++++++--- 3 files changed, 73 insertions(+), 6 deletions(-) diff --git a/.gitignore b/.gitignore index 6fc71fbf..cbe189c2 100644 --- a/.gitignore +++ b/.gitignore @@ -41,4 +41,5 @@ blueprint/src/flasklog ## Pip .venv/* ## Update script -blueprint/src/cycles.txt \ No newline at end of file +blueprint/src/cycles.txt +lean_explore_key diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean index a7008b65..3796f17a 100644 --- a/LeanBridge/Lookup/Basic.lean +++ b/LeanBridge/Lookup/Basic.lean @@ -191,6 +191,23 @@ column `col` (`= 't'`, or `= 'f'` when negated). -/ def flagIs (c : Name) (column : String) : Bool → Expr → Option Cond := fun pos e => if e.isAppOf c then some (boolCol pos column) else none +/-- `flagCond c posSql negSql refs`: matches any application of `c` to the SQL condition +`posSql` (or `negSql` when negated). Use when a Lean predicate has no dedicated boolean column +but translates to a condition on existing columns (e.g. `NumberField.IsTotallyReal F` ↦ +`r2 = 0`). `refs` lists the `(displayName, selectExpr)` columns to report. -/ +def flagCond (c : Name) (posSql negSql : String) (refs : Array (String × String)) : + Bool → Expr → Option Cond := + fun pos e => if e.isAppOf c then some { sql := if pos then posSql else negSql, refs } else none + +/-- `flagCondMentions head obj posSql negSql refs`: like `flagCond`, but for a *generic* +predicate `head` (e.g. `Finite`, `IsPrincipalIdealRing`) that only identifies this table when +its argument mentions `obj`. Matches `head … obj …` (e.g. `Finite W.Point`, with `obj` the +elliptic-curve point group) to `posSql` (or `negSql` when negated). -/ +def flagCondMentions (head obj : Name) (posSql negSql : String) (refs : Array (String × String)) : + Bool → Expr → Option Cond := + fun pos e => if e.isAppOf head && containsConst e obj then + some { sql := if pos then posSql else negSql, refs } else none + /-- `isAbelian "col"`: matches the commutativity statement `∀ a b, a * b = b * a` to the boolean column `col`. -/ def isAbelian (column : String) : Bool → Expr → Option Cond := diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean index 09bd93d7..fe65b7a6 100644 --- a/LeanBridge/Lookup/Tables.lean +++ b/LeanBridge/Lookup/Tables.lean @@ -27,12 +27,36 @@ def nfFields : TableInfo where -- `|NumberField.discr F|` ↦ disc_abs absOf ``NumberField.discr "disc_abs" "|discriminant|", -- `NumberField.discr F` ↦ disc_sign · disc_abs (signed, sign-split on comparison) - signedValue ``NumberField.discr "disc_sign" "disc_abs" "discriminant"] + signedValue ``NumberField.discr "disc_sign" "disc_abs" "discriminant", + -- `NumberField.rootDiscr F` ↦ rd + headIs ``NumberField.rootDiscr "rd" "root discriminant", + -- `NumberField.Units.regulator F` ↦ regulator + headIs ``NumberField.Units.regulator "regulator" "regulator", + -- `NumberField.Units.torsionOrder F` ↦ torsion_order (number of roots of unity) + headIs ``NumberField.Units.torsionOrder "torsion_order" "number of roots of unity", + -- `NumberField.InfinitePlace.nrComplexPlaces F` ↦ r2 + headIs ``NumberField.InfinitePlace.nrComplexPlaces "r2" "number of complex places"] props := #[ -- `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)` ↦ class_group = [n₁, …] isoStructure ``MulEquiv ``ClassGroup "class_group::text" "class group" true, -- additive spelling: `Additive (ClassGroup (𝓞 F)) ≃+ (∏ ZMod nᵢ)` ↦ class_group = [n₁, …] - isoStructure ``AddEquiv ``ClassGroup "class_group::text" "class group" true] + isoStructure ``AddEquiv ``ClassGroup "class_group::text" "class group" true, + -- `NumberField.IsCMField F` ↦ cm = 't' + flagIs ``NumberField.IsCMField "cm", + -- `IsGalois ℚ F` ↦ is_galois = 't' + flagIs ``IsGalois "is_galois", + -- `IsAbelianGalois ℚ F` ↦ gal_is_abelian = 't' + flagIs ``IsAbelianGalois "gal_is_abelian", + -- `NumberField.IsTotallyReal F` ↦ no real-place column: r2 = 0 + flagCond ``NumberField.IsTotallyReal "r2 = 0" "r2 <> 0" #[("r2", "r2")], + -- `NumberField.IsTotallyComplex F` ↦ r1 = 0, i.e. degree = 2·r2 (no r1 column) + flagCond ``NumberField.IsTotallyComplex "degree = 2 * r2" "degree <> 2 * r2" + #[("degree", "degree"), ("r2", "r2")], + -- `Algebra.IsQuadraticExtension ℚ F` ↦ degree = 2 + flagCond ``Algebra.IsQuadraticExtension "degree = 2" "degree <> 2" #[("degree", "degree")], + -- `IsPrincipalIdealRing (𝓞 F)` ↦ class_number = 1 (trivial class group) + flagCondMentions ``IsPrincipalIdealRing ``NumberField.RingOfIntegers + "class_number = 1" "class_number <> 1" #[("class_number", "class_number")]] /-- Elliptic curves over `ℚ`. -/ def ecCurvedata : TableInfo where @@ -52,10 +76,18 @@ def ecCurvedata : TableInfo where -- `Module.finrank ℤ W.Point` ↦ rank finrankOver ``Int "rank" "rank", -- `Nat.card (AddCommGroup.torsion W.Point)` ↦ torsion - cardMentions ``AddCommGroup.torsion "torsion" "torsion"] + cardMentions ``AddCommGroup.torsion "torsion" "torsion", + -- `WeierstrassCurve.j W` ↦ jinv (model-independent, so exact) + headIs ``WeierstrassCurve.j "jinv" "j-invariant"] props := #[ -- `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)` ↦ torsion_structure = {n₁, …} - isoStructure ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false] + isoStructure ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false, + -- `Finite W.Point` ↦ rank = 0 (Mordell–Weil group finite ⟺ rank zero) + flagCondMentions ``Finite ``WeierstrassCurve.Affine.Point "rank = 0" "rank <> 0" + #[("rank", "rank")], + -- `IsAddTorsionFree W.Point` ↦ torsion = 1 + flagCondMentions ``IsAddTorsionFree ``WeierstrassCurve.Affine.Point "torsion = 1" "torsion <> 1" + #[("torsion", "torsion")]] /-- Finite groups. -/ def gpsGroups : TableInfo where @@ -66,11 +98,28 @@ def gpsGroups : TableInfo where url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}" -- `order` is a SQL reserved word, so it must be quoted. orderBy := "\"order\"" + scalars := #[ + -- `Monoid.exponent G` ↦ exponent + headIs ``Monoid.exponent "exponent" "exponent", + -- `Group.nilpotencyClass G` ↦ nilpotency_class + headIs ``Group.nilpotencyClass "nilpotency_class" "nilpotency class", + -- `Group.rank G` ↦ rank (minimal number of generators) + headIs ``Group.rank "rank" "rank", + -- `Nat.card (Subgroup.center G)` ↦ center_order + cardMentions ``Subgroup.center "center_order" "order of the center", + -- `Nat.card (ConjClasses G)` ↦ number_conjugacy_classes + cardMentions ``ConjClasses "number_conjugacy_classes" "number of conjugacy classes", + -- `Nat.card (MulAut G)` ↦ aut_order + cardMentions ``MulAut "aut_order" "order of the automorphism group"] props := #[ -- `IsSimpleGroup G` ↦ simple = 't' flagIs ``IsSimpleGroup "simple", -- `∀ a b : G, a * b = b * a` ↦ abelian = 't' - isAbelian "abelian"] + isAbelian "abelian", + -- `Group.IsNilpotent G` ↦ nilpotent = 't' + flagIs ``Group.IsNilpotent "nilpotent", + -- `Group.IsPerfect G` ↦ perfect = 't' + flagIs ``Group.IsPerfect "perfect"] /-- All supported object families. To support a new one, add its `TableInfo` here. -/ def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] From d9bad0c20b692e1eff45e78890cd854a0d78e21b Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:32:42 +0000 Subject: [PATCH 21/34] drop the lean_explore_key gitignore entry --- .gitignore | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index cbe189c2..6fc71fbf 100644 --- a/.gitignore +++ b/.gitignore @@ -41,5 +41,4 @@ blueprint/src/flasklog ## Pip .venv/* ## Update script -blueprint/src/cycles.txt -lean_explore_key +blueprint/src/cycles.txt \ No newline at end of file From 15ace249a05c6c2c450a1536a5c70c7ac7b8cfc4 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 11:34:28 +0100 Subject: [PATCH 22/34] handle False/True goals --- LeanBridge/Lookup/Demo.lean | 9 +++++++++ LeanBridge/Lookup/Lookup.lean | 2 ++ 2 files changed, 11 insertions(+) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index a53c337c..a8f0f28c 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -29,3 +29,12 @@ example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] example {G : Type*} [Group G] [IsSimpleGroup G] : ¬ ∀ a b : G, a * b = b * a := by lookup + +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] + (e : AddCommGroup.torsion W.Point ≃+ ZMod 2 × ZMod 8) : + False := by + lookup + +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] : + ¬ Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 2 × ZMod 10) := by + lookup diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index 994c242f..0aabc47d 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -74,6 +74,8 @@ pushing the negation down to the operator / boolean value (rather than wrapping transparent (an isomorphism *exists* iff the structures match). -/ partial def toCond (positive : Bool) (e : Expr) : Option Cond := match_expr e with + | False => some { sql := if positive then "FALSE" else "TRUE" } + | True => some { sql := if positive then "TRUE" else "FALSE" } | Not p => toCond (!positive) p | Nonempty p => toCond positive p | _ => From c8451de00b2bce7f8cae00922addc8f33fdc1b80 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 11:41:43 +0100 Subject: [PATCH 23/34] reword the user-facing messages --- LeanBridge/Lookup/Lookup.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index 0aabc47d..ec1d8587 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -128,7 +128,7 @@ actual `` element and embed it via `MessageData.ofHtml`. -/ def reportHtml (info : TableInfo) (row : Json) (items : Array (String × String)) : Html := let label := rowStr row "label" Html.element "div" #[] #[ - .text "lookup: the statement is FALSE — LMFDB has a counterexample.", + .text "the statement is false, LMFDB has a counterexample.", .element "br" #[] #[], .text (info.describe row), .element "br" #[] #[], @@ -139,7 +139,7 @@ def reportHtml (info : TableInfo) (row : Json) (items : Array (String × String) /-- A plain-text fallback for the counterexample, shown where HTML cannot render. -/ def reportAlt (info : TableInfo) (row : Json) (items : Array (String × String)) : String := - s!"lookup: the statement is FALSE — LMFDB has a counterexample.\n\ + s!"the statement is false, LMFDB has a counterexample.\n\ {info.describe row}\n\ {", ".intercalate (valueStrs row items).toList}\n\ {info.url (rowStr row "label")}" @@ -158,7 +158,7 @@ def collectHypotheses : TacticM (Array Cond) := do | some s => out := out.push s | none => if (matchCmp ty).isSome then - logWarning m!"lookup: ignoring hypothesis `{ldecl.userName}` : {ty}\n\ + logWarning m!"ignoring hypothesis `{ldecl.userName}` : {ty}\n\ (couldn't translate it to a SQL condition, so the search ignores this constraint)." return out @@ -167,15 +167,15 @@ elab "lookup" : tactic => do goal.withContext do -- The negated goal is the final condition: we hunt for a row that breaks the goal. let some goalCond := toSqlCondNeg (← instantiateMVars (← goal.getType)) - | throwError "lookup: don't know how to translate the goal into a SQL query" + | throwError "don't know how to translate the goal into a SQL query" let conditions := (← collectHypotheses).push goalCond -- Every condition must point at the same LMFDB table. let info ← match (conditions.filterMap (·.table)).toList.dedup with | [t] => match tableInfo? t with | some info => pure info - | none => throwError "lookup: no table configuration for `{t}`" - | [] => throwError "lookup: couldn't determine which LMFDB table the goal is about" - | ts => throwError "lookup: the goal mixes multiple LMFDB object types {ts}" + | none => throwError "no table configuration for `{t}`" + | [] => throwError "couldn't determine which LMFDB table the goal is about" + | ts => throwError "the goal mixes multiple LMFDB object types {ts}" let conds := conditions.map (·.sql) let items := dedupRefs (conditions.foldl (fun acc s => acc ++ s.refs) #[]) let query := buildQuery info conds items @@ -183,7 +183,7 @@ elab "lookup" : tactic => do match firstRow? (← runSql query) with | none => -- No counterexample in the database: report, but do *not* close the goal. - logInfo m!"lookup: no counterexample found in LMFDB \ + logInfo m!"no counterexample found in LMFDB \ (the statement is consistent with the database, but this is not a proof)." | some row => throwError (← MessageData.ofHtml (reportHtml info row items) (reportAlt info row items)) From 91d6f0148405db9547fb3ecbf615c48889dc3208 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:50:37 +0000 Subject: [PATCH 24/34] recognise cyclic and solvable groups --- LeanBridge/Lookup/Tables.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean index fe65b7a6..0acf6a89 100644 --- a/LeanBridge/Lookup/Tables.lean +++ b/LeanBridge/Lookup/Tables.lean @@ -119,7 +119,11 @@ def gpsGroups : TableInfo where -- `Group.IsNilpotent G` ↦ nilpotent = 't' flagIs ``Group.IsNilpotent "nilpotent", -- `Group.IsPerfect G` ↦ perfect = 't' - flagIs ``Group.IsPerfect "perfect"] + flagIs ``Group.IsPerfect "perfect", + -- `IsCyclic G` ↦ cyclic = 't' (generic head, but no other table recognises `IsCyclic`) + flagIs ``IsCyclic "cyclic", + -- `IsSolvable G` ↦ solvable = 't' + flagIs ``IsSolvable "solvable"] /-- All supported object families. To support a new one, add its `TableInfo` here. -/ def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] From b6f8105b0e1fa422aebc3bd6c72654ba0af96017 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 10:51:19 +0000 Subject: [PATCH 25/34] recognise group order and abelian groups --- LeanBridge/Lookup/Basic.lean | 10 ++++++++++ LeanBridge/Lookup/Tables.lean | 8 +++++++- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean index 3796f17a..f5dc538c 100644 --- a/LeanBridge/Lookup/Basic.lean +++ b/LeanBridge/Lookup/Basic.lean @@ -186,6 +186,16 @@ def signedValue (c : Name) (signCol absCol display : String) : Expr → Option C fun e => if e.isAppOf c then some (col s!"({signCol} * {absCol})" display (some (signCol, absCol))) else none +/-- `cardIs "col" "name"`: matches a cardinality `Nat.card G` or `Fintype.card G` to the column +`col`. The cardinality is read generically (it doesn't matter whether `G` is a group, or whether +it is written multiplicatively or additively); it is the *object* — fixed by a group instance +hypothesis or another property — that determines this is e.g. a group's order. -/ +def cardIs (sql display : String) : Expr → Option Column := + fun e => match_expr e with + | Nat.card _ => some (col sql display) + | Fintype.card _ _ => some (col sql display) + | _ => none + /-- `flagIs c "col"`: matches any application of `c` (e.g. `IsSimpleGroup G`) to the boolean column `col` (`= 't'`, or `= 'f'` when negated). -/ def flagIs (c : Name) (column : String) : Bool → Expr → Option Cond := diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean index 0acf6a89..bccfc95b 100644 --- a/LeanBridge/Lookup/Tables.lean +++ b/LeanBridge/Lookup/Tables.lean @@ -110,12 +110,18 @@ def gpsGroups : TableInfo where -- `Nat.card (ConjClasses G)` ↦ number_conjugacy_classes cardMentions ``ConjClasses "number_conjugacy_classes" "number of conjugacy classes", -- `Nat.card (MulAut G)` ↦ aut_order - cardMentions ``MulAut "aut_order" "order of the automorphism group"] + cardMentions ``MulAut "aut_order" "order of the automorphism group", + -- `Nat.card G` / `Fintype.card G` ↦ order (generic cardinality; last, so the + -- `cardMentions` recognisers above claim the cardinalities of named subobjects first) + cardIs "\"order\"" "order"] props := #[ -- `IsSimpleGroup G` ↦ simple = 't' flagIs ``IsSimpleGroup "simple", -- `∀ a b : G, a * b = b * a` ↦ abelian = 't' isAbelian "abelian", + -- a `CommGroup G` / `AddCommGroup G` hypothesis ↦ abelian = 't' + flagIs ``CommGroup "abelian", + flagIs ``AddCommGroup "abelian", -- `Group.IsNilpotent G` ↦ nilpotent = 't' flagIs ``Group.IsNilpotent "nilpotent", -- `Group.IsPerfect G` ↦ perfect = 't' From d7b3b8e4d6813a2fe23dd5ebc3c77f8647c32e3e Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 13:22:19 +0100 Subject: [PATCH 26/34] restate the last demo as a False goal --- LeanBridge/Lookup/Demo.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index a8f0f28c..8386b550 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -35,6 +35,7 @@ example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] False := by lookup -example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] : - ¬ Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 2 × ZMod 10) := by +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] + (e : AddCommGroup.torsion W.Point ≃+ ZMod 2 × ZMod 10) : + False := by lookup From 74adf7bc65b70e1bd5568777a60b9fb5ff715506 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 13:49:58 +0100 Subject: [PATCH 27/34] =?UTF-8?q?handle=20implication=20and=20=E2=88=A7/?= =?UTF-8?q?=E2=88=A8=20goals?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanBridge/Lookup/Demo.lean | 5 +++-- LeanBridge/Lookup/Lookup.lean | 35 +++++++++++++++++++++++++++++------ 2 files changed, 32 insertions(+), 8 deletions(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index 8386b550..cb1fbae4 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -8,8 +8,9 @@ example {F : Type*} [Field F] [NumberField F] lookup example {F : Type*} [Field F] [NumberField F] - (h1 : NumberField.classNumber F = 4) (h2 : Module.finrank ℚ F = 2) : - Nonempty (ClassGroup (NumberField.RingOfIntegers F) ≃* Multiplicative (ZMod 4)) := by + (h2 : Module.finrank ℚ F = 2) : + NumberField.classNumber F = 4 → + ClassGroup (NumberField.RingOfIntegers F) ≃* Multiplicative (ZMod 4) := by lookup example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index ec1d8587..dc6970f3 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -68,16 +68,22 @@ def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Cond := | none, some (cb, tb) => (getIntLit? a).map (colVsLit cb tb cmp.reverse) | none, none => none +/-- Combine two conditions with a SQL connective, merging their refs and table. -/ +def combineCond (op : String) (a b : Cond) : Cond := + { sql := s!"(({a.sql}) {op} ({b.sql}))", refs := a.refs ++ b.refs, table := a.table <|> b.table } + /-- Translate a `Prop` into a SQL condition. `positive := false` translates its negation; -pushing the negation down to the operator / boolean value (rather than wrapping in SQL -`NOT (...)`) keeps the query index-friendly. `Not` flips the polarity; `Nonempty` is -transparent (an isomorphism *exists* iff the structures match). -/ +pushing the negation down to the operator / boolean value / connective (rather than wrapping in +SQL `NOT (...)`) keeps the query index-friendly. `Not` flips the polarity, `Nonempty` is +transparent, and `∧`/`∨` are pushed through by De Morgan. -/ partial def toCond (positive : Bool) (e : Expr) : Option Cond := match_expr e with | False => some { sql := if positive then "FALSE" else "TRUE" } | True => some { sql := if positive then "TRUE" else "FALSE" } | Not p => toCond (!positive) p | Nonempty p => toCond positive p + | And a b => return combineCond (if positive then "AND" else "OR") (← toCond positive a) (← toCond positive b) + | Or a b => return combineCond (if positive then "OR" else "AND") (← toCond positive a) (← toCond positive b) | _ => match matchCmp e with | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b @@ -162,13 +168,30 @@ def collectHypotheses : TacticM (Array Cond) := do (couldn't translate it to a SQL condition, so the search ignores this constraint)." return out +/-- Peel leading non-dependent implications `a₁ → ⋯ → b` into the antecedents `#[a₁, …]` +(treated as extra hypotheses) and the final consequent `b`. -/ +partial def peelImplications : Expr → Array Expr × Expr + | e@(.forallE _ a b _) => + if b.hasLooseBVars then (#[], e) + else let (hyps, goal) := peelImplications b; (#[a] ++ hyps, goal) + | e => (#[], e) + elab "lookup" : tactic => do let goal ← getMainGoal goal.withContext do - -- The negated goal is the final condition: we hunt for a row that breaks the goal. - let some goalCond := toSqlCondNeg (← instantiateMVars (← goal.getType)) + -- Treat the antecedents of an implication goal as extra hypotheses; the negated final + -- consequent is the condition we hunt for a row to satisfy. + let (antecedents, goalType) := peelImplications (← instantiateMVars (← goal.getType)) + let some goalCond := toSqlCondNeg goalType | throwError "don't know how to translate the goal into a SQL query" - let conditions := (← collectHypotheses).push goalCond + let mut conditions ← collectHypotheses + for a in antecedents do + match toSqlCond a with + | some c => conditions := conditions.push c + | none => + if (matchCmp a).isSome then + logWarning m!"ignoring antecedent `{a}` (couldn't translate it to a SQL condition)." + conditions := conditions.push goalCond -- Every condition must point at the same LMFDB table. let info ← match (conditions.filterMap (·.table)).toList.dedup with | [t] => match tableInfo? t with From 9ca321f8b1d77198f63830101d83cb146c9daf14 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 15:22:05 +0000 Subject: [PATCH 28/34] add modular forms (mf_newspaces) --- LeanBridge/Lookup/Basic.lean | 47 ++++++++++++++++++++++++++++++++++- LeanBridge/Lookup/Lookup.lean | 15 ++++++----- LeanBridge/Lookup/Tables.lean | 22 +++++++++++++++- 3 files changed, 74 insertions(+), 10 deletions(-) diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean index f5dc538c..2df9a6dc 100644 --- a/LeanBridge/Lookup/Basic.lean +++ b/LeanBridge/Lookup/Basic.lean @@ -54,11 +54,21 @@ end Cmp /-- A scalar quantity of an object: an SQL column expression and a human-readable name. A quantity stored split as `sign * |·|` records those two columns in `signed?`, so comparisons -against a literal can be made index-friendly. -/ +against a literal can be made index-friendly. `extraConds` are extra `WHERE` conjuncts the +quantity implies — used when the object's identity is bundled into the quantity's expression +rather than supplied by separate hypotheses (e.g. a modular space's level/weight/character read +off the type inside `Module.finrank ℂ (CuspForm Γ₀(N) k)`). -/ structure Column where sql : String display : String signed? : Option (String × String) := none + extraConds : Array String := #[] + +/-- Prefix `core` with the column's extra `WHERE` conjuncts (the object identity it implies), +if any. -/ +def Column.withConds (c : Column) (core : String) : String := + if c.extraConds.isEmpty then core + else s!"{String.intercalate " AND " c.extraConds.toList} AND {core}" /-- A translated SQL condition: the boolean SQL, the columns it references (as `(displayName, selectExpr)` pairs, for reporting), and the LMFDB table it forces. -/ @@ -196,6 +206,41 @@ def cardIs (sql display : String) : Expr → Option Column := | Fintype.card _ _ => some (col sql display) | _ => none +/-- From a modular/cusp form *type* `CuspForm Γ k` / `ModularForm Γ k` with `Γ` containing a +`CongruenceSubgroup.Gamma0 N` subterm, read `(isCuspidal, level N, weight k)`. -/ +def modularSpace? (M : Expr) : Option (Bool × Nat × Int) := do + let (isCusp, Γ, k) ← (match_expr M with + | CuspForm Γ k => some (true, Γ, k) + | ModularForm Γ k => some (false, Γ, k) + | _ => none) + let kLit ← getIntLit? k + let g ← Γ.find? (·.isAppOf ``CongruenceSubgroup.Gamma0) + let N ← getNatLit? g.appArg! + return (isCusp, N, kLit) + +/-- The `WHERE` conjuncts identifying the `mf_newspaces` row for `S_k(Γ₀(N))`: its level, weight +and the trivial character (`char_orbit_index = 1`, i.e. the `Γ₀(N)` nebentypus). -/ +def mfSpaceConds (N : Nat) (k : Int) : Array String := + #[s!"level = {N}", s!"weight = {k}", "char_orbit_index = 1"] + +/-- Recognise `Module.finrank ℂ (CuspForm Γ₀(N) k)` / `(ModularForm Γ₀(N) k)`, mapping to the +cuspidal/total dimension column of `mf_newspaces` with the level/weight/character pinned. -/ +def modularDim : Expr → Option Column := fun e => + match_expr e with + | Module.finrank _ M _ _ _ => do + let (isCusp, N, k) ← modularSpace? M + pure { sql := if isCusp then "cusp_dim" else "mf_dim", display := "dimension", + extraConds := mfSpaceConds N k } + | _ => none + +/-- Recognise a modular/cusp form *type* `CuspForm Γ₀(N) k` / `ModularForm Γ₀(N) k` (e.g. a +hypothesis `f : CuspForm Γ₀(N) k`), pinning the space's level, weight and trivial character. The +polarity is ignored — the type names the object, it is not a refutable property. -/ +def modularSpace : Bool → Expr → Option Cond := fun _ e => do + let (_, N, k) ← modularSpace? e + some { sql := String.intercalate " AND " (mfSpaceConds N k).toList, + refs := #[("level", "level"), ("weight", "weight")] } + /-- `flagIs c "col"`: matches any application of `c` (e.g. `IsSimpleGroup G`) to the boolean column `col` (`= 't'`, or `= 'f'` when negated). -/ def flagIs (c : Name) (column : String) : Bool → Expr → Option Cond := diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index dc6970f3..00ff9732 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -50,19 +50,18 @@ def findScalar (e : Expr) : Option (Column × String) := case-split on the sign, so the comparison hits the indexed absolute-value column rather than the non-indexable product. -/ def colVsLit (c : Column) (table : String) (cmp : Cmp) (k : Int) : Cond := - match c.signed? with - | some (signCol, absCol) => - { sql := s!"(({signCol} = 1 AND {absCol} {cmp.toSql} {k}) OR \ - ({signCol} = -1 AND {absCol} {cmp.reverse.toSql} {-k}))", - refs := #[(c.display, c.sql)], table := some table } - | none => - { sql := s!"{c.sql} {cmp.toSql} {k}", refs := #[(c.display, c.sql)], table := some table } + let core := match c.signed? with + | some (signCol, absCol) => + s!"(({signCol} = 1 AND {absCol} {cmp.toSql} {k}) OR \ + ({signCol} = -1 AND {absCol} {cmp.reverse.toSql} {-k}))" + | none => s!"{c.sql} {cmp.toSql} {k}" + { sql := c.withConds core, refs := #[(c.display, c.sql)], table := some table } /-- Translate a comparison `cmp a b` (column vs literal, or column vs column) into a `Cond`. -/ def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Cond := match findScalar a, findScalar b with | some (ca, ta), some (cb, _) => - some { sql := s!"{ca.sql} {cmp.toSql} {cb.sql}", + some { sql := ca.withConds (cb.withConds s!"{ca.sql} {cmp.toSql} {cb.sql}"), refs := #[(ca.display, ca.sql), (cb.display, cb.sql)], table := some ta } | some (ca, ta), none => (getIntLit? b).map (colVsLit ca ta cmp) | none, some (cb, tb) => (getIntLit? a).map (colVsLit cb tb cmp.reverse) diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean index bccfc95b..2ccfa2b3 100644 --- a/LeanBridge/Lookup/Tables.lean +++ b/LeanBridge/Lookup/Tables.lean @@ -131,8 +131,28 @@ def gpsGroups : TableInfo where -- `IsSolvable G` ↦ solvable = 't' flagIs ``IsSolvable "solvable"] +/-- Spaces of classical modular forms `S_k(Γ₀(N))` / `M_k(Γ₀(N))`. The object is identified by +its level and weight, read off the type `CuspForm Γ k` / `ModularForm Γ k` (with `Γ = Γ₀(N)`) +inside a `Module.finrank ℂ …` — see `modularDim`. -/ +def mfNewspaces : TableInfo where + table := "mf_newspaces" + labelCol := "label" + descSelects := #["level::text AS level", "weight::text AS weight", + "cusp_dim::text AS cusp_dim", "mf_dim::text AS mf_dim"] + describe row := s!"space of level {rowStr row "level"}, weight {rowStr row "weight"} \ + (cuspidal dimension {rowStr row "cusp_dim"}, total dimension {rowStr row "mf_dim"})" + -- LMFDB newspace labels `23.2.a` live at `.../holomorphic/23/2/a`. + url label := s!"https://www.lmfdb.org/ModularForm/GL2/Q/holomorphic/{label.replace "." "/"}" + orderBy := "level" + scalars := #[ + -- `Module.finrank ℂ (CuspForm Γ₀(N) k)` ↦ cusp_dim, `(ModularForm …)` ↦ mf_dim + modularDim] + props := #[ + -- a `CuspForm Γ₀(N) k` / `ModularForm Γ₀(N) k` type ↦ level = N AND weight = k AND trivial char + modularSpace] + /-- All supported object families. To support a new one, add its `TableInfo` here. -/ -def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups] +def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups, mfNewspaces] /-- The table configuration for a table name. -/ def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == name) From d59fe182215ec93f11006740346934d021ac95e1 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 15:46:08 +0000 Subject: [PATCH 29/34] recognise num_ram for number fields --- LeanBridge/Lookup/Tables.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean index 2ccfa2b3..a05da528 100644 --- a/LeanBridge/Lookup/Tables.lean +++ b/LeanBridge/Lookup/Tables.lean @@ -35,7 +35,15 @@ def nfFields : TableInfo where -- `NumberField.Units.torsionOrder F` ↦ torsion_order (number of roots of unity) headIs ``NumberField.Units.torsionOrder "torsion_order" "number of roots of unity", -- `NumberField.InfinitePlace.nrComplexPlaces F` ↦ r2 - headIs ``NumberField.InfinitePlace.nrComplexPlaces "r2" "number of complex places"] + headIs ``NumberField.InfinitePlace.nrComplexPlaces "r2" "number of complex places", + -- `Nat.card {p // ¬ Algebra.IsUnramifiedAt ℤ p}` ↦ num_ram: the prime ideals at which + -- `F` is not unramified, i.e. the ramified primes. + (fun e => match_expr e with + | Nat.card t => + if containsConst t ``Algebra.IsUnramifiedAt && containsConst t ``Not then + some (col "num_ram" "number of ramified primes") + else none + | _ => none)] props := #[ -- `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)` ↦ class_group = [n₁, …] isoStructure ``MulEquiv ``ClassGroup "class_group::text" "class group" true, From 45e3705c346f4841623b251cba15e928b0fefbc5 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 30 Jun 2026 21:30:43 +0000 Subject: [PATCH 30/34] demo modular-form and num_ram lookups --- LeanBridge/Lookup/Demo.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index cb1fbae4..312e6f7c 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -40,3 +40,15 @@ example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] (e : AddCommGroup.torsion W.Point ≃+ ZMod 2 × ZMod 10) : False := by lookup + +-- modular forms: `M₂(Γ₀(11))` is nonzero (the newspace `11.2.a`), so its dimension is not `≤ 0` +example : Module.finrank ℂ + (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) + (CongruenceSubgroup.Gamma0 11)) 2) ≤ 0 := by + lookup + +-- no quadratic field is unramified at every prime: some prime ramifies +example {F : Type*} [Field F] [NumberField F] (h : Module.finrank ℚ F = 2) : + Nat.card {p : PrimeSpectrum (NumberField.RingOfIntegers F) // + ¬ Algebra.IsUnramifiedAt ℤ p.asIdeal} = 0 := by + lookup From 332cdbd1da75b20a45fb4706109796d9de77cfc3 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 1 Jul 2026 00:44:52 +0100 Subject: [PATCH 31/34] line wrap --- LeanBridge/Lookup/Lookup.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index 00ff9732..82390511 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -75,19 +75,19 @@ def combineCond (op : String) (a b : Cond) : Cond := pushing the negation down to the operator / boolean value / connective (rather than wrapping in SQL `NOT (...)`) keeps the query index-friendly. `Not` flips the polarity, `Nonempty` is transparent, and `∧`/`∨` are pushed through by De Morgan. -/ -partial def toCond (positive : Bool) (e : Expr) : Option Cond := +partial def toCond (pos : Bool) (e : Expr) : Option Cond := match_expr e with - | False => some { sql := if positive then "FALSE" else "TRUE" } - | True => some { sql := if positive then "TRUE" else "FALSE" } - | Not p => toCond (!positive) p - | Nonempty p => toCond positive p - | And a b => return combineCond (if positive then "AND" else "OR") (← toCond positive a) (← toCond positive b) - | Or a b => return combineCond (if positive then "OR" else "AND") (← toCond positive a) (← toCond positive b) + | False => some { sql := if pos then "FALSE" else "TRUE" } + | True => some { sql := if pos then "TRUE" else "FALSE" } + | Not p => toCond (!pos) p + | Nonempty p => toCond pos p + | And a b => return combineCond (if pos then "AND" else "OR") (← toCond pos a) (← toCond pos b) + | Or a b => return combineCond (if pos then "OR" else "AND") (← toCond pos a) (← toCond pos b) | _ => match matchCmp e with - | some (cmp, a, b) => toSqlCondCmp (if positive then cmp else cmp.negate) a b + | some (cmp, a, b) => toSqlCondCmp (if pos then cmp else cmp.negate) a b | none => tables.findSome? fun t => - (t.props.findSome? (· positive e)).map fun c => { c with table := some t.table } + (t.props.findSome? (· pos e)).map fun c => { c with table := some t.table } /-- Translate a `Prop` into a SQL condition. -/ def toSqlCond (e : Expr) : Option Cond := toCond true e From 2f29d3f61806c838ebe22969377e8334b066c2c6 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 1 Jul 2026 01:36:00 +0100 Subject: [PATCH 32/34] treat ZMod 1 and Unit as trivial groups --- LeanBridge/Lookup/Basic.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean index 2df9a6dc..19f3914e 100644 --- a/LeanBridge/Lookup/Basic.lean +++ b/LeanBridge/Lookup/Basic.lean @@ -102,10 +102,14 @@ def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome /-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` or -`Additive` wrappers stripped) as its list of moduli, in the order written. -/ +`Additive` wrappers stripped) as its list of moduli, in the order written. The trivial group — +`ZMod 1`, `Unit`/`PUnit`, or any `ZMod 1` factor — contributes nothing, matching LMFDB's +convention of dropping trivial invariant factors (so the trivial group is the empty array). -/ partial def cyclicFactors? (e : Expr) : Option (Array Nat) := match_expr e with - | ZMod n => (getNatLit? n).map (#[·]) + | ZMod n => (getNatLit? n).map fun k => if k == 1 then #[] else #[k] + | Unit => some #[] + | PUnit => some #[] | Multiplicative a => cyclicFactors? a | Additive a => cyclicFactors? a | Prod a b => do return (← cyclicFactors? a) ++ (← cyclicFactors? b) From 1054aba374f547923e0e0541166137de3a939b55 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 1 Jul 2026 01:38:27 +0100 Subject: [PATCH 33/34] demo trivial-torsion counterexamples --- LeanBridge/Lookup/Demo.lean | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean index 312e6f7c..f89510d0 100644 --- a/LeanBridge/Lookup/Demo.lean +++ b/LeanBridge/Lookup/Demo.lean @@ -3,7 +3,7 @@ import LeanBridge.Lookup.Lookup open Lookup example {F : Type*} [Field F] [NumberField F] - (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) : + (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) (h3 : 2 = 2) : |NumberField.discr F| ≤ 163 := by lookup @@ -52,3 +52,23 @@ example {F : Type*} [Field F] [NumberField F] (h : Module.finrank ℚ F = 2) : Nat.card {p : PrimeSpectrum (NumberField.RingOfIntegers F) // ¬ Algebra.IsUnramifiedAt ℤ p.asIdeal} = 0 := by lookup + +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] + (hW : 2 ≤ Module.finrank ℤ W.Point) : + Nat.card (AddCommGroup.torsion W.Point) ≠ 1 := by + lookup + +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] + (hW : 2 ≤ Module.finrank ℤ W.Point) : + ¬ Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 1) := by + lookup + +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] + (hW : 2 ≤ Module.finrank ℤ W.Point) : + AddCommGroup.torsion W.Point ≃+ ZMod 1 := by + lookup + +example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic] + (hW : 2 ≤ Module.finrank ℤ W.Point) : + AddCommGroup.torsion W.Point ≃+ Unit := by + lookup From 28b280ecf45cc182af3d9f8f5f193816c9d9af12 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Thu, 2 Jul 2026 12:41:08 +0000 Subject: [PATCH 34/34] tighten docstrings --- LeanBridge/Lookup/Basic.lean | 72 ++++++++++++++++------------------- LeanBridge/Lookup/Lookup.lean | 38 +++++++++--------- LeanBridge/Lookup/Tables.lean | 14 +++---- 3 files changed, 58 insertions(+), 66 deletions(-) diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean index 19f3914e..f3927bc0 100644 --- a/LeanBridge/Lookup/Basic.lean +++ b/LeanBridge/Lookup/Basic.lean @@ -2,9 +2,9 @@ import Mathlib /-! # `lookup` vocabulary -The table-agnostic building blocks shared by the rest of the tactic: the value types -(`Column`, `Cond`, `Cmp`), low-level `Expr` matchers, the recogniser combinators used to -describe a table's columns/properties, small result-row utilities, and the `TableInfo` record. +The shared, table-agnostic pieces: the value types (`Column`, `Cond`, `Cmp`), low-level `Expr` +matchers, the recogniser combinators for a table's columns and properties, result-row helpers, +and `TableInfo`. The concrete tables live in `LeanBridge.Lookup.Tables`; the tactic itself in `LeanBridge.Lookup.Lookup`. -/ @@ -52,12 +52,9 @@ end Cmp /-! ## Columns and conditions -/ -/-- A scalar quantity of an object: an SQL column expression and a human-readable name. A -quantity stored split as `sign * |·|` records those two columns in `signed?`, so comparisons -against a literal can be made index-friendly. `extraConds` are extra `WHERE` conjuncts the -quantity implies — used when the object's identity is bundled into the quantity's expression -rather than supplied by separate hypotheses (e.g. a modular space's level/weight/character read -off the type inside `Module.finrank ℂ (CuspForm Γ₀(N) k)`). -/ +/-- A scalar quantity: an SQL expression and a display name. `signed?` names the `(sign, abs)` +columns for a value LMFDB stores as `sign * |·|`. `extraConds` are extra `WHERE` conjuncts the +quantity implies, e.g. a modular space's level and weight from its `Module.finrank ℂ` type. -/ structure Column where sql : String display : String @@ -101,10 +98,9 @@ def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) := /-- Whether `e` mentions the constant `n` anywhere. -/ def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome -/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (with any `Multiplicative` or -`Additive` wrappers stripped) as its list of moduli, in the order written. The trivial group — -`ZMod 1`, `Unit`/`PUnit`, or any `ZMod 1` factor — contributes nothing, matching LMFDB's -convention of dropping trivial invariant factors (so the trivial group is the empty array). -/ +/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (after stripping any +`Multiplicative`/`Additive` wrapper) as its list of moduli, in order. A trivial factor (`ZMod 1`, +`Unit`, `PUnit`) drops out, as LMFDB does, so the trivial group is `#[]`. -/ partial def cyclicFactors? (e : Expr) : Option (Array Nat) := match_expr e with | ZMod n => (getNatLit? n).map fun k => if k == 1 then #[] else #[k] @@ -125,8 +121,8 @@ def bvarIdx? : Expr → Option Nat | .bvar n => some n | _ => none -/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` ("the group is abelian"), -allowing the two multiplications to have swapped operands. -/ +/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` (an abelian group), up to +swapping the operands of the two products. -/ def isAbelianPattern (e : Expr) : Bool := match e with | .forallE _ _ (.forallE _ _ body _) _ => @@ -193,17 +189,16 @@ def absOf (c : Name) (sql display : String) : Expr → Option Column := | abs _ _ _ x => if x.isAppOf c then some (col sql display) else none | _ => none -/-- `signedValue c "signCol" "absCol" "name"`: matches an application of `c` whose value LMFDB -stores split as `signCol * absCol` (e.g. the signed discriminant). Recording the two columns -lets comparisons against a literal case-split on the sign and stay index-friendly. -/ +/-- `signedValue c "signCol" "absCol" "name"`: matches `c …` whose LMFDB value is split as +`signCol * absCol` (e.g. the signed discriminant). A comparison then case-splits on the sign to +stay index-friendly. -/ def signedValue (c : Name) (signCol absCol display : String) : Expr → Option Column := fun e => if e.isAppOf c then some (col s!"({signCol} * {absCol})" display (some (signCol, absCol))) else none -/-- `cardIs "col" "name"`: matches a cardinality `Nat.card G` or `Fintype.card G` to the column -`col`. The cardinality is read generically (it doesn't matter whether `G` is a group, or whether -it is written multiplicatively or additively); it is the *object* — fixed by a group instance -hypothesis or another property — that determines this is e.g. a group's order. -/ +/-- `cardIs "col" "name"`: matches `Nat.card G` or `Fintype.card G` to `col`. It ignores what `G` +is, so it covers additive groups too; a group instance or another property marks this as a +group's order. -/ def cardIs (sql display : String) : Expr → Option Column := fun e => match_expr e with | Nat.card _ => some (col sql display) @@ -222,13 +217,13 @@ def modularSpace? (M : Expr) : Option (Bool × Nat × Int) := do let N ← getNatLit? g.appArg! return (isCusp, N, kLit) -/-- The `WHERE` conjuncts identifying the `mf_newspaces` row for `S_k(Γ₀(N))`: its level, weight -and the trivial character (`char_orbit_index = 1`, i.e. the `Γ₀(N)` nebentypus). -/ +/-- The `WHERE` conjuncts for the `mf_newspaces` row of `S_k(Γ₀(N))`: level, weight, and trivial +character (`char_orbit_index = 1`, the `Γ₀(N)` nebentypus). -/ def mfSpaceConds (N : Nat) (k : Int) : Array String := #[s!"level = {N}", s!"weight = {k}", "char_orbit_index = 1"] -/-- Recognise `Module.finrank ℂ (CuspForm Γ₀(N) k)` / `(ModularForm Γ₀(N) k)`, mapping to the -cuspidal/total dimension column of `mf_newspaces` with the level/weight/character pinned. -/ +/-- Match `Module.finrank ℂ (CuspForm Γ₀(N) k)` / `(ModularForm Γ₀(N) k)` to the cuspidal or +total dimension column of `mf_newspaces`, with level, weight and character pinned. -/ def modularDim : Expr → Option Column := fun e => match_expr e with | Module.finrank _ M _ _ _ => do @@ -237,9 +232,9 @@ def modularDim : Expr → Option Column := fun e => extraConds := mfSpaceConds N k } | _ => none -/-- Recognise a modular/cusp form *type* `CuspForm Γ₀(N) k` / `ModularForm Γ₀(N) k` (e.g. a -hypothesis `f : CuspForm Γ₀(N) k`), pinning the space's level, weight and trivial character. The -polarity is ignored — the type names the object, it is not a refutable property. -/ +/-- Match a form *type* `CuspForm Γ₀(N) k` / `ModularForm Γ₀(N) k` (e.g. a hypothesis +`f : CuspForm Γ₀(N) k`) and pin the space's level, weight and character. Polarity is ignored: a +type names the object rather than a refutable property. -/ def modularSpace : Bool → Expr → Option Cond := fun _ e => do let (_, N, k) ← modularSpace? e some { sql := String.intercalate " AND " (mfSpaceConds N k).toList, @@ -250,18 +245,16 @@ column `col` (`= 't'`, or `= 'f'` when negated). -/ def flagIs (c : Name) (column : String) : Bool → Expr → Option Cond := fun pos e => if e.isAppOf c then some (boolCol pos column) else none -/-- `flagCond c posSql negSql refs`: matches any application of `c` to the SQL condition -`posSql` (or `negSql` when negated). Use when a Lean predicate has no dedicated boolean column -but translates to a condition on existing columns (e.g. `NumberField.IsTotallyReal F` ↦ -`r2 = 0`). `refs` lists the `(displayName, selectExpr)` columns to report. -/ +/-- `flagCond c posSql negSql refs`: matches `c …` to `posSql` (or `negSql` when negated). Use it +when a predicate has no boolean column but maps to a condition on existing columns (e.g. +`NumberField.IsTotallyReal F` ↦ `r2 = 0`). `refs` lists the columns to report. -/ def flagCond (c : Name) (posSql negSql : String) (refs : Array (String × String)) : Bool → Expr → Option Cond := fun pos e => if e.isAppOf c then some { sql := if pos then posSql else negSql, refs } else none -/-- `flagCondMentions head obj posSql negSql refs`: like `flagCond`, but for a *generic* -predicate `head` (e.g. `Finite`, `IsPrincipalIdealRing`) that only identifies this table when -its argument mentions `obj`. Matches `head … obj …` (e.g. `Finite W.Point`, with `obj` the -elliptic-curve point group) to `posSql` (or `negSql` when negated). -/ +/-- Like `flagCond`, but for a *generic* `head` (e.g. `Finite`, `IsPrincipalIdealRing`) that only +picks this table when its argument mentions `obj`. Matches `head … obj …` (e.g. `Finite W.Point`, +`obj` the point group) to `posSql`/`negSql`. -/ def flagCondMentions (head obj : Name) (posSql negSql : String) (refs : Array (String × String)) : Bool → Expr → Option Cond := fun pos e => if e.isAppOf head && containsConst e obj then @@ -273,9 +266,8 @@ def isAbelian (column : String) : Bool → Expr → Option Cond := fun pos e => if isAbelianPattern e then some (boolCol pos column) else none /-- `isoStructure equiv c "col" "name" bracketed`: matches an isomorphism `lhs ≃ (∏ ZMod nᵢ)` -written with `equiv` (``AddEquiv`` or ``MulEquiv``) and `lhs` mentioning `c`, comparing the -invariant factors against `col`. `bracketed` selects the JSON `[…]` encoding (ideal class -group) over the array `{…}` encoding (torsion structure). -/ +via `equiv` (``AddEquiv``/``MulEquiv``) with `lhs` mentioning `c`, and compares the invariant +factors against `col`. `bracketed` picks the JSON `[…]` form (class group) over `{…}` (torsion). -/ def isoStructure (equiv c : Name) (column display : String) (bracketed : Bool) : Bool → Expr → Option Cond := fun pos e => do diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean index 82390511..98cdc590 100644 --- a/LeanBridge/Lookup/Lookup.lean +++ b/LeanBridge/Lookup/Lookup.lean @@ -3,10 +3,10 @@ import ProofWidgets.Component.HtmlDisplay /-! # The `lookup` tactic -`lookup` reads the local hypotheses and the goal, translates them into a SQL query against -LMFDB that searches for a *counterexample* (a database object satisfying all the hypotheses but -**violating** the goal), and reports it if one is found. It never closes the goal: a hit shows -the statement is false, and a miss is only evidence (the database is not exhaustive). +`lookup` reads the local hypotheses and the goal, translates them into a SQL query against LMFDB +that searches for a *counterexample* (a database object that satisfies every hypothesis but +violates the goal), and reports it if one is found. It never closes the goal: a hit shows the +statement is false, and a miss is only evidence, since the database is not exhaustive. The vocabulary lives in `LeanBridge.Lookup.Basic` and the table registry in `LeanBridge.Lookup.Tables`; this file wires them into the query, the report, and the tactic. -/ @@ -41,14 +41,14 @@ def runSql (sql : String) : MetaM Json := do /-! ## Dispatch: translating a `Prop` to a SQL condition -/ -/-- Find the scalar column an expression denotes (trying every table's recognisers), together -with the table it belongs to. -/ +/-- Find the scalar column an expression denotes, and its table, across every table's +recognisers. -/ def findScalar (e : Expr) : Option (Column × String) := tables.findSome? fun t => (t.scalars.findSome? (· e)).map (·, t.table) -/-- A column compared against an integer literal. A "signed" column stored as `sign * |·|` is -case-split on the sign, so the comparison hits the indexed absolute-value column rather than -the non-indexable product. -/ +/-- A column compared against an integer literal. For a signed column (`sign * |·|`), the +comparison case-splits on the sign to hit the indexed `abs` column instead of the non-indexable +product. -/ def colVsLit (c : Column) (table : String) (cmp : Cmp) (k : Int) : Cond := let core := match c.signed? with | some (signCol, absCol) => @@ -71,10 +71,10 @@ def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Cond := def combineCond (op : String) (a b : Cond) : Cond := { sql := s!"(({a.sql}) {op} ({b.sql}))", refs := a.refs ++ b.refs, table := a.table <|> b.table } -/-- Translate a `Prop` into a SQL condition. `positive := false` translates its negation; -pushing the negation down to the operator / boolean value / connective (rather than wrapping in -SQL `NOT (...)`) keeps the query index-friendly. `Not` flips the polarity, `Nonempty` is -transparent, and `∧`/`∨` are pushed through by De Morgan. -/ +/-- Translate a `Prop` into a SQL condition; `pos := false` translates its negation. The negation +is pushed onto the operator, boolean value, or connective instead of an SQL `NOT (...)`, to keep +the query index-friendly. `Not` flips polarity, `Nonempty` is transparent, `∧`/`∨` go through by +De Morgan. -/ partial def toCond (pos : Bool) (e : Expr) : Option Cond := match_expr e with | False => some { sql := if pos then "FALSE" else "TRUE" } @@ -127,9 +127,9 @@ def valueStrs (row : Json) (items : Array (String × String)) : Array String := return out open ProofWidgets in -/-- Render a counterexample row as interactive HTML, including a clickable LMFDB link. -A bare or markdown URL in a `MessageData` is not linkified by the infoview, so we build an -actual `` element and embed it via `MessageData.ofHtml`. -/ +/-- Render a counterexample row as interactive HTML with a clickable LMFDB link. The infoview +doesn't linkify a bare or markdown URL in `MessageData`, so we build an actual `` element and +embed it via `MessageData.ofHtml`. -/ def reportHtml (info : TableInfo) (row : Json) (items : Array (String × String)) : Html := let label := rowStr row "label" Html.element "div" #[] #[ @@ -151,9 +151,9 @@ def reportAlt (info : TableInfo) (row : Json) (items : Array (String × String)) /-! ## The tactic -/ -/-- Translate the hypotheses in context into SQL conditions. A hypothesis that *is* a -comparison but that we cannot translate is reported as a warning (and dropped), since silently -ignoring it would weaken any "no counterexample" conclusion. -/ +/-- Translate the context hypotheses into SQL conditions. If a hypothesis is a comparison we +can't translate, warn and drop it: ignoring it silently would weaken any "no counterexample" +conclusion. -/ def collectHypotheses : TacticM (Array Cond) := do let mut out : Array Cond := #[] for ldecl in ← getLCtx do diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean index a05da528..2fca2c72 100644 --- a/LeanBridge/Lookup/Tables.lean +++ b/LeanBridge/Lookup/Tables.lean @@ -2,9 +2,9 @@ import LeanBridge.Lookup.Basic /-! # LMFDB table registry -The object families `lookup` knows about. **To support a new family, add a `TableInfo` here** -(and list it in `tables`); **to teach an existing family a new column or property, add a -recogniser** to its `scalars`/`props` using the combinators from `LeanBridge.Lookup.Basic`. -/ +The object families `lookup` knows about. To add a family, add a `TableInfo` here and list it in +`tables`. To teach a family a new column or property, add a recogniser to its `scalars`/`props` +with the combinators from `LeanBridge.Lookup.Basic`. -/ open Lean @@ -90,7 +90,7 @@ def ecCurvedata : TableInfo where props := #[ -- `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)` ↦ torsion_structure = {n₁, …} isoStructure ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false, - -- `Finite W.Point` ↦ rank = 0 (Mordell–Weil group finite ⟺ rank zero) + -- `Finite W.Point` ↦ rank = 0 (Mordell-Weil group finite ⟺ rank zero) flagCondMentions ``Finite ``WeierstrassCurve.Affine.Point "rank = 0" "rank <> 0" #[("rank", "rank")], -- `IsAddTorsionFree W.Point` ↦ torsion = 1 @@ -139,9 +139,9 @@ def gpsGroups : TableInfo where -- `IsSolvable G` ↦ solvable = 't' flagIs ``IsSolvable "solvable"] -/-- Spaces of classical modular forms `S_k(Γ₀(N))` / `M_k(Γ₀(N))`. The object is identified by -its level and weight, read off the type `CuspForm Γ k` / `ModularForm Γ k` (with `Γ = Γ₀(N)`) -inside a `Module.finrank ℂ …` — see `modularDim`. -/ +/-- Spaces of classical modular forms `S_k(Γ₀(N))` / `M_k(Γ₀(N))`. Level and weight come from the +form type `CuspForm Γ k` / `ModularForm Γ k` (`Γ = Γ₀(N)`) inside a `Module.finrank ℂ …`; see +`modularDim`. -/ def mfNewspaces : TableInfo where table := "mf_newspaces" labelCol := "label"