Split examples of FactSyntax, remove unnecessary dependency in FreeMa…

…gma (#460) Makes `FactSyntax` not depend on `AllEquations` and `FreeMagma` not depend on `EquationalResults`. We need this to avoid cyclic dependencies on meta code. This is a cleanup that I'm factoring out of #459
teorth · Oct 9, 2024 · 2f89113 · 2f89113
1 parent c27789e
commit 2f89113
Show file tree

Hide file tree

Showing 6 changed files with 3 additions and 22 deletions.
diff --git a/equational_theories.lean b/equational_theories.lean
@@ -17,3 +17,4 @@ import equational_theories.CentralGroupoids
 import equational_theories.Z3Counterexamples
 import equational_theories.LinearOps
 import equational_theories.Confluence
+import equational_theories.FactsSyntaxExamples
diff --git a/equational_theories/AllEquations.lean b/equational_theories/AllEquations.lean
@@ -971,7 +971,6 @@ equation 949 := x = y ◇ ((z ◇ x) ◇ (y ◇ z))
 equation 950 := x = y ◇ ((z ◇ x) ◇ (y ◇ w))
 equation 951 := x = y ◇ ((z ◇ x) ◇ (z ◇ x))
 equation 952 := x = y ◇ ((z ◇ x) ◇ (z ◇ y))
-equation 953 := x = y ◇ ((z ◇ x) ◇ (z ◇ z))
 equation 954 := x = y ◇ ((z ◇ x) ◇ (z ◇ w))
 equation 955 := x = y ◇ ((z ◇ x) ◇ (w ◇ x))
 equation 956 := x = y ◇ ((z ◇ x) ◇ (w ◇ y))

diff --git a/equational_theories/Equations.lean b/equational_theories/Equations.lean
@@ -80,6 +80,8 @@ equation 381  :=  x ◇ y = (x ◇ z) ◇ y
 /-- from the mathoverflow post by paste bee -/
 equation 387  :=  x ◇ y = (y ◇ y) ◇ x
 
+equation 953 := x = y ◇ ((z ◇ x) ◇ (z ◇ z))
+
 /-- From a paper of Mendelsohn & Padmanabhan, this law axiomatizes abelian groups of exponent 2 -/
 equation 1571  :=  x = (y ◇ z) ◇ (y ◇ (x ◇ z))
 -- x = (y ◇ z) ◇ (y ◇ (x ◇ z))

diff --git a/equational_theories/FactsSyntax.lean b/equational_theories/FactsSyntax.lean
@@ -1,6 +1,5 @@
 import Lean
 import equational_theories.Magma
-import equational_theories.AllEquations
 
 /-!
 This defines a compact way of saying “Magma G satisfies this list of equations, but refutes these
@@ -34,25 +33,6 @@ elab_rules : term | `(Facts $G [ $sats,* ] [ $refs,*]) => do
   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
 
 open Lean Meta Elab Term Tactic Parser.Term in
 /--

diff --git a/equational_theories/FactsSyntaxExamples.lean b/equational_theories/FactsSyntaxExamples.lean
diff --git a/equational_theories/FreeMagma.lean b/equational_theories/FreeMagma.lean
@@ -1,4 +1,3 @@
-import equational_theories.EquationalResult
 import equational_theories.Homomorphisms
 
 universe u