Lean, Coq and other proof assistants: Visualising proofs as trees

#1

Post by lakesare » Wed, Sep 20, 2023, 11:48 AM UTC

This is my overview of proof visualisation tools among all modern proof assistants.

If you're aware of any tools I might have missed, please @ me in the comments. I aimed to cover every one I could find.

Lean, Coq and other proof assistants: Visualising proofs as trees
lakesare.brick.do

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#2

Post by [deleted] » Wed, Sep 20, 2023, 11:48 AM UTC

[deleted]

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#3

Post by Reubend » Thu, Sep 21, 2023, 9:52 PM UTC

Thanks for posting this. As a beginner, do I need to already know what "sequent-calculus-style trees" are for this to be useful?

I didn't see any broad explanation of what the tree structure means here. I can see that disjunctions split a branch into 2 branches, but I'm still pretty confused overall.

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#4

Post by nathell » Thu, Sep 21, 2023, 9:58 PM UTC

Reminds me of Leslie Lamport’s „How to Write a Proof” [1]. I wonder whether there exist tools that aid in manually writing visualisable proofs?

https://lamport.azurewebsites.net/pubs/lamport-how-to-write....

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#5

Post by tunesmith » Thu, Sep 21, 2023, 10:16 PM UTC

Well, I think a DAG would generally be better than a tree for visually representing a proof. Because a premise can support multiple lemmas.

One site I've been working on uses graphs to generate arguments in that fashion:

http://concludia.org/

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#6

Post by lakesare » Thu, Sep 21, 2023, 10:18 PM UTC

Reubend wrote: post #3

Thanks for posting this. As a beginner, do I need to already know what "sequent-calculus-style trees" are for this to be useful? I didn't see any broad explanation of what the tree structure means here. I can see that disjunctions split a branch into 2 branches, but I'm still pretty confused overall.

It isn't necessary to know theory for these visualisations to be useful, both Traf and Paperproof (and sequence calculus trees!) should, ideally, just reflect what's already happening in your mental image while you're writing a Lean/Coq/on-paper mathematical proof. But I agree it warrants a tutorial/explanation, got to write it. I think it might be particularly unclear what's happening if you're just looking at the full tree of the already-proved-theorem. As we're writing the proof, hypothesis nodes (green, what we have) move down; and goal nodes (red, what we want to have) move up. So it kind of goes from both sides to the center, and you should read it "from both sides to the center", takes getting used to. Here is a video of what's happening in Paperproof as we're writing the proof e.g.: https://www.youtube.com/watch?v=0dVj4ITAF1o.

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#7

Post by cobbal » Thu, Sep 21, 2023, 10:25 PM UTC

Reubend wrote: post #3

Thanks for posting this. As a beginner, do I need to already know what "sequent-calculus-style trees" are for this to be useful? I didn't see any broad explanation of what the tree structure means here. I can see that disjunctions split a branch into 2 branches, but I'm still pretty confused overall.

Some searching found http://logitext.mit.edu/tutorial . It tries to explain sequent calculus with an interactive gui prover. Not sure how approachable it is... I've gotten too used to these things to know how to explain them properly.

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#8

Post by mjfl » Thu, Sep 21, 2023, 10:28 PM UTC

What is it with proof assistant designers and terrible naming instincts? "Lean" as a name collides with all sorts of business/engineering productivity frameworks "Lean software development", "lean business management", "running a lean startup". And of course Coq is phallic both in English and the original French. It must be the case that the people that design these things live in a separate plane of existence where these things don't bother them.

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#9

Post by [deleted] » Thu, Sep 21, 2023, 10:29 PM UTC

mjfl wrote: post #8

What is it with proof assistant designers and terrible naming instincts? "Lean" as a name collides with all sorts of business/engineering productivity frameworks "Lean software development", "lean business management", "running a lean startup". And of course Coq is phallic both in English and the original French. It must be the case that the people that design these things live in a separate plane of existence where…

[deleted]

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#10

Post by lakesare » Thu, Sep 21, 2023, 10:56 PM UTC

tunesmith wrote: post #5

Well, I think a DAG would generally be better than a tree for visually representing a proof. Because a premise can support multiple lemmas. One site I've been working on uses graphs to generate arguments in that fashion: http://concludia.org/

That's correct, in fact we would have a DAG if we displayed all possible arrows, but we conceal it to make the UI easier to interact with for the user. Hypotheses (green nodes) form many little trees, and goals (red trees) form a single tree. These must be trees, and not lattices, because that's just how Lean and Coq tactics work. However, tactics make use of hypotheses, and these can be displayed as arrows that connect hypotheses and goals, making it, in this sense, a DAG (here is an example, I moved the nodes a bit to make the arrows obvious https://github.com/Paper-Proof/paperproof/issues/9#issuecomm...). Concludia looks interesting, does it support first-order logic/ORs?