Visualizing the diagram of implications

Stream: Equational

[Anand Rao Tadipatri]

I've written a prototype of a widget that renders the diagram of implications within the Lean infoview using vis.js:
image.png
image.png
The PR is here, and depends on an open PR by @David Renshaw.

The diagram can be rendered by running the command #display_implications defined in the file equational_theories/Visualization.lean.

Any suggestions and feedback are welcome.

[Edward van de Meent]

I think it will be useful to have the following available:

• display only the nodes that transitively imply the provided node
• display only the nodes that the provided node transitively implies
• the above, but add the neighbours in reverse direction for one step (if possible in a different color). Disproving that the provided node resp. implies or is implied by these nodes, should be sufficient to prove that the node is complete...

[Edward van de Meent]

I.e. I think the above is the minimal set of implications you need to disprove to be able to claim all implications that exist are proven?

[Edward van de Meent]

(and if possible it might be nice to have a command with a code-action that suggests all of these proof_wanted implications)

[Edward van de Meent]

I just realised that the algorithm I described is not quite right; it only works when the graph is reduced to be acyclic (in the directional sense), which might be a good idea to have nonetheless

[Amir Livne Bar-on]

There's value in formalizing the idea of equivalent laws, it helps with these analyses but also helps reduce the space for automatic runs