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…
Lean, Coq and other proof assistants: Visualising proofs as trees
11–20 of 33 posts
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#12What 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…
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#13Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#14Thanks 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.
Sometimes the trees are upside down from this, for reasons I haven't been able to divine. Some logics also permit multiple (alternative) conclusions in a judgment, which is then properly called a sequent.
Nearly the same notation is used for type judgements in type theory as well, with "assumptions ⊢ conclusion" being replaced by "environment ⊢ type assignments". [2]
[1] https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK (The preceding section introduces the notation but uses the upside-down variant, for unclear reasons -- I've rarely seen it elsewhere.)
[2] https://en.wikipedia.org/wiki/Type_theory#Technical_details
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#15Well, 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 conn…
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#16Reminds 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....
[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...
[2] https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-ref...
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#17What 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…
Relevant example: my current toy proof engine and language is called lesc. There are lots of things called "lesc", but none of them to my knowledge stand for Less Elegant Space Cowboy.
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#18Earlier quoted context omitted.
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 conn…
Propositional, so no exists or foralls, but yes for ORs and NOTs. Acyclic only.
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#19What 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…
I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#20What 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…