teorth · nomeata · Sep 30, 2024 · Sep 27, 2024 · Sep 27, 2024 · Sep 27, 2024
diff --git a/.gitattributes b/.gitattributes
@@ -0,0 +1,2 @@
+
+equational_theories/FinitePoly/Refutation*.lean linguist-generated
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
@@ -51,6 +51,9 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake build equational_theories
 
+      - name: Build Counterexamples
+        run: LEAN_NUM_THREADS=1 ~/.elan/bin/lake build counterexamples
+
       - name: Cache mathlib API docs
         uses: actions/cache@v4
         with:

diff --git a/DecideBang.lean b/DecideBang.lean
@@ -0,0 +1,85 @@
+import Lean
+
+/-!
+This is a variant of the `decide` tactic that doesn’t actually check the proposition in meta code.
+This is useful in non-interactive mode, where we know it will succeed, and we really just want the
+check done once, in the kernel.
+
+This also includes a hack to do large disjunctions outside the `decdies`, as inference can blow up.
+-/
+
+open Lean Elab Tactic Meta
+
+private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
+  let mut expectedType ← instantiateMVars expectedType
+  if expectedType.hasFVar then
+    expectedType ← zetaReduce expectedType
+  if expectedType.hasFVar || expectedType.hasMVar then
+    throwError "expected type must not contain free or meta variables{indentExpr expectedType}"
+  return expectedType
+
+private def splitConjs (e : Lean.Expr) : Array (Lean.Expr) := Id.run do
+  let mut e := e
+  let mut r := #[]
+  while e.isAppOf `And do
+    r := r.push e.appFn!.appArg!
+    e := e.appArg!
+  r := r.push e
+  return r
+
+elab "decide!" : tactic => do
+  closeMainGoalUsing `decide fun expectedType => do
+    let expectedType ← preprocessPropToDecide expectedType
+    let expectedTypes := splitConjs expectedType
+    let proofs ← expectedTypes.mapM fun expectedType => do
+      let d ← mkDecide expectedType
+      let d ← instantiateMVars d
+      -- Get instance from `d`
+      let s := d.appArg!
+      let rflPrf ← mkEqRefl (toExpr true)
+      return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
+    let proof ← proofs.pop.foldrM (mkAppM ``And.intro #[·, ·]) proofs.back
+    return proof
+
+private partial def inferDecideFin (p : Expr) : MetaM Expr := do
+  let p ← whnfR p
+  match p with
+  | .forallE i d b bi =>
+    match_expr (← whnfR d) with
+    | Fin n =>
+      let inst ← withLocalDeclD i d fun x => do
+        let body := b.instantiate1 x
+        let inst ← inferDecideFin body
+        mkLambdaFVars #[x] inst
+      return mkApp3 (mkConst ``Nat.decidableForallFin) n (.lam i d b bi) inst
+    | _ => throwError "Expected Fin n quantifier"
+  | _ =>
+    match_expr p with
+    | Not p' =>
+      let inst ← inferDecideFin p'
+      return mkApp2 (mkConst ``instDecidableNot) p' inst
+    | Eq t l r =>
+      match_expr (← whnfR t) with
+      | Fin n =>
+        return mkApp3 (mkConst ``instDecidableEqFin) n l r
+      | _ => throwError "Expected Fin n equality"
+    | _ => throwError "Unsupported propositoin"
+
+
+/-!
+Like `decide!`, but only supports goals that are conjunctions of (possibly negations of) goals
+of the form `∀ (x … z : Fin n), lhs = rhs`.
+
+Using type class synthesis to infer the decidability instances can be very slow, slower than the
+actual proof checking, so this tactic construts the instances very directly.
+-/
+elab "decideFin!" : tactic => do
+  closeMainGoalUsing `decideFin fun expectedType => do
+    let expectedType ← preprocessPropToDecide expectedType
+    let expectedTypes := splitConjs expectedType
+    let proofs ← expectedTypes.mapM fun expectedType => do
+      let s ← inferDecideFin expectedType
+      let rflPrf ← mkEqRefl (toExpr true)
+      return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
+    let proof ← proofs.pop.foldrM (mkAppM ``And.intro #[·, ·]) proofs.back
+    return proof
diff --git a/data/finite_poly_refutations.txt b/data/finite_poly_refutations.txt
diff --git a/equational_theories/FinitePoly/Common.lean b/equational_theories/FinitePoly/Common.lean
diff --git a/equational_theories/FinitePoly/FactsSyntax.lean b/equational_theories/FinitePoly/FactsSyntax.lean
@@ -0,0 +1,49 @@
+import Lean
+import equational_theories.FinitePoly.Common
+
+/-!
+This defines a compact way of saying “Magma G satisfies this list of equations, but refutes these
+others”.
+-/
+
+-- May ways to skin the cat here; using syntactic macros to expand the conjunction,
+-- or an actual predicate `Facts G : List Nat → List Nat → Prop`.
+
+-- Trying the syntactic variant here
+
+
+syntax "Facts " term:max " [" num,* "] " " [" num,* "]" : term
+
+open Lean Meta Elab Term Tactic Parser.Term in
+elab_rules : term | `(Facts $G [ $sats,* ] [ $refs,*]) => do
+  let G ← elabTerm G none
+  let some u := (← getLevel G).dec | throwError "expected G to be a type"
+  let inst ← synthInstance (mkApp (mkConst ``Magma [u]) G)
+  let s := sats.getElems.map fun ⟨s⟩ =>
+    let n := .mkSimple s!"Equation{s.toNat}"
+    mkApp2 (mkConst n [u]) G inst
+  let r := refs.getElems.map fun ⟨s⟩ =>
+    let n := .mkSimple s!"Equation{s.toNat}"
+    mkApp (mkConst ``Not)  (mkApp2 (mkConst n [u]) G inst)
+  let e := mkAndN (s ++ r).toList
+  return e
+
+example (G : Type _) [Magma G] :
+   Facts G [1, 2] [4, 5] ↔ (Equation1 G ∧ Equation2 G ∧ ¬ Equation4 G ∧ ¬ Equation5 G) :=
+   Iff.rfl
+
+example (G : Type _) [Magma G] :
+   Facts G [1] [4, 5] ↔ (Equation1 G ∧ ¬ Equation4 G ∧ ¬ Equation5 G) :=
+   Iff.rfl
+
+example (G : Type _) [Magma G] :
+   Facts G [] [4, 5] ↔ (¬ Equation4 G ∧ ¬ Equation5 G) :=
+   Iff.rfl
+
+example (G : Type _) [Magma G] :
+   Facts G [1, 2] [] ↔ (Equation1 G ∧ Equation2 G) :=
+   Iff.rfl
+
+example (G : Type _) [Magma G] :
+   Facts G [] [] ↔ True :=
+   Iff.rfl
diff --git a/equational_theories/FinitePoly/Refutation0.lean b/equational_theories/FinitePoly/Refutation0.lean
diff --git a/equational_theories/FinitePoly/Refutation1.lean b/equational_theories/FinitePoly/Refutation1.lean
diff --git a/equational_theories/FinitePoly/Refutation109.lean b/equational_theories/FinitePoly/Refutation109.lean
diff --git a/equational_theories/FinitePoly/Refutation11.lean b/equational_theories/FinitePoly/Refutation11.lean
diff --git a/equational_theories/FinitePoly/Refutation110.lean b/equational_theories/FinitePoly/Refutation110.lean
diff --git a/equational_theories/FinitePoly/Refutation111.lean b/equational_theories/FinitePoly/Refutation111.lean
diff --git a/equational_theories/FinitePoly/Refutation113.lean b/equational_theories/FinitePoly/Refutation113.lean
diff --git a/equational_theories/FinitePoly/Refutation114.lean b/equational_theories/FinitePoly/Refutation114.lean
diff --git a/equational_theories/FinitePoly/Refutation115.lean b/equational_theories/FinitePoly/Refutation115.lean
diff --git a/equational_theories/FinitePoly/Refutation116.lean b/equational_theories/FinitePoly/Refutation116.lean
diff --git a/equational_theories/FinitePoly/Refutation117.lean b/equational_theories/FinitePoly/Refutation117.lean
diff --git a/equational_theories/FinitePoly/Refutation119.lean b/equational_theories/FinitePoly/Refutation119.lean
diff --git a/equational_theories/FinitePoly/Refutation122.lean b/equational_theories/FinitePoly/Refutation122.lean
diff --git a/equational_theories/FinitePoly/Refutation125.lean b/equational_theories/FinitePoly/Refutation125.lean
diff --git a/equational_theories/FinitePoly/Refutation127.lean b/equational_theories/FinitePoly/Refutation127.lean
diff --git a/equational_theories/FinitePoly/Refutation129.lean b/equational_theories/FinitePoly/Refutation129.lean
diff --git a/equational_theories/FinitePoly/Refutation13.lean b/equational_theories/FinitePoly/Refutation13.lean
diff --git a/equational_theories/FinitePoly/Refutation131.lean b/equational_theories/FinitePoly/Refutation131.lean
diff --git a/equational_theories/FinitePoly/Refutation132.lean b/equational_theories/FinitePoly/Refutation132.lean
diff --git a/equational_theories/FinitePoly/Refutation134.lean b/equational_theories/FinitePoly/Refutation134.lean
diff --git a/equational_theories/FinitePoly/Refutation135.lean b/equational_theories/FinitePoly/Refutation135.lean
diff --git a/equational_theories/FinitePoly/Refutation138.lean b/equational_theories/FinitePoly/Refutation138.lean
diff --git a/equational_theories/FinitePoly/Refutation139.lean b/equational_theories/FinitePoly/Refutation139.lean
diff --git a/equational_theories/FinitePoly/Refutation14.lean b/equational_theories/FinitePoly/Refutation14.lean
diff --git a/equational_theories/FinitePoly/Refutation141.lean b/equational_theories/FinitePoly/Refutation141.lean
diff --git a/equational_theories/FinitePoly/Refutation142.lean b/equational_theories/FinitePoly/Refutation142.lean
diff --git a/equational_theories/FinitePoly/Refutation144.lean b/equational_theories/FinitePoly/Refutation144.lean
diff --git a/equational_theories/FinitePoly/Refutation146.lean b/equational_theories/FinitePoly/Refutation146.lean
diff --git a/equational_theories/FinitePoly/Refutation148.lean b/equational_theories/FinitePoly/Refutation148.lean
diff --git a/equational_theories/FinitePoly/Refutation150.lean b/equational_theories/FinitePoly/Refutation150.lean
diff --git a/equational_theories/FinitePoly/Refutation151.lean b/equational_theories/FinitePoly/Refutation151.lean
diff --git a/equational_theories/FinitePoly/Refutation152.lean b/equational_theories/FinitePoly/Refutation152.lean
diff --git a/equational_theories/FinitePoly/Refutation155.lean b/equational_theories/FinitePoly/Refutation155.lean
diff --git a/equational_theories/FinitePoly/Refutation157.lean b/equational_theories/FinitePoly/Refutation157.lean
diff --git a/equational_theories/FinitePoly/Refutation159.lean b/equational_theories/FinitePoly/Refutation159.lean
diff --git a/equational_theories/FinitePoly/Refutation161.lean b/equational_theories/FinitePoly/Refutation161.lean
diff --git a/equational_theories/FinitePoly/Refutation163.lean b/equational_theories/FinitePoly/Refutation163.lean
diff --git a/equational_theories/FinitePoly/Refutation167.lean b/equational_theories/FinitePoly/Refutation167.lean
diff --git a/equational_theories/FinitePoly/Refutation170.lean b/equational_theories/FinitePoly/Refutation170.lean
diff --git a/equational_theories/FinitePoly/Refutation172.lean b/equational_theories/FinitePoly/Refutation172.lean
diff --git a/equational_theories/FinitePoly/Refutation174.lean b/equational_theories/FinitePoly/Refutation174.lean
diff --git a/equational_theories/FinitePoly/Refutation175.lean b/equational_theories/FinitePoly/Refutation175.lean
diff --git a/equational_theories/FinitePoly/Refutation179.lean b/equational_theories/FinitePoly/Refutation179.lean
diff --git a/equational_theories/FinitePoly/Refutation180.lean b/equational_theories/FinitePoly/Refutation180.lean
diff --git a/equational_theories/FinitePoly/Refutation182.lean b/equational_theories/FinitePoly/Refutation182.lean
diff --git a/equational_theories/FinitePoly/Refutation186.lean b/equational_theories/FinitePoly/Refutation186.lean
diff --git a/equational_theories/FinitePoly/Refutation188.lean b/equational_theories/FinitePoly/Refutation188.lean
diff --git a/equational_theories/FinitePoly/Refutation189.lean b/equational_theories/FinitePoly/Refutation189.lean
diff --git a/equational_theories/FinitePoly/Refutation19.lean b/equational_theories/FinitePoly/Refutation19.lean
diff --git a/equational_theories/FinitePoly/Refutation190.lean b/equational_theories/FinitePoly/Refutation190.lean
diff --git a/equational_theories/FinitePoly/Refutation191.lean b/equational_theories/FinitePoly/Refutation191.lean
diff --git a/equational_theories/FinitePoly/Refutation196.lean b/equational_theories/FinitePoly/Refutation196.lean
diff --git a/equational_theories/FinitePoly/Refutation198.lean b/equational_theories/FinitePoly/Refutation198.lean
diff --git a/equational_theories/FinitePoly/Refutation199.lean b/equational_theories/FinitePoly/Refutation199.lean
diff --git a/equational_theories/FinitePoly/Refutation2.lean b/equational_theories/FinitePoly/Refutation2.lean
diff --git a/equational_theories/FinitePoly/Refutation20.lean b/equational_theories/FinitePoly/Refutation20.lean
diff --git a/equational_theories/FinitePoly/Refutation202.lean b/equational_theories/FinitePoly/Refutation202.lean
diff --git a/equational_theories/FinitePoly/Refutation207.lean b/equational_theories/FinitePoly/Refutation207.lean
diff --git a/equational_theories/FinitePoly/Refutation209.lean b/equational_theories/FinitePoly/Refutation209.lean
diff --git a/equational_theories/FinitePoly/Refutation21.lean b/equational_theories/FinitePoly/Refutation21.lean
diff --git a/equational_theories/FinitePoly/Refutation210.lean b/equational_theories/FinitePoly/Refutation210.lean
diff --git a/equational_theories/FinitePoly/Refutation212.lean b/equational_theories/FinitePoly/Refutation212.lean
diff --git a/equational_theories/FinitePoly/Refutation214.lean b/equational_theories/FinitePoly/Refutation214.lean
diff --git a/equational_theories/FinitePoly/Refutation218.lean b/equational_theories/FinitePoly/Refutation218.lean
diff --git a/equational_theories/FinitePoly/Refutation23.lean b/equational_theories/FinitePoly/Refutation23.lean
diff --git a/equational_theories/FinitePoly/Refutation24.lean b/equational_theories/FinitePoly/Refutation24.lean
diff --git a/equational_theories/FinitePoly/Refutation25.lean b/equational_theories/FinitePoly/Refutation25.lean
diff --git a/equational_theories/FinitePoly/Refutation28.lean b/equational_theories/FinitePoly/Refutation28.lean
diff --git a/equational_theories/FinitePoly/Refutation29.lean b/equational_theories/FinitePoly/Refutation29.lean
diff --git a/equational_theories/FinitePoly/Refutation3.lean b/equational_theories/FinitePoly/Refutation3.lean
diff --git a/equational_theories/FinitePoly/Refutation30.lean b/equational_theories/FinitePoly/Refutation30.lean
diff --git a/equational_theories/FinitePoly/Refutation31.lean b/equational_theories/FinitePoly/Refutation31.lean
diff --git a/equational_theories/FinitePoly/Refutation34.lean b/equational_theories/FinitePoly/Refutation34.lean
diff --git a/equational_theories/FinitePoly/Refutation35.lean b/equational_theories/FinitePoly/Refutation35.lean
diff --git a/equational_theories/FinitePoly/Refutation36.lean b/equational_theories/FinitePoly/Refutation36.lean
diff --git a/equational_theories/FinitePoly/Refutation37.lean b/equational_theories/FinitePoly/Refutation37.lean
diff --git a/equational_theories/FinitePoly/Refutation38.lean b/equational_theories/FinitePoly/Refutation38.lean
diff --git a/equational_theories/FinitePoly/Refutation4.lean b/equational_theories/FinitePoly/Refutation4.lean
diff --git a/equational_theories/FinitePoly/Refutation42.lean b/equational_theories/FinitePoly/Refutation42.lean
diff --git a/equational_theories/FinitePoly/Refutation44.lean b/equational_theories/FinitePoly/Refutation44.lean
diff --git a/equational_theories/FinitePoly/Refutation45.lean b/equational_theories/FinitePoly/Refutation45.lean
diff --git a/equational_theories/FinitePoly/Refutation5.lean b/equational_theories/FinitePoly/Refutation5.lean
diff --git a/equational_theories/FinitePoly/Refutation50.lean b/equational_theories/FinitePoly/Refutation50.lean
diff --git a/equational_theories/FinitePoly/Refutation54.lean b/equational_theories/FinitePoly/Refutation54.lean
diff --git a/equational_theories/FinitePoly/Refutation56.lean b/equational_theories/FinitePoly/Refutation56.lean
diff --git a/equational_theories/FinitePoly/Refutation6.lean b/equational_theories/FinitePoly/Refutation6.lean
diff --git a/equational_theories/FinitePoly/Refutation60.lean b/equational_theories/FinitePoly/Refutation60.lean
diff --git a/equational_theories/FinitePoly/Refutation61.lean b/equational_theories/FinitePoly/Refutation61.lean
diff --git a/equational_theories/FinitePoly/Refutation63.lean b/equational_theories/FinitePoly/Refutation63.lean
diff --git a/equational_theories/FinitePoly/Refutation64.lean b/equational_theories/FinitePoly/Refutation64.lean
diff --git a/equational_theories/FinitePoly/Refutation65.lean b/equational_theories/FinitePoly/Refutation65.lean
diff --git a/equational_theories/FinitePoly/Refutation66.lean b/equational_theories/FinitePoly/Refutation66.lean
diff --git a/equational_theories/FinitePoly/Refutation67.lean b/equational_theories/FinitePoly/Refutation67.lean
diff --git a/equational_theories/FinitePoly/Refutation68.lean b/equational_theories/FinitePoly/Refutation68.lean
diff --git a/equational_theories/FinitePoly/Refutation7.lean b/equational_theories/FinitePoly/Refutation7.lean
diff --git a/equational_theories/FinitePoly/Refutation71.lean b/equational_theories/FinitePoly/Refutation71.lean
diff --git a/equational_theories/FinitePoly/Refutation74.lean b/equational_theories/FinitePoly/Refutation74.lean
diff --git a/equational_theories/FinitePoly/Refutation75.lean b/equational_theories/FinitePoly/Refutation75.lean
diff --git a/equational_theories/FinitePoly/Refutation78.lean b/equational_theories/FinitePoly/Refutation78.lean
diff --git a/equational_theories/FinitePoly/Refutation79.lean b/equational_theories/FinitePoly/Refutation79.lean
diff --git a/equational_theories/FinitePoly/Refutation8.lean b/equational_theories/FinitePoly/Refutation8.lean
diff --git a/equational_theories/FinitePoly/Refutation81.lean b/equational_theories/FinitePoly/Refutation81.lean
diff --git a/equational_theories/FinitePoly/Refutation84.lean b/equational_theories/FinitePoly/Refutation84.lean
diff --git a/equational_theories/FinitePoly/Refutation86.lean b/equational_theories/FinitePoly/Refutation86.lean
diff --git a/equational_theories/FinitePoly/Refutation87.lean b/equational_theories/FinitePoly/Refutation87.lean
diff --git a/equational_theories/FinitePoly/Refutation88.lean b/equational_theories/FinitePoly/Refutation88.lean
diff --git a/equational_theories/FinitePoly/Refutation93.lean b/equational_theories/FinitePoly/Refutation93.lean
diff --git a/equational_theories/FinitePoly/Refutation94.lean b/equational_theories/FinitePoly/Refutation94.lean
diff --git a/equational_theories/FinitePoly/Refutation97.lean b/equational_theories/FinitePoly/Refutation97.lean
diff --git a/equational_theories/FinitePoly/Refutation99.lean b/equational_theories/FinitePoly/Refutation99.lean
diff --git a/equational_theories/FinitePolyExample.lean b/equational_theories/FinitePolyExample.lean
@@ -0,0 +1,26 @@
+-- This is an example file, repesenting the generated files, but with shorter lists
+
+
+import DecideBang
+import equational_theories.FinitePoly.Common
+import equational_theories.FinitePoly.FactsSyntax
+
+/-!
+This file is generated from the following refutation as produced by
+random generation of polynomials:
+'(4 * x**2 + 4 * y**2 + 4 * x + 4 * y + 0 * x * y) % 5' (0, 42, 3252, 3318, 3341, 3455, 3521, 3544, 3861, 3914, 3963, 4064, 4117, 4166, 4282, 4357, 4379, 4397, 4404, 4434, 4441, 4481, 4530, 4543, 4634, 4676)
+
+-/
+
+set_option maxRecDepth 100000
+set_option synthInstance.maxHeartbeats 20000000
+
+/-! The magma definition -/
+def «FinitePoly 4 * x² + 4 * y² + 4 * x + 4 * y» : Magma (Fin 5) where
+  op x y := 4 * x*x + 4 * y*y + 4 * x + 4 * y
+
+/-! The facts -/
+theorem «Facts from FinitePoly 4 * x² + 4 * y² + 4 * x + 4 * y» :
+  ∃ (G : Type) (_ : Magma G), Facts G [1, 43, 3253] [2, 3, 4] := by
+    refine ⟨Fin 5, «FinitePoly 4 * x² + 4 * y² + 4 * x + 4 * y», ?_⟩
+    decideFin!
diff --git a/lakefile.toml b/lakefile.toml
@@ -1,28 +1,38 @@
-name = "equational_theories"
-defaultTargets = ["equational_theories"]
-
-[leanOptions]
-pp.unicode.fun = true
-autoImplicit = false
-relaxedAutoImplicit = false
-
-[[require]]
-name = "mathlib"
-git = "https://github.com/leanprover-community/mathlib4.git"
-
-[[require]]
-name = "checkdecls"
-git = "https://github.com/PatrickMassot/checkdecls.git"
-
-[[require]]
-name = "«doc-gen4»"
-git = "https://github.com/leanprover/doc-gen4"
-rev = "main"
-
-[[lean_lib]]
-name = "equational_theories"
-
-[[require]]
-name = "egg"
-git  = "https://github.com/marcusrossel/lean-egg"
-rev  = "main"
+name = "equational_theories"
+defaultTargets = ["equational_theories"]
+
+[leanOptions]
+pp.unicode.fun = true
+autoImplicit = false
+relaxedAutoImplicit = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+
+[[require]]
+name = "checkdecls"
+git = "https://github.com/PatrickMassot/checkdecls.git"
+
+[[require]]
+name = "«doc-gen4»"
+git = "https://github.com/leanprover/doc-gen4"
+rev = "main"
+
+[[lean_lib]]
+name = "equational_theories"
+
+# until this tactic is upstreamed we want to run it as compiled code
+[[lean_lib]]
+name = "DecideBang"
+root = "DecideBang"
+precompileModules = true
+
+[[lean_lib]]
+name = "counterexamples"
+globs = "equational_theories.FinitePoly.+"
+
+[[require]]
+name = "egg"
+git  = "https://github.com/marcusrossel/lean-egg"
+rev  = "main"
diff --git a/scripts/finite_poly_generate_lean.py b/scripts/finite_poly_generate_lean.py
@@ -0,0 +1,75 @@
+#! /usr/bin/env python3
+
+import ast
+import re
+
+#
+# This script reads the file `finite_poly_refutations.txt` and turns each line into a
+# a file `equational_theories/FinitePoly/Refutation<n>.lean`
+#
+
+
+# we have 4694 equations
+full = set(list(range(4694)))
+
+def generate_lean(refutation_line):
+    _, eq, nums = refutation_line.split("'")
+    data = set(ast.literal_eval(nums.strip()))
+    # the numbers are off by one, the offcial equations list is 1-indexed
+    satisfied = [i+1 for i in range(4694) if i in data]
+    refuted = [i+1 for i in range(4694) if i not in data]
+
+    # we turn the equation as printed in the refutation file into a valid lean expression,
+    # and a pretty version of it for the name. We also remove trivial factors and summands
+    m = re.match(r"\((.*)\) % (.*)", eq)
+    div = int(m.group(2))
+
+    summands = m.group(1).split(" + ")
+    summands = [ s.removeprefix("1 * ") for s in summands if not s.startswith("0 * ") ]
+    poly = " + ".join(summands) if summands else "0"
+
+    pretty_eq = poly
+    pretty_eq = pretty_eq.replace("**2", "²")
+    poly = poly.replace("x**2", "x*x").replace("y**2", "y*y")
+
+    name = f"FinitePoly {pretty_eq}"
+    satname= lambda i: f"{name} satisfies Equation{i}"
+    refname= lambda i: f"{name} refutes Equation{i}"
+
+    out = f"""
+import DecideBang
+import equational_theories.FinitePoly.Common
+import equational_theories.FinitePoly.FactsSyntax
+
+/-!
+This file is generated from the following refutation as produced by
+random generation of polynomials:
+{refutation_line}
+-/
+
+set_option maxRecDepth 10000000
+set_option maxHeartbeats 200000000
+set_option synthInstance.maxHeartbeats 200000000
+set_option linter.unusedVariables false
+
+/-! The magma definition -/
+def «{name}» : Magma (Fin {div}) where
+  op x y := {poly}
+
+/-! The facts -/
+theorem «Facts from {name}» :
+  ∃ (G : Type) (_ : Magma G), Facts G {satisfied} {refuted} := by
+    refine ⟨Fin {div}, «{name}», ?_⟩
+    decideFin!
+"""
+    return out
+
+
+with open("data/finite_poly_refutations.txt") as f:
+    lines = f.readlines()
+    for i, line in enumerate(lines):
+        leanfile = f"equational_theories/FinitePoly/Refutation{i}.lean"
+        print(f"Writing {leanfile}")
+        if not "seen" in line:
+          with open(leanfile, "w") as f:
+                f.write(generate_lean(line))