Software Foundations

Stream: general

[Simon Hudon]

@Kevin Buzzard I think a while back you were looking at Software Foundations using Lean. Did you write anything up?

[Kevin Buzzard]

I have got a work experience kid doing it for a week in July!

[Kevin Buzzard]

Goodness knows how far they'll get

[Simon Hudon]

Interesting! What is the scope of the project? Only writing up solutions in Lean or reformulating the parts of the book that are specifically about Lean?

[Kevin Buzzard]

It's one of my kids

[Kevin Buzzard]

so they'll just do what they want really

[Kevin Buzzard]

I'm just hoping to get them engaged with the material

[Kevin Buzzard]

because I know they'll like it

[Kevin Buzzard]

He's good at python

[Kevin Buzzard]

and I showed him that python had lambdas

[Kevin Buzzard]

and he got quite interested in them

[Simon Hudon]

Amazing :D How old is he?

[Kevin Buzzard]

16

[Kevin Buzzard]

wants to do computer science

[Simon Hudon]

How disappointed is the dad? :laughing:

[Simon Hudon]

One of my former undergraduate student is thinking of going through SF with Lean. Do you think that might help your son to have a studying buddy?

[Kenny Lau]

who is SF?

[Simon Hudon]

Software Foundations

[Kenny Lau]

aha

[Andrew Ashworth]

i think in general it might not be a bad idea to have a lean translation of SF

[Andrew Ashworth]

I'd volunteer to do 4-5 chapters if people were interested

[Simon Hudon]

That'd be great, that's true. I should probably pitch in too :D

[Andrew Ashworth]

great, you can take all the chapters that deal with tactics

[Andrew Ashworth]

haha

[Simon Hudon]

I would but then there would be nothing left for you to do!

[Andrew Ashworth]

don't forget SF is 3 books now... it's a big project

[Simon Hudon]

I'm wondering how different the result would be from SF

[Simon Hudon]

I would hope that change capitals for lower cases with an underscore in front be enough but we might have rewrite some sections significantly

[Andrew Ashworth]

^

[Andrew Ashworth]

yes, because i taught myself lean by doing sf in lean

[Andrew Ashworth]

and there are differences

[Andrew Ashworth]

unfortunately i didn't keep my solutions around...

[Kevin Buzzard]

I have solutions for some stuff, which I was going to let my son see if he was completely lost

[Andrew Ashworth]

cool. i'll take a look at setting up a github repo . SF is GPL licensed so I don't think there's any issue forking it and putting it online

[Simon Hudon]

I'm wondering if we could team up with the SF team. I don't know if they will keep updating SF but if they do, it would be great to be notified (automatically?) so that we can adjust the Lean version too

[Andrew Ashworth]

why does that need teaming up? you could just watch their github repo

[Simon Hudon]

is there actually a notification system for that?

[Simon Hudon]

Oh, yeah, ok I see. I guess we can register to get emails on commits to their repos

[Andrew Ashworth]

yeah, you can choose to receive notification emails

[Reid Barton]

I would hope that change capitals for lower cases with an underscore in front be enough

Don't forget to find-and-replace A to α as well

[Amin Bandali]

One of my former undergraduate student is thinking of going through SF with Lean. Do you think that might help your son to have a studying buddy?

Hi all, I'm the said former undergrad (now masters) student :simple_smile: I'm a Haske-holic coming to Lean and hope to do neat things with programming language semantics, and with system specs and models as well

[Andrew Ashworth]

nice. I got started on translating the first chapter of sf, basics. Everything up to chapter 11 seems pretty straightforward

[Andrew Ashworth]

that said, even though it's straightforward, it's still work. actually, I've been spending most of my time figuring out how the sphinx documentation workflow works

[Andrew Ashworth]

i'll have more time to devote to this after thursday

[Simon Hudon]

Let me know when you decide to show it

[Kevin Buzzard]

So my son will start from book 1 p1 because he's learning the entire theory from nothing but a background of python.

[Kevin Buzzard]

But I'm independently interested in any sphinx tips because I want to write something about Lean for mathematicians at some point and I am still not 100% clear on the format this should take -- at the minute I am tempted to just copy TPIL but my concern is that I don't know how to display LaTeX within that set-up. Is this possible?

[Johan Commelin]

What kind of LaTeX do you want to use? Merely "equations"? Or also other fancy typesetting, like diagrams?

[Adam Kurkiewicz]

Hey guys, I'm working through software foundations lists chapter:
https://softwarefoundations.cis.upenn.edu/current/lf-current/Lists.html#lab60

After some fairly mindless pattern-matching I was able to implement a function, which can compute a sum of a list of natural numbers, and I think it basically works, but a few things seem strange:

1. I had to use meta in front of list_sum. I suspect this is something to do with recursion not necessarily being well-defined, but my PL knowledge + understanding of lean are a bit lacking, so not _really_ sure why. Any idea how to do it without meta?
2. There's a weird thing inside the recursor inside list_sum, I've called it "what_is_this_for". I thought I was producing a term of type nat, not of type nat → nat, but lean disagrees. Any idea why?

inductive natlist : Type
    | nil : natlist
    | cons : nat → natlist → natlist

meta definition list_sum : natlist → nat :=
    λ list : natlist,
    natlist.rec_on list 0 (λ list_element : nat, λ previous_list : natlist, λ what_is_this_for: nat, list_element + (list_sum previous_list))

open natlist

#reduce list_sum $ cons 2 $ cons 2 nil

#eval list_sum $ cons 4 $ cons 3 $ cons 2 nil

[Mario Carneiro]

What you called what_is_this_for is the inductive hypothesis

[Mario Carneiro]

you should use it in place of list_sum previous_list

[Mario Carneiro]

and then it won't need to be meta

[Mario Carneiro]

Or you can just use the equation compiler instead of the recursor, and then you can make reference to the function you are defining and lean automatically compiles it to recursors

[Adam Kurkiewicz]

Of course! Thank you Mario, in hindsight this is super-obvious (I think you've actually explained this to me last year in Cambridge).

[Sean Leather]

Here's an alternative definition:

def natlist.sum : natlist → ℕ :=
natlist.rec 0 (λ (n : ℕ) (nl : natlist) (ih : ℕ), n + ih)

[Sean Leather]

It's definitely easier to use the equation compiler, though. :simple_smile:

[Adam Kurkiewicz]

I should definitely learn to use the equation compiler, thanks guys!