Massive generation of refutations via polynomials over Z/nZ

This PR adds a large number of automatically generated refutations by @carlini in https://github.com/carlini/equational_theories. All of them are magmas over Z/nZ with a polynomial of degree ≤2 as the operations.

A bit of engineering was needed to get the file size and processing down:

Having one theorem per non-implication would produce huge files (100MBs), that seems pointless. So as suggested by Vlad Tsyrklevich this defines a compact syntax for “facts about a given magma”:
```
Facts G [1, 2] [4, 5]
```
where the lists are of course much longer. This expands to
```
Equation1 G ∧ Equation2 G ∧ ¬ Equation4 G ∧ ¬ Equation5 G
```
Presumably the code that scrapes the lean files to generate graphs etc can make use of that information. See https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Efficent.20representation.20of.20refutations for a discussion.
A decides! tactic is used that
- Applies And.intro first, as otherwise the type class inference blows up, it seems.
- Doesn’t check whether decides P will succeed, and simply sends it to the kernel. Not checking it twice half the processing times.
Actually, a decideFin! tactic is used that replaces type class inference with metacode constructing the instance. This yields about 2,5× speedup, leaving the kernel type checking as the bottleneck.

Some of these files are rather slow to process. To speed things up we could be smarter in which magmas and which equations we are actually be interested in. And maybe using native_decide can help (if that’s acceptable for this project), we’ll see.

For now, until we know better what to actually run, I excluded all magmas with 5 or more elements, just to keep this PR sizable.

Things that should happen in the repo before this can be merged:

[ ] This adds some common files (definition of Magma and of the equations). These should be put in a more central place.

Things that still need to happen in this PR:

[ ] Include the actual scripts from https://github.com/carlini/equational_theories and add some documentation
[x] Include the generated files (once small enough), marked as autogenerated in .gitattributes

teorth / equational_theories

Massive generation of refutations via polynomials over Z/nZ #19