Zulip Chat Archive

Stream: new members

Topic: learning path


Patrick Thomas (Feb 16 2019 at 23:26):

I was wondering if anyone might have advice on a learning path for getting to the point of being able to make useful contributions to the goal of easing the use of computer proof assistants like Lean. I have spent some time studying mathematical logic, primarily from "First Order Mathematical Logic" by Angelo Margaris, and I have started going through "Lectures on the Curry-Howard Isomorphism" by Morten Heine Sørensen and Pawel Urzyczyn (https://play.google.com/store/books/details?id=_mtnm-9KtbEC). In some respects there seems to be a bit of a catch-22 here, having the mathematics from these texts available in a fully formalized fashion would be an aid to understanding them, but first needing that understanding to formalize them or to understand their formalization. Nevertheless, I am making progress in these, but it is time consuming, so I would like to be sure that it is a good approach. I am also curious as to the kind of open problems in the field.

Kevin Buzzard (Feb 17 2019 at 00:38):

My strategy was : read Theorem Proving In Lean, think of some hard problems, try to solve them, get stuck, ask loads of questions here, and then people start realising where the true bottlenecks are

Simon Hudon (Feb 17 2019 at 00:38):

I do not specifically know those texts but that seems like a good approach. You have to be ok with things being slow at first

Patrick Thomas (Feb 17 2019 at 01:08):

@Kevin Buzzard Did you already know type theory and logic before you did so?

Patrick Thomas (Feb 17 2019 at 03:44):

Would it be useful, apart from my own learning, for me to try and formalize the latter book in Lean?

Andrew Ashworth (Feb 17 2019 at 05:27):

I don't think you need to know any of those if your goal is to "make Lean easier to use"

Andrew Ashworth (Feb 17 2019 at 05:30):

TBH if you're looking for a textbook Coq has way more mindshare at the moment, you may work through Software Foundations and some of the harder exercises in CPDT in Coq. At that point you're a year or two in and a whiz, and then you come back and pick up Lean since most things are similar...

Andrew Ashworth (Feb 17 2019 at 05:37):

I would say also most people don't use Lean/Coq to implement programs because specifying and proving program behavior is exceedingly tedious

Andrew Ashworth (Feb 17 2019 at 05:37):

unit tests in regular programming languages are already seen as a chore

Andrew Ashworth (Feb 17 2019 at 05:38):

anything which reduces the burden of writing proofs is ultimately what's needed; that means automatic proof search, better lemma and theorem search & autocomplete, code linting, etc etc etc

Andrew Ashworth (Feb 17 2019 at 05:39):

none of those things really require a back to front knowledge of type theory / curry-howard isomorphism / etc

Patrick Thomas (Feb 22 2019 at 08:11):

I have been hesitant to start learning Coq because it appears designed for backward reasoning with tactics, and I would like to create proofs with forward reasoning so that they are readable outside of the proof assistant. Can I use forward reasoning with Coq, or automatically convert tactic style proofs to term style proofs that are readable outside of Coq?

Moses Schönfinkel (Feb 22 2019 at 08:42):

Yes you can reason any way you see fit in both Coq and Lean. I wouldn't say either of the tools is designed for either of the options, although backwards reasoning if of some preference in mechanized environments simply because you don't end up cluttering your goals with redundant assumptions (as much).

Kevin Buzzard (Feb 22 2019 at 09:52):

I genuinely don't know why computer scientists seem to make so much fuss about forward v backward reasoning. This concept is never thought about in mathematics, a logical argument is a logical argument and who cares which order the steps go in. Can anyone enlighten me as to why this sort of thing seems to come up again and again in the CS community?

Mario Carneiro (Feb 22 2019 at 09:57):

I think it's primarily because it is actually a difference between "natural proving style" on paper vs on the computer

Mario Carneiro (Feb 22 2019 at 09:57):

No one writes a paper proof with a list of "it suffices to show" statements

Mario Carneiro (Feb 22 2019 at 09:57):

it's hard to follow

Mario Carneiro (Feb 22 2019 at 09:58):

but in a computer proof it's generally easier and more structured to approach proofs like this, where the forward proving steps are the exception, not the norm

Mario Carneiro (Feb 22 2019 at 10:00):

From my experience I would say it's not "the computer scientists" making the fuss, it's the mathematicians who are expecting formal proofs to look like LaTeX paper proofs

Kevin Buzzard (Feb 22 2019 at 10:29):

But the reason that can't be right is that 99.9% of mathematicians have never even heard of the phrases "forward reasoning" and "backward reasoning" so we can't possibly be making a fuss about them :-)

Kevin Buzzard (Feb 22 2019 at 10:30):

We just reason.

Mario Carneiro (Feb 22 2019 at 10:30):

no but you know it when it's explained to you

Kevin Buzzard (Feb 22 2019 at 10:30):

Yes we do -- but then we wonder what the fuss is about :-)

Kevin Buzzard (Feb 22 2019 at 10:31):

I say again -- why does this question even matter? We have "thus" and we have "it suffices to prove that"

Kevin Buzzard (Feb 22 2019 at 10:31):

and they can go in any order. And we, as far as I know, attach no special importance to this. They're just different ways of making progress.

Kevin Buzzard (Feb 22 2019 at 10:31):

But for some reason this is an issue in CS.

Mario Carneiro (Feb 22 2019 at 10:31):

It's a style question. Like I said, if you saw someone prove an entire proof using "it suffices to prove" (I mean like 10+ uses of this), it would be disorientating

Mario Carneiro (Feb 22 2019 at 10:32):

even though it's clearly how you come to proofs quite often

Kevin Buzzard (Feb 22 2019 at 10:32):

On the other hand, you might claim you're doing backwards reasoning but when I see 3000+ line files like multiset.lean consisting of lemma after lemma after lemma with three-line proofs, you're doing forward reasoning really.

Mario Carneiro (Feb 22 2019 at 10:32):

for some reason the usual style of presentation prefers the "rabbit out of a hat" kind of steps

Kevin Buzzard (Feb 22 2019 at 10:32):

That's what you write with your short lemmas -- your preferred style.

Mario Carneiro (Feb 22 2019 at 10:33):

Actually I'm writing closer to "mathematical order" there. It's backward reasoning, but I write in reverse order so it comes out looking like forward proof order

Mario Carneiro (Feb 22 2019 at 10:33):

which is also what I do when composing paper proofs

Kevin Buzzard (Feb 22 2019 at 10:33):

Your backwards / forwards reasoning discussion seems to be going on at a micro-level -- within the proof of one lemma. If you wrote all the lemmas backwards in multiset.lean it wouldn't compile.

Mario Carneiro (Feb 22 2019 at 10:34):

I'm saying I write the last lemma first, and work backwards, typing upward in the file

Mario Carneiro (Feb 22 2019 at 10:34):

in the end it looks like I wrote in forward order

Kevin Buzzard (Feb 22 2019 at 10:34):

I think it might be a lemma v theorem thing. We prove theorems forwards and you prove lemmas backwards, and then we say we do things in different order. But we don't give the proofs of lemmas because they're trivial, and you prove lemmas in the right order, so we're both doing things the same way really, but focussing on different aspects.

Mario Carneiro (Feb 22 2019 at 10:35):

I only prove lemmas in textual order if I happen to be sufficiently forward thinking to predict the lemmas in advance

Kevin Buzzard (Feb 22 2019 at 10:36):

Whereas we don't prove them at all, because the fact that you can do induction on multisets is trivial.

Mario Carneiro (Feb 22 2019 at 10:36):

No, you have lemmas too, they are just at a different level

Kevin Buzzard (Feb 22 2019 at 10:38):

Probably in real life (i.e. when I'm being a mathematician) I reason in a highly non-linear manner.

Patrick Thomas (Feb 23 2019 at 22:42):

"it's the mathematicians who are expecting formal proofs to look like LaTeX paper proofs". I think I fall into this category.

Kevin Buzzard (Feb 23 2019 at 22:42):

http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html Patrick's working on it.

Patrick Thomas (Feb 23 2019 at 22:46):

This has been generated automatically from a Lean proof?

Kevin Buzzard (Feb 23 2019 at 22:46):

Not really

Kevin Buzzard (Feb 23 2019 at 22:46):

It's been generated from a .lean file though

Patrick Thomas (Feb 23 2019 at 22:47):

Is there a link to that file, and more info on the project?

Kevin Buzzard (Feb 23 2019 at 22:48):

Check out the Lean + LaTeX? thread in #general

Kevin Sullivan (Feb 26 2019 at 19:13):

As a computer scientist and software engineering guy, I've come to the conclusion that the phrase, "backwards reasoning", is really not as clarifying as it could be. When we use (apply and.intro _ _), for example, to start a proof script, sure, we can think of "going backwards through the arrow to the premises", and all that. But a better way to think of what we've done is to give a complete proof term, defining the overall architecture of the proof, albeit with a few remaining holes still abstracted away. We then recursively fill the remaining "stubs" (aka holes) by applying the same method recursively.

In the software design and engineering field, this is known as top-down, structured programming. A better term might be top-down, type-guided refinement. But that I think is the right way to think about what's happening. A complete working proof is given modulo fleshing out of remaining stubs.
It's not really backwards, it's top-down. It's a great way to develop simple procedural or functional programs, and it's just as great a way to develop proofs. Nothing strange about it at all, if you see it as top-down, structured programming.

Patrick Thomas (Feb 28 2019 at 06:30):

I don't think of it as strange. It is just that to me the resulting proof seems hard to read and comprehend, especially outside of the IDE.


Last updated: Dec 20 2023 at 11:08 UTC