From cf97f575addc6ba3fe58cd69fc5be0d6d4713ef6 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Tue, 8 Oct 2024 11:46:18 -0400 Subject: [PATCH] prove some nonimplications for Equations 2712 and 3545 (#430) This follows @zaklogician's procedure for adding a new magma, via the [Finite Magma Explorer](https://totallyqed.com/fme/). We already had the dual facts in [Refutation726](https://github.com/teorth/equational_theories/blob/11ab32cf92d0ce5c1516fef6f5e63251c8cd5b66/equational_theories/Generated/All4x4Tables/Refutation726.lean) and [VampireProven/Disproofs2](https://github.com/teorth/equational_theories/blob/11ab32cf92d0ce5c1516fef6f5e63251c8cd5b66/equational_theories/Generated/VampireProven/Disproofs2.lean#L81-L83). --- .../Generated/All4x4Tables.lean | 2 ++ .../Generated/All4x4Tables/Refutation742.lean | 22 +++++++++++++++++++ .../Generated/All4x4Tables/Refutation743.lean | 22 +++++++++++++++++++ .../Generated/All4x4Tables/data/extra.txt | 5 +++++ .../Generated/All4x4Tables/data/plan.txt | 7 ++++++ 5 files changed, 58 insertions(+) create mode 100644 equational_theories/Generated/All4x4Tables/Refutation742.lean create mode 100644 equational_theories/Generated/All4x4Tables/Refutation743.lean create mode 100644 equational_theories/Generated/All4x4Tables/data/extra.txt diff --git a/equational_theories/Generated/All4x4Tables.lean b/equational_theories/Generated/All4x4Tables.lean index 9171ad74..77c66aea 100644 --- a/equational_theories/Generated/All4x4Tables.lean +++ b/equational_theories/Generated/All4x4Tables.lean @@ -740,3 +740,5 @@ import equational_theories.Generated.All4x4Tables.Refutation738 import equational_theories.Generated.All4x4Tables.Refutation739 import equational_theories.Generated.All4x4Tables.Refutation740 import equational_theories.Generated.All4x4Tables.Refutation741 +import equational_theories.Generated.All4x4Tables.Refutation742 +import equational_theories.Generated.All4x4Tables.Refutation743 diff --git a/equational_theories/Generated/All4x4Tables/Refutation742.lean b/equational_theories/Generated/All4x4Tables/Refutation742.lean new file mode 100644 index 00000000..a3311dc5 --- /dev/null +++ b/equational_theories/Generated/All4x4Tables/Refutation742.lean @@ -0,0 +1,22 @@ + +import equational_theories.AllEquations +import equational_theories.FactsSyntax +import equational_theories.MemoFinOp +import equational_theories.DecideBang + +/-! +This file is generated from the following operator table: +[[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]] +-/ + +set_option linter.unusedVariables false + +/-! The magma definition -/ +def «FinitePoly [[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]]» : Magma (Fin 11) where + op := memoFinOp fun x y => [[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]][x.val]![y.val]! + +/-! The facts -/ +@[equational_result] +theorem «Facts from FinitePoly [[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]]» : + ∃ (G : Type) (_ : Magma G), Facts G [2712] [1647, 2240, 2459, 3068] := + ⟨Fin 11, «FinitePoly [[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]]», by decideFin!⟩ diff --git a/equational_theories/Generated/All4x4Tables/Refutation743.lean b/equational_theories/Generated/All4x4Tables/Refutation743.lean new file mode 100644 index 00000000..0e3571e3 --- /dev/null +++ b/equational_theories/Generated/All4x4Tables/Refutation743.lean @@ -0,0 +1,22 @@ + +import equational_theories.AllEquations +import equational_theories.FactsSyntax +import equational_theories.MemoFinOp +import equational_theories.DecideBang + +/-! +This file is generated from the following operator table: +[[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]] +-/ + +set_option linter.unusedVariables false + +/-! The magma definition -/ +def «FinitePoly [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]]» : Magma (Fin 17) where + op := memoFinOp fun x y => [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]][x.val]![y.val]! + +/-! The facts -/ +@[equational_result] +theorem «Facts from FinitePoly [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]]» : + ∃ (G : Type) (_ : Magma G), Facts G [3545] [3862] := + ⟨Fin 17, «FinitePoly [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]]», by decideFin!⟩ diff --git a/equational_theories/Generated/All4x4Tables/data/extra.txt b/equational_theories/Generated/All4x4Tables/data/extra.txt new file mode 100644 index 00000000..106ae2ac --- /dev/null +++ b/equational_theories/Generated/All4x4Tables/data/extra.txt @@ -0,0 +1,5 @@ +Table [[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]] +Proves [1,23,203,208,211,307,323,1629,2238,2243,2246,2253,2256,2263,2266,2273,2277,2281,2441,2443,2446,2449,2452,2456,2466,2476,2644,2646,2696,2706,2709,2712,3050,3065,3142,3253,3306,3456,3458,3519,3522,4065,4118,4128] + +Table [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]] +Proves [1,3456,3545] diff --git a/equational_theories/Generated/All4x4Tables/data/plan.txt b/equational_theories/Generated/All4x4Tables/data/plan.txt index ea645423..a2f7c535 100644 --- a/equational_theories/Generated/All4x4Tables/data/plan.txt +++ b/equational_theories/Generated/All4x4Tables/data/plan.txt @@ -2967,3 +2967,10 @@ Magma [[0,2,3,4,6,1,8,5,10,7,9],[2,1,6,5,7,4,10,9,0,8,3],[3,6,2,8,1,7,5,10,9,4,0 Satisfies [474,3113] Refutes [513,833,879,1026,1682,1721,1851,1885,2503,2650,2699,3079,3474,3868] +Magma [[2,1,2,2,4,2,6,4,8,2,2],[3,5,9,3,5,5,5,3,9,9,9],[0,6,6,3,4,5,6,7,6,9,9],[4,1,2,2,4,2,6,4,8,2,2],[0,8,2,3,8,5,8,5,8,9,10],[10,1,2,9,4,9,6,4,8,9,10],[0,8,2,3,5,5,5,5,8,9,10],[10,8,2,9,8,2,8,8,8,9,10],[0,6,9,3,4,5,6,7,9,9,9],[7,1,2,7,4,5,6,7,8,4,2],[7,6,6,7,4,5,6,7,6,4,6]] +Satisfies [2712] +Refutes [205,1647,2240,2459,2462,3068] + +Magma [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]] +Satisfies [3545] +Refutes [3862]