generated from pitmonticone/LeanProject
-
Notifications
You must be signed in to change notification settings - Fork 40
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Massive generation of refutations via polynomials over Z/nZ (#19)
* Massive generation of refutations via polynomials over cyclic groups * Use compact syntax to good effect * Use compact syntax, actually commit files * Add counterexamples as separate lib * Do not generate empty files * Remove debugging check * Make DecideBang tactic compiled * Fix bad formula mangling * Introduce decideFin! tactic to avoid type inference overhead. 2.5× times faster! * linter.unusedVariables false * Build counter-examples not parallel * Remove example, now that we can commit the files * Docstring and other cosmetics * Import more refutations * Only include magmas with <5 elements for now * Try to use native decide * Try to balance the large conjunction * Hidingt the inst in a top-level declaration does not help * Revert * Use Magma file, mild refactoring * Memoize monoid op * Typos * Put AllEquations into a namespace for now * Move DecideBang back into main library * SmallMagmas file * Different examples * Move to Generated * Prune counter-examples based on implications * Prune much more * Include more magmas * Remove dead code * Also prune based on covering * Set equational_result
- Loading branch information
Showing
138 changed files
with
39,321 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
23 changes: 23 additions & 0 deletions
23
equational_theories/Generated/FinitePoly/Refutation108.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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!⟩ |
Oops, something went wrong.