Infrastructure for large counterexamples

Stream: Equational

[Joachim Breitner]

I created a PR with some infrastructure for proving a large number of properties for Fin n-based magmas, extracted from the PR with the many counter examples. I thought I’d highlight it here so that interested parties know about the existence of these tools:

https://github.com/teorth/equational_theories/pull/110

• The Facts G [1,2] [3,4] syntax to concisely and efficiently state
  that G satisfies Equation1 and Equation2, but not Equation3 and
  Equation4

  There is also a crude calculate_facts command that takes a magma
  and an instance and a tactic and lists those for which the tactic
  succeeds.

• The decideFin! tactic that is a bit like decide but simply
  believes that the statement is true, so that the check only happens by
  the kernel, and uses custom code to construct the Decidable instance
  for the kind of theorems we actually encounter, to avoid the (slow)
  type inference.

• The memoFinOp elaborator that take a function
  Fin n → Fin n → Fin n, tabulates it, encodes this table in a single
  number and implements the lookup based on that. Presumably that's more
  compact and faster to evaluate by decide than other forms (array
  indexing, polynomials etc.)

It also includes, more as a demo, an exhaustive Facts statement for three Fin 2-based magmas, so that’s a fair number of antiimplications already right there

[Joachim Breitner]

CI is happy. Do people want to review/comment on this, or should I just merge :-)

Maybe someone has a better name instead of Facts?

[Joachim Breitner]

@David Renshaw Once this is in it would be good if the attribute from #93 will understand theorems of the form

theorem Magma2a.Facts : ∃ (G : Type) (_ : Magma G), Facts G [1,2,3] [4,5,6]

although now that I write this, this will appear as

theorem Magma2a.Facts : ∃ (G : Type) (_ : Magma G), Equation1 G ∧ Equation2 G ∧ ¬ Equation3 G ∧ ¬ Equation4 G

in the environment (because Facts is an elaborator), so that’s what the attribute would have look for, a mild generalization of what you already do.

[David Renshaw]

should be straightforward

[David Renshaw]

... and should be a separate PR from equational#93. :)

[Terence Tao]

One could possibly use G.satisfies [1,2,3] [4,5,6] instead of Facts G [1,2,3] [4,5,6]

[Joachim Breitner]

Hmm, it's an elaborator, not a normal function, so probably easier starting with a keyword.

[Terence Tao]

I guess Facts is fine. One could try for some pseudo-English such as G satisfies [1,2,3] not [4,5,6] but that also reads weirdly

[Terence Tao]

Another option is G ⊧ [1,2,3] \ [4,5,6] which is pseudo-model theory notation

[Joachim Breitner]

I guess we can start with Facts and change later when we are so inclined