Add Z3Counterexamples.lean, with a counterexample found by z3 (teorth…

…#291) Resolves a new edge that is still not covered by teorth#281, plus 5 more by transitivity. Includes in a comment the z3 spec that I ran, which involved bit vectors of length 3. When I tried the same thing with bit vectors of length 2, z3 said it was unsatisfiable.
b-mehta · Oct 5, 2024 · d99988d · d99988d
1 parent dac82d9
commit d99988d
Show file tree

Hide file tree

Showing 2 changed files with 100 additions and 0 deletions.
diff --git a/equational_theories.lean b/equational_theories.lean
@@ -12,3 +12,4 @@ import equational_theories.OrderMetatheorem
 import equational_theories.Preorder
 import equational_theories.SmallMagmas
 import equational_theories.Homomorphisms
+import equational_theories.Z3Counterexamples
diff --git a/equational_theories/Z3Counterexamples.lean b/equational_theories/Z3Counterexamples.lean
@@ -0,0 +1,99 @@
+import Mathlib.Tactic
+import equational_theories.AllEquations
+import equational_theories.FactsSyntax
+import equational_theories.MemoFinOp
+import equational_theories.DecideBang
+import equational_theories.EquationalResult
+
+namespace Z3Counterexamples
+
+/-
+Found with the following Z3 spec:
+```
+(declare-fun op ((_ BitVec 3) (_ BitVec 3)) (_ BitVec 3))
+
+(assert (forall ((x (_ BitVec 3)) (y (_ BitVec 3)) (z (_ BitVec 3)))
+                         (= x (op x (op (op y x) (op x z))))))
+
+(declare-const x (_ BitVec 3))
+(declare-const y (_ BitVec 3))
+(assert (not (= x (op x (op y x)))))
+
+(check-sat)
+(get-model)
+```
+-/
+
+def f_834_10 : Fin 8 → Fin 8 →  Fin 8
+| 0b010, 0b101 => ⟨0b110, by omega⟩
+| 0b101, 0b110 => ⟨0b111, by omega⟩
+| 0b101, 0b101 => ⟨0b000, by omega⟩
+| 0b101, 0b100 => ⟨0b101, by omega⟩
+| 0b110, 0b110 => ⟨0b000, by omega⟩
+| 0b110, 0b101 => ⟨0b000, by omega⟩
+| 0b101, 0b010 => ⟨0b110, by omega⟩
+| 0b010, 0b010 => ⟨0b101, by omega⟩
+| 0b110, 0b010 => ⟨0b110, by omega⟩
+| 0b110, 0b111 => ⟨0b000, by omega⟩
+| 0b111, 0b100 => ⟨0b001, by omega⟩
+| 0b101, 0b000 => ⟨0b101, by omega⟩
+| 0b010, 0b111 => ⟨0b010, by omega⟩
+| 0b111, 0b010 => ⟨0b111, by omega⟩
+| 0b000, 0b100 => ⟨0b001, by omega⟩
+| 0b010, 0b100 => ⟨0b010, by omega⟩
+| 0b100, 0b111 => ⟨0b011, by omega⟩
+| 0b010, 0b011 => ⟨0b110, by omega⟩
+| 0b000, 0b010 => ⟨0b000, by omega⟩
+| 0b100, 0b100 => ⟨0b011, by omega⟩
+| 0b100, 0b110 => ⟨0b100, by omega⟩
+| 0b110, 0b001 => ⟨0b110, by omega⟩
+| 0b111, 0b000 => ⟨0b100, by omega⟩
+| 0b011, 0b100 => ⟨0b011, by omega⟩
+| 0b000, 0b000 => ⟨0b100, by omega⟩
+| 0b000, 0b101 => ⟨0b000, by omega⟩
+| 0b000, 0b111 => ⟨0b001, by omega⟩
+| 0b000, 0b110 => ⟨0b100, by omega⟩
+| 0b110, 0b100 => ⟨0b110, by omega⟩
+| 0b101, 0b001 => ⟨0b101, by omega⟩
+| 0b111, 0b001 => ⟨0b111, by omega⟩
+| 0b100, 0b001 => ⟨0b011, by omega⟩
+| 0b001, 0b100 => ⟨0b010, by omega⟩
+| 0b001, 0b001 => ⟨0b001, by omega⟩
+| 0b001, 0b110 => ⟨0b001, by omega⟩
+| 0b011, 0b001 => ⟨0b010, by omega⟩
+| 0b001, 0b101 => ⟨0b001, by omega⟩
+| 0b001, 0b111 => ⟨0b001, by omega⟩
+| 0b111, 0b110 => ⟨0b100, by omega⟩
+| 0b000, 0b001 => ⟨0b001, by omega⟩
+| 0b100, 0b010 => ⟨0b100, by omega⟩
+| 0b010, 0b000 => ⟨0b010, by omega⟩
+| 0b001, 0b010 => ⟨0b001, by omega⟩
+| 0b111, 0b101 => ⟨0b100, by omega⟩
+| 0b100, 0b000 => ⟨0b011, by omega⟩
+| 0b010, 0b001 => ⟨0b010, by omega⟩
+| 0b001, 0b000 => ⟨0b011, by omega⟩
+| 0b100, 0b011 => ⟨0b100, by omega⟩
+| 0b110, 0b000 => ⟨0b100, by omega⟩
+| 0b010, 0b110 => ⟨0b010, by omega⟩
+| 0b110, 0b011 => ⟨0b110, by omega⟩
+| 0b000, 0b011 => ⟨0b000, by omega⟩
+| 0b001, 0b011 => ⟨0b010, by omega⟩
+| 0b011, 0b010 => ⟨0b101, by omega⟩
+| 0b100, 0b101 => ⟨0b100, by omega⟩
+| 0b011, 0b111 => ⟨0b011, by omega⟩
+| 0b011, 0b011 => ⟨0b010, by omega⟩
+| 0b111, 0b011 => ⟨0b111, by omega⟩
+| 0b101, 0b111 => ⟨0b000, by omega⟩
+| 0b111, 0b111 => ⟨0b001, by omega⟩
+| 0b101, 0b011 => ⟨0b101, by omega⟩
+| 0b011, 0b000 => ⟨0b011, by omega⟩
+| 0b011, 0b101 => ⟨0b011, by omega⟩
+| 0b011, 0b110 => ⟨0b011, by omega⟩
+
+def Magma834_10 : Magma (Fin 8) where op := f_834_10
+
+-- TODO use calculate_facts to find more places where this magma helps.
+
+@[equational_result]
+theorem Equation834_not_implies_Equation10 : ∃ (G: Type) (_: Magma G), Facts G [834] [10] :=
+  ⟨Fin 8, Magma834_10, by decide!⟩