The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 11/13/21 8:06 PM, Talia Ringer wrote:
> If you do, I'd love examples!!! This idea is like a couple of hours old, 
> but I want to write it up with some examples so I can get a sense of how 
> tractable it is, and probably propose it to some students next year.

This is a very cool topic.  I've been looking at it on and off for a while in 
the context of Alectryon (you can see some examples at the end of 
https://pit-claudel.fr/clement/papers/alectryon-SLE20.pdf ).

As I see it there are two fairly different kinds of visualizations you may 
want from your proof assistant: one is an instantaneous "show me concrete 
examples of this goal".  So if I'm trying to prove 
    right_triangle(a, b, c) /\ sorted [d(a, b);d(b, c);d(c, a)] -> 
    d(c, a)^2 = d(a, b)^2 + d(b, c)^2
then I may want to generate diagrams of triangles that show me that relation 
on triangles with concrete edge sizes.  This is the kind of stuff that 
Penrose is good for, IIUC (http://penrose.ink/siggraph20.html)

This first use case is a bit like a visual quickchick.

But then there's a completely different use case, which is drawing a figure 
that fully captures the generality of your goal.  You may want to print a 
math formula with proper mathematical notations, for example; or maybe you 
want to render a separation logic formula as a graph of objects and memory 
locations.

(You can see a very very unpolished prototype of the latter one at 
https://people.csail.mit.edu/cpitcla/links/2020-10-sepview/LiterateQueue.html 
: use the "windowed" style and use Ctrl+down arrow to step through the proof 
steps; the pre- and post-conditions of the programs are presented as graphs 
instead of separation logic formulae).

Tools like Penrose are not fully suited for that second problem, because in 
general they don't guarantee "uniform continuity" of the diagrams, in the 
sense that small modifications of the inputs (goals) can yield large changes 
of the output (visualization).  This is a problem because in this second use 
case you typically want to show the way the visualization evolves as proof 
steps are taken, so generating a completely new visualization is very 
detrimental (it will completely confuse the user).

There are some descriptions of stuff I'd like to do in that realm on my "for 
students" page at https://pit-claudel.fr/clement/prospective-students.html, 
specifically the 
https://pit-claudel.fr/clement/prospective-students.html#domain-specific-proof-visualizations
 section and the 
https://pit-claudel.fr/clement/prospective-students.html#mixed-rendering-for-proof-presentation
 section

Also worth mentioning is the work the Lean folks are doing exploring all sort 
of cool visualizations with widgets (unfortunately the paper at 
https://drops.dagstuhl.de/opus/volltexte/2021/13899/pdf/LIPIcs-ITP-2021-4.pdf 
is a bit light on pictures).

Clément.