Draft book using Lean for CS Discrete Math

Stream: new members

[Kevin Sullivan]

Hi everyone, Happy to find this forum. I'm Kevin Sullivan, University of Virginia CS. I've been using Coq, and now Lean, and also Dafny, in teach graduate and undergraduate students, for several years. I'm ramping up the role of Lean. I haven't been a Lean dev, and so am likely to have some questions, concerns, comments, etc. about aspects of Lean that impinge on pedagogy. Very best wishes and thanks to all. --Kevin

[Andrew Ashworth]

Wahoowa! Welcome!

[Johan Commelin]

Welcome!

[Kevin Buzzard]

Hi Kevin -- I'm Kevin Buzzard, a pure mathematician at Imperial College London. This autumn I'll be using Lean as part of my undergraduate mathematics teaching, in my introduction to proof course. As you can imagine I'm also very much interested in aspects of Lean that impinge on pedagogy. I hope to spend some time this summer making some good teaching materials for mathematicians; I currently have a bunch of stuff scattered around, and a bunch of ideas, but it seriously needs collating. One year ago I knew absolutely nothing about Coq or Lean or anything; I was just starting. I'm blogging as I learn at xenaproject.wordpress.com .

[Kenny Lau]

Hi Kevin -- I'm Kevin

[Mario Carneiro]

https://www.theonion.com/report-u-s-still-leads-world-with-highest-density-of-1819576406

[Scott Morrison]

Welcome Kevin! It's great to see more and more people using Lean in teaching. I'm Scott Morrison, a pure mathematician at the Australian National University. I'm not at all at the scale Kevin B is at yet, but I do have 3 maths undergraduates doing semester long projects with me at the moment in Lean, and I'm hoping to incorporate Lean in a larger way soon.

[Patrick Massot]

Maybe one day we will have a teaching stream here. I'll also experiment on real students during the spring term. I'll try to teach them how to write traditional maths proofs on paper after convincing Lean.

[Rob Lewis]

Yeah, there are quite a few people who have taught using Lean or who are planning to. Jeremy Avigad and I taught a intro math course at CMU; I'll be adapting that and teaching to a CS audience this winter. @Johannes Hölzl and our boss are teaching Lean in a more advanced CS course this fall.

[Rob Lewis]

Just to advertise a bit :wink: I'm hoping to make this a topic of discussion at our January workshop: https://lean-forward.github.io/lean-together/2019/index.html

[Kevin Sullivan]

(deleted)

[Kevin Sullivan]

Just to advertise a bit :wink: I'm hoping to make this a topic of discussion at our January workshop: https://lean-forward.github.io/lean-together/2019/index.html

Here's where we're posting notes / draft book on this stuff for my discrete math class. We've got a draft of all of it, and are pushing chapters to this site for the students as we get them edited. https://kevinsullivan.github.io/cs-dm-dev/. Comments welcome.

[Patrick Massot]

We now know for sure that no one will ever find integers, a, b, c, and n, where n > 2, such that a^n + b^n = c^n.

Hum...

[Patrick Massot]

And why don't you use mathjax instead of images?

[Patrick Massot]

and why is section 1.4 called Automated reasoning? Do you have a tactic I don't have?

[Patrick Massot]

@Kevin Sullivan Do you know whether your students managed to install Lean on Windows following your appendix?

[Kevin Buzzard]

We now know for sure that no one will ever find integers, a, b, c, and n, where n > 2, such that a^n + b^n = c^n.

Hum...

Maybe you should stick to positive integers here -- but even so, I don't think anyone formalised the proof yet ;-)

[Patrick Massot]

This time I did it. I created a stream "Lean for teaching". Click and subscribe!

[Moses Schönfinkel]

An excellent read! I was thinking of trying to push Lean (and really, even this kind of course, as we only have "logic") on my uni so I've taken a peek at your work. I have a few observations.
In 2.1.6.1.
a) The error that contains "already has an object named ‘x’" is, imho, more aching to what would happen in an imperative language if you tried to define a second function with the same name (and same parameters if we consider overloading), which is also disallowed - and you get an error that resembles the one of Lean, something along the lines of "redefinition of x". In Lean, this doesn't quite talk about attempting to somehow assign a new value to the same variable or some such - note that your example there contains the keyword def twice, the second one is therefore not even attempting to do some kind of would-be assignment; for that you would have a hypothetical def x := 5 followed by x := 6, note the lack of def.
In 2.2.4.
a) Just malformed math environment.
In 2.3.
a) The chapter rises a question that should be addressed briefly therein - why isn't every programming language typed then. You do say "type checking does constrain the programmer to produce type-correct code", but I find this a bit vague. While I have yet to hear a convincing argument anyway, the one that has yet not been completely debunked is that occasionally, types can potentially reject programs that would work correctly - good examples are various numeric type conversions, which leads me to:
b) "They are also strongly typed, which means that all type errors are detected". Weakly typed systems also detect all type errors! :) It's more about their attitude towards what constitutes a type error.
In 2.4.
a) Given the very introduction to this chapter talks about what are essentially extensional / intentional points of views on functions, there is very little mentioned about this thereafter - I see 2.4.4. tries, but perhaps an example of how the axiom of functional extensionality loses the computational information would be beneficial; e.g. just because ''normal'' matrix multiplication and Strassen both do the same thing does not mean they are the same algorithm / function.
In 2.4.5.
a) You've already talked a bit how functions are essentially sets of pairs, might be worth using this fact to reinforce the idea that "functions are just values".
b) Have I missed something - there's no notion of currying (schoenfinkeling, should i say :)!) and partial application anywhere? This would also help with this concept of returning functions / using them as arguments, as a -> b -> c = a -> (b -> c) and then (a -> b) -> c is something completely different.

[Kevin Sullivan]

Kevin Sullivan Do you know whether your students managed to install Lean on Windows following your appendix?

Yes, they did.

[Kevin Sullivan]

We now know for sure that no one will ever find integers, a, b, c, and n, where n > 2, such that a^n + b^n = c^n.

Hum...

We'll take another look at that! :)

[Kevin Sullivan]

An excellent read! I was thinking of trying to push Lean (and really, even this kind of course, as we only have "logic") on my uni so I've taken a peek at your work. I have a few observations.
In 2.1.6.1.
a) The error that contains "already has an object named ‘x’" is, imho, more aching to what would happen in an imperative language if you tried to define a second function with the same name (and same parameters if we consider overloading), which is also disallowed - and you get an error that resembles the one of Lean, something along the lines of "redefinition of x". In Lean, this doesn't quite talk about attempting to somehow assign a new value to the same variable or some such - note that your example there contains the keyword def twice, the second one is therefore not even attempting to do some kind of would-be assignment; for that you would have a hypothetical def x := 5 followed by x := 6, note the lack of def.
In 2.2.4.
a) Just malformed math environment.
In 2.3.
a) The chapter rises a question that should be addressed briefly therein - why isn't every programming language typed then. You do say "type checking does constrain the programmer to produce type-correct code", but I find this a bit vague. While I have yet to hear a convincing argument anyway, the one that has yet not been completely debunked is that occasionally, types can potentially reject programs that would work correctly - good examples are various numeric type conversions, which leads me to:
b) "They are also strongly typed, which means that all type errors are detected". Weakly typed systems also detect all type errors! :) It's more about their attitude towards what constitutes a type error.
In 2.4.
a) Given the very introduction to this chapter talks about what are essentially extensional / intentional points of views on functions, there is very little mentioned about this thereafter - I see 2.4.4. tries, but perhaps an example of how the axiom of functional extensionality loses the computational information would be beneficial; e.g. just because ''normal'' matrix multiplication and Strassen both do the same thing does not mean they are the same algorithm / function.
In 2.4.5.
a) You've already talked a bit how functions are essentially sets of pairs, might be worth using this fact to reinforce the idea that "functions are just values".
b) Have I missed something - there's no notion of currying (schoenfinkeling, should i say :)!) and partial application anywhere? This would also help with this concept of returning functions / using them as arguments, as a -> b -> c = a -> (b -> c) and then (a -> b) -> c is something completely different.

Moses,

Thank you very much for these comments. I will process them shortly and make some mods to the draft. It's still in somewhat rough shape as you can see. There's plenty of room for improvement, and I will take your comments to heart (and start a list of acks for people who send helpful suggestions and corrections). Very busy with some other stuff at the moment, but will get back to this shortly. Thank you again and kind regards,

Kevin

[Kevin Sullivan]

And why don't you use mathjax instead of images?

The aim is to produce both HTML and LaTeX from the same source. Maybe mathjax would work. It's clear that the typography needs to be improved throughout. We borrowed (with thanks and acks) Jeremy Avigad's technology for generating HTML+LaTeX. So it's partly just the legacy issue. We'll take a look at alternatives at some point.

[Patrick Massot]

mathjax certainly won't prevent you from getting HTML+LaTeX from the same source, it's quite the contrary. I don't understand how you can blame Jeremy. https://leanprover.github.io/logic_and_proof certainly uses mathjax

[Kevin Sullivan]

mathjax certainly won't prevent you from getting HTML+LaTeX from the same source, it's quite the contrary. I don't understand how you can blame Jeremy. https://leanprover.github.io/logic_and_proof certainly uses mathjax

Ok,, we'll take another look. Clearly needs fixing. Apologies to Jeremy. Will fix when time permits. Right now fairly slammed getting context edited and out to my students.

[Moses Schönfinkel]

I finally had the time to go over 3. Observations are for the most part just nitpicks.
In 3.4.(6) is missing?
a) Formalization of false' is simply inductive false' : Prop, then I guess example : false' ↔ false := iff.intro (λcontra : false', contra.cases_on _) (λcontra : false, contra.cases_on _) is pertinent there.
In 3.5.6
a) example : true' ↔ true := iff.intro (λh : true', true.intro) (λh : true, true'.intro) could be handy here
In 3.6.3.2.
a) I may have missed some previous occurences but it appears that here is the first time you curry a function (sumOfSqaures) - this "works" in combination with my previous comment 2.4.5/b
In 3.7.4.
a) Hahah, there really appears to be no mp in core Lean; I guess function application is enough :). Anyway, in your example you provide two interpretations, written in different styles. You "missed" my absolute favourite ones, once again have to do with currying: def arrow_elim' { P Q : Prop } (pimpq: P -> Q) : (P -> Q) := pimpq- note that the parens around the return (P -> Q) are redundant, but under this particular interpretation, it's clear that this thing is really just identity, so then this follows: def arrow_elim'' { P Q : Prop } : forall (pimpq : P -> Q), forall p : P, Q := id where the proof itself is just id! (Lean can figure out that this is the identity for (P -> Q), or you could even be explicit and say := @id (P -> Q). Furthermore, might be worth noting this is basically Haskell's ($) :: (a -> b) -> a -> b, which Lean has too, but I believe it's some baked-in syntax in Lean because of... reasons. (You can't do #check ($) in Lean).
In 3.7.5.
a) I would help with todo: give better example but I am not sure what exactly youre trying to demonstrate here :P
In 3.10.4.7.
a) altImplication should have implicit P Q
In 3.11.
a) It could be perhaps instructive to show that exists can be built from forall and by extension, show dependent pairs / Sigmas, as I believe I saw Pi being mentioned somewhere.

[Kevin Sullivan]

I finally had the time to go over 3. Observations are for the most part just nitpicks.
In 3.4.(6) is missing?
a) Formalization of false' is simply inductive false' : Prop, then I guess example : false' ↔ false := iff.intro (λcontra : false', contra.cases_on _) (λcontra : false, contra.cases_on _) is pertinent there.
In 3.5.6
a) example : true' ↔ true := iff.intro (λh : true', true.intro) (λh : true, true'.intro) could be handy here
In 3.6.3.2.
a) I may have missed some previous occurences but it appears that here is the first time you curry a function (sumOfSqaures) - this "works" in combination with my previous comment 2.4.5/b
In 3.7.4.
a) Hahah, there really appears to be no mp in core Lean; I guess function application is enough :). Anyway, in your example you provide two interpretations, written in different styles. You "missed" my absolute favourite ones, once again have to do with currying: def arrow_elim' { P Q : Prop } (pimpq: P -> Q) : (P -> Q) := pimpq- note that the parens around the return (P -> Q) are redundant, but under this particular interpretation, it's clear that this thing is really just identity, so then this follows: def arrow_elim'' { P Q : Prop } : forall (pimpq : P -> Q), forall p : P, Q := id where the proof itself is just id! (Lean can figure out that this is the identity for (P -> Q), or you could even be explicit and say := @id (P -> Q). Furthermore, might be worth noting this is basically Haskell's ($) :: (a -> b) -> a -> b, which Lean has too, but I believe it's some baked-in syntax in Lean because of... reasons. (You can't do #check ($) in Lean).
In 3.7.5.
a) I would help with todo: give better example but I am not sure what exactly youre trying to demonstrate here :P
In 3.10.4.7.
a) altImplication should have implicit P Q
In 3.11.
a) It could be perhaps instructive to show that exists can be built from forall and by extension, show dependent pairs / Sigmas, as I believe I saw Pi being mentioned somewhere.

These are terrific comments. Thank you very much. I'm tied up with another project but will come back to this in a few days. Very much appreciated. Thanks, again. More soon enough. -Kevin

[Kevin Sullivan]

(deleted)