Zulip Chat Archive

Stream: general

Topic: Software Foundations


Simon Hudon (May 01 2018 at 19:37):

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

Kevin Buzzard (May 01 2018 at 19:38):

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

Kevin Buzzard (May 01 2018 at 19:38):

Goodness knows how far they'll get

Simon Hudon (May 01 2018 at 19:42):

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 (May 01 2018 at 19:42):

It's one of my kids

Kevin Buzzard (May 01 2018 at 19:42):

so they'll just do what they want really

Kevin Buzzard (May 01 2018 at 19:43):

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

Kevin Buzzard (May 01 2018 at 19:43):

because I know they'll like it

Kevin Buzzard (May 01 2018 at 19:43):

He's good at python

Kevin Buzzard (May 01 2018 at 19:43):

and I showed him that python had lambdas

Kevin Buzzard (May 01 2018 at 19:43):

and he got quite interested in them

Simon Hudon (May 01 2018 at 19:43):

Amazing :D How old is he?

Kevin Buzzard (May 01 2018 at 19:57):

16

Kevin Buzzard (May 01 2018 at 19:57):

wants to do computer science

Simon Hudon (May 01 2018 at 19:57):

How disappointed is the dad? :laughing:

Simon Hudon (May 01 2018 at 21:15):

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 (May 01 2018 at 21:15):

who is SF?

Simon Hudon (May 01 2018 at 21:22):

Software Foundations

Kenny Lau (May 01 2018 at 21:22):

aha

Andrew Ashworth (May 01 2018 at 21:27):

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

Andrew Ashworth (May 01 2018 at 21:27):

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

Simon Hudon (May 01 2018 at 21:28):

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

Andrew Ashworth (May 01 2018 at 21:28):

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

Andrew Ashworth (May 01 2018 at 21:28):

haha

Simon Hudon (May 01 2018 at 21:30):

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

Andrew Ashworth (May 01 2018 at 21:30):

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

Simon Hudon (May 01 2018 at 21:30):

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

Simon Hudon (May 01 2018 at 21:31):

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 (May 01 2018 at 21:36):

^

Andrew Ashworth (May 01 2018 at 21:36):

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

Andrew Ashworth (May 01 2018 at 21:36):

and there are differences

Andrew Ashworth (May 01 2018 at 21:36):

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

Kevin Buzzard (May 01 2018 at 22:02):

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

Andrew Ashworth (May 01 2018 at 22:13):

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 (May 01 2018 at 22:15):

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 (May 01 2018 at 22:18):

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

Simon Hudon (May 01 2018 at 22:19):

is there actually a notification system for that?

Simon Hudon (May 01 2018 at 22:20):

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

Andrew Ashworth (May 01 2018 at 22:20):

yeah, you can choose to receive notification emails

Reid Barton (May 02 2018 at 03:07):

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 (May 02 2018 at 03:15):

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 (May 02 2018 at 03:50):

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

Andrew Ashworth (May 02 2018 at 03:50):

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 (May 02 2018 at 03:51):

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

Simon Hudon (May 02 2018 at 04:08):

Let me know when you decide to show it

Kevin Buzzard (May 02 2018 at 06:58):

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 (May 02 2018 at 07:00):

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 (May 02 2018 at 07:25):

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

Adam Kurkiewicz (Jul 03 2018 at 12:45):

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 (Jul 03 2018 at 12:51):

What you called what_is_this_for is the inductive hypothesis

Mario Carneiro (Jul 03 2018 at 12:51):

you should use it in place of list_sum previous_list

Mario Carneiro (Jul 03 2018 at 12:51):

and then it won't need to be meta

Mario Carneiro (Jul 03 2018 at 12:52):

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 (Jul 03 2018 at 12:56):

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 (Jul 03 2018 at 12:57):

Here's an alternative definition:

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

Sean Leather (Jul 03 2018 at 12:58):

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

Adam Kurkiewicz (Jul 03 2018 at 12:58):

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


Last updated: Dec 20 2023 at 11:08 UTC