[DO NOT MERGE] Deep-embed graph

[alxest]

Hi all! Thank you for initiating this extremely exciting project. This PR is my attempt to simplify & give more principled approach to maintain the implication graph.

[Syntactic data] Each axiom (equation) is now has a concrete, syntactic term, named Equation type. A graph, Graph type, is defined as Equation -> Equation -> Status where Status denotes the current state for the corresponding edge. For example, a concrete instance for the subgraph of our interest is given as a term subgraph: Graph.

[Semantic interpretation] The validity of this graph object is enforced with Graph.valid definition - e.g., subgraph_valid would be the final theorem for the subgraph. The Graph.valid requires corresponding semantic proof for each syntactic edges. Notably, Edge is defined with typeclass and has few benefits below.

Benefits are as follows:

• Compared to doing metaprogramming (with Python script or lean) to (re)construct the graph from the Lean code, deep-embedding the graph from the first place should be more direct, less error-prone, and robust.
• Smaller TCB: the final theorem like subgraph_valid ensures the correctness of the whole graph (that is to be extracted and processed by tools like image-generators later) inside Lean.
• Simplification: (1) the repeated (G: Type*) [Magma G] for each theorem is now omitted, and (2) we don't have to give explicit names to theorems thanks to typeclass mechanism. (e.g., instance : (Edge true .e2 .e4) where instead of theorem Equation2_implies_Equation4 (G: Type*) [Magma G] (h: Equation2 G) : Equation4 G :=)
• Edge Synthesis: see Edge.trans_true, Edge.abduct_false0 and Edge.abduct_false1: the typeclass mechanism allows us to nicely derive some facts from existing facts. This is tested in the code.

One caveat would be performance scalability issue, especially for the final theorem (like subgraph_valid). If typeclass resolution mechanism takes O(n) (where n is the number of instances), it would take prohibitively long. If it takes O(log n), it should (I think) compile in time.

If you find this useful, I can make it a mergeable state quickly.

[teorth]

I like this idea but it needs to be coordinated with #36 , perhaps one can discuss it on the Lean Zulip thread https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Syntax ?