Massive generation of refutations via polynomials over Z/nZ

.gitattributes

@@ -2,3 +2,6 @@ equational_theories/Generated/TrivialBruteforce/theorems/Apply.lean linguist-gen
 equational_theories/Generated/TrivialBruteforce/theorems/RewriteGoal.lean linguist-generated
 equational_theories/Generated/TrivialBruteforce/theorems/RewriteHypothesis.lean linguist-generated
 equational_theories/Generated/TrivialBruteforce/theorems/RewriteHypothesisAndGoal.lean linguist-generated
+
+equational_theories/FinitePoly/Refutation*.lean linguist-generated
+equational_theories/FinitePoly.lean linguist-generated

equational_theories/Generated.lean

@@ -2,3 +2,4 @@ import equational_theories.Generated.SimpleRewrites
 import equational_theories.Generated.Constant
 import equational_theories.Generated.Singleton
 import equational_theories.Generated.TrivialBruteforce
+import equational_theories.Generated.FinitePoly

equational_theories/Generated/FinitePoly.lean

@@ -0,0 +1,132 @@
+import equational_theories.Generated.FinitePoly.Refutation6
+import equational_theories.Generated.FinitePoly.Refutation8
+import equational_theories.Generated.FinitePoly.Refutation14
+import equational_theories.Generated.FinitePoly.Refutation18
+import equational_theories.Generated.FinitePoly.Refutation20
+import equational_theories.Generated.FinitePoly.Refutation24
+import equational_theories.Generated.FinitePoly.Refutation26
+import equational_theories.Generated.FinitePoly.Refutation32
+import equational_theories.Generated.FinitePoly.Refutation34
+import equational_theories.Generated.FinitePoly.Refutation40
+import equational_theories.Generated.FinitePoly.Refutation46
+import equational_theories.Generated.FinitePoly.Refutation50
+import equational_theories.Generated.FinitePoly.Refutation56
+import equational_theories.Generated.FinitePoly.Refutation60
+import equational_theories.Generated.FinitePoly.Refutation66
+import equational_theories.Generated.FinitePoly.Refutation68
+import equational_theories.Generated.FinitePoly.Refutation72
+import equational_theories.Generated.FinitePoly.Refutation74
+import equational_theories.Generated.FinitePoly.Refutation78
+import equational_theories.Generated.FinitePoly.Refutation82
+import equational_theories.Generated.FinitePoly.Refutation84
+import equational_theories.Generated.FinitePoly.Refutation88
+import equational_theories.Generated.FinitePoly.Refutation90
+import equational_theories.Generated.FinitePoly.Refutation92
+import equational_theories.Generated.FinitePoly.Refutation94
+import equational_theories.Generated.FinitePoly.Refutation96
+import equational_theories.Generated.FinitePoly.Refutation108
+import equational_theories.Generated.FinitePoly.Refutation112
+import equational_theories.Generated.FinitePoly.Refutation114
+import equational_theories.Generated.FinitePoly.Refutation116
+import equational_theories.Generated.FinitePoly.Refutation120
+import equational_theories.Generated.FinitePoly.Refutation126
+import equational_theories.Generated.FinitePoly.Refutation128
+import equational_theories.Generated.FinitePoly.Refutation132
+import equational_theories.Generated.FinitePoly.Refutation138
+import equational_theories.Generated.FinitePoly.Refutation144
+import equational_theories.Generated.FinitePoly.Refutation146
+import equational_theories.Generated.FinitePoly.Refutation150
+import equational_theories.Generated.FinitePoly.Refutation152
+import equational_theories.Generated.FinitePoly.Refutation154
+import equational_theories.Generated.FinitePoly.Refutation172
+import equational_theories.Generated.FinitePoly.Refutation174
+import equational_theories.Generated.FinitePoly.Refutation176
+import equational_theories.Generated.FinitePoly.Refutation178
+import equational_theories.Generated.FinitePoly.Refutation184
+import equational_theories.Generated.FinitePoly.Refutation190
+import equational_theories.Generated.FinitePoly.Refutation194
+import equational_theories.Generated.FinitePoly.Refutation196
+import equational_theories.Generated.FinitePoly.Refutation198
+import equational_theories.Generated.FinitePoly.Refutation200
+import equational_theories.Generated.FinitePoly.Refutation206
+import equational_theories.Generated.FinitePoly.Refutation208
+import equational_theories.Generated.FinitePoly.Refutation212
+import equational_theories.Generated.FinitePoly.Refutation214
+import equational_theories.Generated.FinitePoly.Refutation216
+import equational_theories.Generated.FinitePoly.Refutation218
+import equational_theories.Generated.FinitePoly.Refutation220
+import equational_theories.Generated.FinitePoly.Refutation226
+import equational_theories.Generated.FinitePoly.Refutation232
+import equational_theories.Generated.FinitePoly.Refutation234
+import equational_theories.Generated.FinitePoly.Refutation236
+import equational_theories.Generated.FinitePoly.Refutation238
+import equational_theories.Generated.FinitePoly.Refutation246
+import equational_theories.Generated.FinitePoly.Refutation250
+import equational_theories.Generated.FinitePoly.Refutation262
+import equational_theories.Generated.FinitePoly.Refutation264
+import equational_theories.Generated.FinitePoly.Refutation268
+import equational_theories.Generated.FinitePoly.Refutation270
+import equational_theories.Generated.FinitePoly.Refutation272
+import equational_theories.Generated.FinitePoly.Refutation280
+import equational_theories.Generated.FinitePoly.Refutation284
+import equational_theories.Generated.FinitePoly.Refutation286
+import equational_theories.Generated.FinitePoly.Refutation290
+import equational_theories.Generated.FinitePoly.Refutation302
+import equational_theories.Generated.FinitePoly.Refutation312
+import equational_theories.Generated.FinitePoly.Refutation314
+import equational_theories.Generated.FinitePoly.Refutation316
+import equational_theories.Generated.FinitePoly.Refutation318
+import equational_theories.Generated.FinitePoly.Refutation320
+import equational_theories.Generated.FinitePoly.Refutation326
+import equational_theories.Generated.FinitePoly.Refutation328
+import equational_theories.Generated.FinitePoly.Refutation330
+import equational_theories.Generated.FinitePoly.Refutation340
+import equational_theories.Generated.FinitePoly.Refutation342
+import equational_theories.Generated.FinitePoly.Refutation344
+import equational_theories.Generated.FinitePoly.Refutation346
+import equational_theories.Generated.FinitePoly.Refutation352
+import equational_theories.Generated.FinitePoly.Refutation356
+import equational_theories.Generated.FinitePoly.Refutation364
+import equational_theories.Generated.FinitePoly.Refutation366
+import equational_theories.Generated.FinitePoly.Refutation370
+import equational_theories.Generated.FinitePoly.Refutation374
+import equational_theories.Generated.FinitePoly.Refutation380
+import equational_theories.Generated.FinitePoly.Refutation386
+import equational_theories.Generated.FinitePoly.Refutation388
+import equational_theories.Generated.FinitePoly.Refutation390
+import equational_theories.Generated.FinitePoly.Refutation394
+import equational_theories.Generated.FinitePoly.Refutation400
+import equational_theories.Generated.FinitePoly.Refutation402
+import equational_theories.Generated.FinitePoly.Refutation404
+import equational_theories.Generated.FinitePoly.Refutation406
+import equational_theories.Generated.FinitePoly.Refutation408
+import equational_theories.Generated.FinitePoly.Refutation410
+import equational_theories.Generated.FinitePoly.Refutation418
+import equational_theories.Generated.FinitePoly.Refutation420
+import equational_theories.Generated.FinitePoly.Refutation422
+import equational_theories.Generated.FinitePoly.Refutation424
+import equational_theories.Generated.FinitePoly.Refutation426
+import equational_theories.Generated.FinitePoly.Refutation432
+import equational_theories.Generated.FinitePoly.Refutation444
+import equational_theories.Generated.FinitePoly.Refutation454
+import equational_theories.Generated.FinitePoly.Refutation470
+import equational_theories.Generated.FinitePoly.Refutation472
+import equational_theories.Generated.FinitePoly.Refutation474
+import equational_theories.Generated.FinitePoly.Refutation476
+import equational_theories.Generated.FinitePoly.Refutation482
+import equational_theories.Generated.FinitePoly.Refutation488
+import equational_theories.Generated.FinitePoly.Refutation492
+import equational_theories.Generated.FinitePoly.Refutation502
+import equational_theories.Generated.FinitePoly.Refutation532
+import equational_theories.Generated.FinitePoly.Refutation550
+import equational_theories.Generated.FinitePoly.Refutation568
+import equational_theories.Generated.FinitePoly.Refutation620
+import equational_theories.Generated.FinitePoly.Refutation622
+import equational_theories.Generated.FinitePoly.Refutation636
+import equational_theories.Generated.FinitePoly.Refutation656
+import equational_theories.Generated.FinitePoly.Refutation664
+import equational_theories.Generated.FinitePoly.Refutation672
+import equational_theories.Generated.FinitePoly.Refutation674
+import equational_theories.Generated.FinitePoly.Refutation676
+import equational_theories.Generated.FinitePoly.Refutation682
+import equational_theories.Generated.FinitePoly.Refutation690

equational_theories/Generated/FinitePoly/Refutation108.lean

@@ -0,0 +1,23 @@
+
+import equational_theories.AllEquations
+import equational_theories.FactsSyntax
+import equational_theories.MemoFinOp
+import equational_theories.DecideBang
+
+/-!
+This file is generated from the following refutation as produced by
+random generation of polynomials:
+'(1 * x**2 + 1 * y**2 + 0 * x + 0 * y + 0 * x * y) % 2' (0, 7, 10, 13, 15, 22, 25, 28, 30, 39, 42, 410, 413, 416, 418, 426, 428, 435, 439, 443, 451, 454, 463, 465, 472, 476, 480, 488, 491, 499, 503, 507, 510, 512, 521, 527, 542, 545, 555, 561, 571, 574, 613, 616, 619, 621, 629, 631, 638, 642, 646, 654, 657, 666, 668, 675, 679, 683, 691, 694, 702, 706, 710, 713, 715, 724, 730, 745, 748, 758, 764, 774, 777, 816, 819, 822, 824, 832, 834, 841, 845, 849, 857, 860, 869, 871, 878, 882, 886, 894, 897, 905, 909, 913, 916, 918, 927, 933, 948, 951, 961, 967, 977, 980, 1019, 1022, 1025, 1027, 1035, 1037, 1044, 1048, 1052, 1060, 1063, 1072, 1074, 1081, 1085, 1089, 1097, 1100, 1108, 1112, 1116, 1119, 1121, 1130, 1136, 1151, 1154, 1164, 1170, 1180, 1183, 1222, 1225, 1228, 1230, 1238, 1240, 1247, 1251, 1255, 1263, 1266, 1275, 1277, 1284, 1288, 1292, 1300, 1303, 1311, 1315, 1319, 1322, 1324, 1333, 1339, 1354, 1357, 1367, 1373, 1383, 1386, 1425, 1428, 1431, 1433, 1441, 1443, 1450, 1454, 1458, 1466, 1469, 1478, 1480, 1487, 1491, 1495, 1503, 1506, 1514, 1518, 1522, 1525, 1527, 1536, 1542, 1557, 1560, 1570, 1576, 1586, 1589, 1628, 1631, 1634, 1636, 1644, 1646, 1653, 1657, 1661, 1669, 1672, 1681, 1683, 1690, 1694, 1698, 1706, 1709, 1717, 1721, 1725, 1728, 1730, 1739, 1745, 1760, 1763, 1773, 1779, 1789, 1792, 1831, 1834, 1837, 1839, 1847, 1849, 1856, 1860, 1864, 1872, 1875, 1884, 1886, 1893, 1897, 1901, 1909, 1912, 1920, 1924, 1928, 1931, 1933, 1942, 1948, 1963, 1966, 1976, 1982, 1992, 1995, 2034, 2037, 2040, 2042, 2050, 2052, 2059, 2063, 2067, 2075, 2078, 2087, 2089, 2096, 2100, 2104, 2112, 2115, 2123, 2127, 2131, 2134, 2136, 2145, 2151, 2166, 2169, 2179, 2185, 2195, 2198, 2237, 2240, 2243, 2245, 2253, 2255, 2262, 2266, 2270, 2278, 2281, 2290, 2292, 2299, 2303, 2307, 2315, 2318, 2326, 2330, 2334, 2337, 2339, 2348, 2354, 2369, 2372, 2382, 2388, 2398, 2401, 2440, 2443, 2446, 2448, 2456, 2458, 2465, 2469, 2473, 2481, 2484, 2493, 2495, 2502, 2506, 2510, 2518, 2521, 2529, 2533, 2537, 2540, 2542, 2551, 2557, 2572, 2575, 2585, 2591, 2601, 2604, 2643, 2646, 2649, 2651, 2659, 2661, 2668, 2672, 2676, 2684, 2687, 2696, 2698, 2705, 2709, 2713, 2721, 2724, 2732, 2736, 2740, 2743, 2745, 2754, 2760, 2775, 2778, 2788, 2794, 2804, 2807, 2846, 2849, 2852, 2854, 2862, 2864, 2871, 2875, 2879, 2887, 2890, 2899, 2901, 2908, 2912, 2916, 2924, 2927, 2935, 2939, 2943, 2946, 2948, 2957, 2963, 2978, 2981, 2991, 2997, 3007, 3010, 3049, 3052, 3055, 3057, 3065, 3067, 3074, 3078, 3082, 3090, 3093, 3102, 3104, 3111, 3115, 3119, 3127, 3130, 3138, 3142, 3146, 3149, 3151, 3160, 3166, 3181, 3184, 3194, 3200, 3210, 3213, 3252, 3255, 3258, 3260, 3268, 3270, 3277, 3281, 3285, 3293, 3296, 3305, 3307, 3314, 3318, 3322, 3330, 3333, 3341, 3345, 3349, 3352, 3354, 3363, 3369, 3384, 3387, 3397, 3403, 3413, 3416, 3455, 3458, 3461, 3463, 3471, 3473, 3480, 3484, 3488, 3496, 3499, 3508, 3510, 3517, 3521, 3525, 3533, 3536, 3544, 3548, 3552, 3555, 3557, 3566, 3572, 3587, 3590, 3600, 3606, 3616, 3619, 3658, 3661, 3664, 3666, 3674, 3676, 3683, 3687, 3691, 3699, 3702, 3711, 3713, 3720, 3724, 3728, 3736, 3739, 3747, 3751, 3755, 3758, 3760, 3769, 3775, 3790, 3793, 3803, 3809, 3819, 3822, 3861, 3864, 3867, 3869, 3877, 3879, 3886, 3890, 3894, 3902, 3905, 3914, 3916, 3923, 3927, 3931, 3939, 3942, 3950, 3954, 3958, 3961, 3963, 3972, 3978, 3993, 3996, 4006, 4012, 4022, 4025, 4064, 4067, 4070, 4072, 4080, 4082, 4089, 4093, 4097, 4105, 4108, 4117, 4119, 4126, 4130, 4134, 4142, 4145, 4153, 4157, 4161, 4164, 4166, 4175, 4181, 4196, 4199, 4209, 4215, 4225, 4228, 4269, 4272, 4274, 4282, 4289, 4296, 4304, 4306, 4319, 4324, 4331, 4340, 4357, 4361, 4363, 4368, 4379, 4382, 4385, 4387, 4395, 4397, 4404, 4408, 4412, 4420, 4423, 4432, 4434, 4441, 4445, 4449, 4457, 4460, 4468, 4472, 4476, 4479, 4481, 4490, 4496, 4511, 4514, 4524, 4530, 4540, 4543, 4584, 4587, 4589, 4597, 4604, 4611, 4619, 4621, 4634, 4639, 4646, 4655, 4672, 4676, 4678, 4683)
+-/
+
+set_option linter.unusedVariables false
+
+/-! The magma definition -/
+def «FinitePoly x² + y² % 2» : Magma (Fin 2) where
+  op := memoFinOp fun x y => x*x + y*y
+
+/-! The facts -/
+@[equational_result]
+theorem «Facts from FinitePoly x² + y² % 2» :
+  ∃ (G : Type) (_ : Magma G), Facts G [11, 26, 29, 43, 452, 455, 481, 492, 508, 522, 543, 546, 556, 572, 647, 655, 658, 684, 692, 695, 711, 725, 749, 759, 775, 861, 887, 895, 898, 914, 928, 949, 952, 962, 978, 1053, 1061, 1090, 1098, 1101, 1117, 1131, 1152, 1165, 1181, 1256, 1264, 1267, 1293, 1301, 1304, 1320, 1334, 1355, 1358, 1368, 1384, 1459, 1467, 1470, 1496, 1504, 1507, 1523, 1537, 1561, 1571, 1587, 1670, 1673, 1699, 1710, 1726, 1740, 1761, 1764, 1774, 1790, 1876, 1902, 1910, 1913, 1929, 1943, 1964, 1967, 1993, 2068, 2076, 2079, 2105, 2113, 2116, 2132, 2146, 2170, 2180, 2196, 2271, 2279, 2282, 2308, 2316, 2319, 2335, 2349, 2370, 2373, 2383, 2399, 2474, 2482, 2511, 2519, 2522, 2538, 2552, 2573, 2586, 2602, 2677, 2685, 2688, 2714, 2722, 2725, 2741, 2755, 2776, 2779, 2789, 2805, 2880, 2888, 2891, 2917, 2925, 2928, 2944, 2958, 2982, 2992, 3008, 3091, 3120, 3128, 3131, 3147, 3161, 3182, 3185, 3211, 3286, 3294, 3297, 3350, 3364, 3370, 3385, 3398, 3404, 3417, 3489, 3497, 3500, 3553, 3567, 3573, 3601, 3607, 3620, 3692, 3703, 3737, 3756, 3770, 3776, 3791, 3804, 3810, 3823, 3895, 3903, 3906, 3932, 3940, 3959, 3973, 3979, 4007, 4013, 4026, 4098, 4106, 4109, 4143, 4162, 4176, 4182, 4197, 4210, 4216, 4229, 4297, 4305, 4325, 4413, 4421, 4450, 4458, 4461, 4477, 4491, 4497, 4612, 4620, 4640] [2, 3, 9, 10, 13, 24, 25, 28, 38, 39, 47, 99, 151, 203, 255, 307, 331, 359, 407, 412, 413, 416, 420, 426, 430, 437, 439, 463, 467, 474, 476, 501, 503, 510, 615, 616, 619, 623, 629, 633, 640, 642, 666, 670, 677, 679, 704, 706, 713, 818, 819, 822, 826, 832, 836, 843, 845, 869, 873, 880, 882, 907, 909, 916, 1021, 1022, 1025, 1029, 1035, 1039, 1046, 1048, 1072, 1076, 1083, 1085, 1110, 1112, 1119, 1224, 1225, 1228, 1232, 1238, 1242, 1249, 1251, 1275, 1279, 1286, 1288, 1313, 1315, 1322, 1427, 1428, 1431, 1435, 1441, 1445, 1452, 1454, 1478, 1482, 1489, 1491, 1516, 1518, 1525, 1630, 1631, 1634, 1638, 1644, 1648, 1655, 1657, 1681, 1685, 1692, 1694, 1719, 1721, 1728, 1833, 1834, 1837, 1841, 1847, 1851, 1858, 1860, 1884, 1888, 1895, 1897, 1922, 1924, 1931, 2036, 2037, 2040, 2044, 2050, 2054, 2061, 2063, 2087, 2091, 2098, 2100, 2125, 2127, 2134, 2239, 2240, 2243, 2247, 2253, 2257, 2264, 2266, 2290, 2294, 2301, 2303, 2328, 2330, 2337, 2442, 2443, 2446, 2450, 2456, 2460, 2467, 2469, 2493, 2497, 2504, 2506, 2531, 2533, 2540, 2645, 2646, 2649, 2653, 2659, 2663, 2670, 2672, 2696, 2700, 2707, 2709, 2734, 2736, 2743, 2848, 2849, 2852, 2856, 2862, 2866, 2873, 2875, 2899, 2903, 2910, 2912, 2937, 2939, 2946, 3051, 3052, 3055, 3059, 3065, 3069, 3076, 3078, 3102, 3106, 3113, 3115, 3140, 3142, 3149, 3254, 3255, 3258, 3262, 3268, 3272, 3279, 3281, 3309, 3316, 3318, 3337, 3343, 3345, 3352, 3457, 3458, 3461, 3465, 3471, 3475, 3482, 3484, 3512, 3519, 3521, 3543, 3546, 3548, 3555, 3660, 3661, 3664, 3668, 3674, 3678, 3685, 3687, 3715, 3722, 3724, 3749, 3751, 3758, 3863, 3864, 3867, 3871, 3877, 3881, 3888, 3890, 3918, 3925, 3927, 3952, 3954, 3961, 4055, 4066, 4067, 4070, 4074, 4080, 4084, 4091, 4093, 4121, 4128, 4130, 4155, 4157, 4164, 4258, 4268, 4269, 4272, 4276, 4284, 4291, 4293, 4314, 4321, 4343, 4368, 4373, 4381, 4382, 4385, 4399, 4406, 4408, 4436, 4443, 4445, 4470, 4472, 4479, 4539, 4547, 4571, 4583, 4584, 4587, 4591, 4599, 4606, 4608, 4629, 4636, 4658, 4683, 4688] :=
+    ⟨Fin 2, «FinitePoly x² + y² % 2», by decideFin!⟩