API: Create an API to handle Magma words, equations, and implications as syntactic objects

[teorth]

See the discussion in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Syntax . Among other things, this would allow one to prove "metatheorems" about equations, for instance that the equation "x = f(y,z,w)" is equivalent to "x=y" for any word f.

[franklindyer]

claim

[franklindyer]

propose PR #96

[teorth]

See also https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Equations.20vs.20Laws for further discussion

[franklindyer]

propose PR #122

See my proof of Equation332_implies_Equation43 for a proof-of-concept example of a duality argument. This is clearly still very awkward to write out, but hopefully with some more convenience functions like the ones in FiniteSatUtils.lean, this can get more pleasant to use.

I also have a question. For some reason, my proof doesn't type check with (G: Type*), only with (G: Type). I think this has something to do with how satisfaction is defined, or how my duality functions are defined, but I'm not clear on what the actual difference between Type and Type* is. Something about different type universes? Any idea how to fix this? And is there a reason we've chosen to write all of the implications in Subgraph.lean using G: Type* rather than G: Type?

[teorth]

I opened a separate request #186 for this. We've stated our implications to allow for the magma G to be "large" - not a member of the Level 0 universe, but potentially something from the Level 1 universe (e.g., a magma whose elements are arbitrary types in Level 0, and whose binary operation is, say, Cartesian product X → Y → X × Y). But it is unlikely that we would actually encounter higher type objects in our arguments, so we could perhaps just reduce to the Type 0 universe. On the other hand, the completeness theorem that is already proven should actually give us a way to pass back and forth between Level 0 and arbitrary level universes, so that may be the best long-term way to resolve the problem in case for some weird reason we do actually need to work with higher type objects at some point (and I think the Mathlib philosophy is to allow arbitrary level whenever possible).

[Shreyas4991]

@teorth : can we close this task closed given that we now have FreeMagma and MagmaLaw along with typical model theoretic properties lke soundness and completeness? If not then maybe a new task with narrower scope would reflect what still remains to be done.