Zulip Chat Archive
Stream: general
Topic: idly trying software foundations
Kevin Buzzard (Mar 27 2018 at 19:47):
I am working through software foundations. I'm finding the first book relatively straightforward, which is a relief. I was trying to do the exercises in a golf-like way. Why doesn't this work:
Kevin Buzzard (Mar 27 2018 at 19:48):
inductive ev : nat → Prop | ev_0 : ev 0 | ev_SS : ∀ n : nat, ev n → ev (n+2) open ev
Kevin Buzzard (Mar 27 2018 at 19:48):
theorem ev_plus4 : ∀ n, ev n → ev (n + 4) := λ _ _,ev_SS _ (ev_SS _ _)
Kevin Buzzard (Mar 27 2018 at 19:48):
I thought there was every chance :-)
Kevin Buzzard (Mar 27 2018 at 19:49):
but I get
Kevin Buzzard (Mar 27 2018 at 19:49):
don't know how to synthesize placeholder context: _x : ℕ, _x : ev _x ⊢ ev _x
Kenny Lau (Mar 27 2018 at 19:57):
what is software foundations?
Kevin Buzzard (Mar 27 2018 at 19:58):
a book on the web
Kevin Buzzard (Mar 27 2018 at 19:58):
https://softwarefoundations.cis.upenn.edu/
Kevin Buzzard (Mar 27 2018 at 19:59):
They have exercises like this:
Gabriel Ebner (Mar 27 2018 at 19:59):
You need to plug in the assumption for ev n somewhere.
Kevin Buzzard (Mar 27 2018 at 19:59):
definition double (n : ℕ) := n + n
theorem ev_double (n : ℕ) : ev (double n) := nat.rec_on n ev_0
(λ n H, have (n+1)+(n+1)=n+n+2,by simp,show ev((n+1)+(n+1)),by {rw this;exact ev_SS _ H})
Kevin Buzzard (Mar 27 2018 at 19:59):
I wanted the elaborator to guess where. I have it as an underscore
Gabriel Ebner (Mar 27 2018 at 20:00):
The underscores won't find it because it is not determined by unification.
Kevin Buzzard (Mar 27 2018 at 20:00):
I know that theorem ev_plus4 : ∀ n, ev n → ev (n + 4) := λ _ H,ev_SS _ (ev_SS _ H) works but I...basically I am trying to get a feeling for what I can get away with with underscores
Kenny Lau (Mar 27 2018 at 20:01):
it's the same reason #check λ n : nat, (rfl : _ + 4 = (_ + 2) + 2) fails, I think
Kenny Lau (Mar 27 2018 at 20:01):
(obviously it's n!!)
Gabriel Ebner (Mar 27 2018 at 20:01):
It could also be 0, or 1, or...
Sebastian Ullrich (Mar 27 2018 at 20:01):
Or n!! :smile:
Kevin Buzzard (Mar 27 2018 at 20:02):
but #check λ n : nat, (rfl : _ + 4 = (_ + 4)) works...
Gabriel Ebner (Mar 27 2018 at 20:02):
But I hope you get a metavariable and not n, right?
Sebastian Ullrich (Mar 27 2018 at 20:03):
Yes, because check allows unsolved metavars. Otherwise #check f where f takes implicit parameters would be pretty useless.
Kevin Buzzard (Mar 27 2018 at 20:04):
ha ha
Kevin Buzzard (Mar 27 2018 at 20:04):
#check (rfl : _ = _ + 0)
Kevin Buzzard (Mar 27 2018 at 20:04):
didn't give what I expected
Kevin Buzzard (Mar 27 2018 at 20:05):
but probably did give what everyone else expected.
Kevin Buzzard (Mar 27 2018 at 20:08):
The underscores won't find it because it is not determined by unification.
unification says "this should be a proof of ev _x", and there is something in the local context which is a proof of ev _x
Kevin Buzzard (Mar 27 2018 at 20:08):
@Kenny Lau my proof of ev_double is lame. Can you do better?
Kevin Buzzard (Mar 27 2018 at 20:09):
This one surely qualifies for the "this is mathematically obvious so it doesn't matter how obscure the proof is, just make it short"
Patrick Massot (Mar 27 2018 at 20:10):
@Kenny Lau my proof of ev_double is lame. Can you do better?
I should do that with my PhD student, and see what comes out of it.
Kenny Lau (Mar 27 2018 at 20:10):
@Patrick Massot "of course it's even, you just doubled it!"
Patrick Massot (Mar 27 2018 at 20:10):
I mean asking about real proofs
Kenny Lau (Mar 27 2018 at 20:11):
@Kevin Buzzard are you aiming for length?
Kevin Buzzard (Mar 27 2018 at 20:12):
brevity
Patrick Massot (Mar 27 2018 at 20:13):
By the way, we have a new nice example of a real world theorem built purely on trusting the big guys in the field: https://arxiv.org/abs/1803.07997 There are three ingredients: one was announced in 2001 and never written. One has a draft written in 2012 but the author doesn't want to make it into a publishable paper. The third one is published but none of the experts except the author understand the proof.
Patrick Massot (Mar 27 2018 at 20:14):
One day, proof assistants will change all that
Kenny Lau (Mar 27 2018 at 20:14):
theorem ev_double : ∀ (n : ℕ), ev (double n) | 0 := ev_0 | (n+1) := (by simp [double] : double n + 2 = double (n+1)) ▸ ev_SS _ (ev_double n)
Kenny Lau (Mar 27 2018 at 20:14):
how is this?
Kenny Lau (Mar 27 2018 at 20:15):
we all know there's so many things we need to do
Kenny Lau (Mar 27 2018 at 20:15):
we need to prove the equality somehow
Kenny Lau (Mar 27 2018 at 20:15):
and we need to use recursion
Chris Hughes (Mar 27 2018 at 20:15):
lemma ev_double (n : ℕ) : ev (2 * n) := nat.rec_on n ev.ev_0 (λ n hi, ev_SS _ hi)
Kenny Lau (Mar 27 2018 at 20:15):
well
Patrick Massot (Mar 27 2018 at 20:16):
Johannes has a bad influence on Chris
Kenny Lau (Mar 27 2018 at 20:16):
changing the definition of double is called cheating :P
Sebastian Ullrich (Mar 27 2018 at 20:16):
I see an unused eta contraction
Chris Hughes (Mar 27 2018 at 20:16):
What's the definition of double?
Kenny Lau (Mar 27 2018 at 20:16):
definition double (n : ℕ) := n + n
Kenny Lau (Mar 27 2018 at 20:17):
and by eta contraction he means
lemma ev_double (n : ℕ) : ev (2 * n) := nat.rec_on n ev.ev_0 (λ n, ev_SS _)
Chris Hughes (Mar 27 2018 at 20:27):
My best attempt for double. I saved three characters by using rec instead of rec_on
lemma ev_double (n : ℕ) : ev (double n) := nat.rec ev_0 (λ n h, show ev (_ + _), by rw succ_add; from ev_SS _ h) n
Kenny Lau (Mar 27 2018 at 20:27):
do we count brevity by characters?
Kevin Buzzard (Mar 27 2018 at 20:27):
or by tokens
Kenny Lau (Mar 27 2018 at 20:27):
this is ridiculous
Kevin Buzzard (Mar 27 2018 at 20:28):
or by file size
Kenny Lau (Mar 27 2018 at 20:28):
if your goal is to save time, you should stick with what you have
Kevin Buzzard (Mar 27 2018 at 20:28):
(so then probably fancy unicode characters cost more)
Kevin Buzzard (Mar 27 2018 at 20:29):
and he opened nat! Is that allowed? you have to put nat.succ_add
Chris Hughes (Mar 27 2018 at 20:30):
I think there should be bonus points for term style. I would have used eq.subst but it was longer.
Kevin Buzzard (Mar 27 2018 at 20:33):
I don't understand the syntax of Chris' answer! What is this ; from business? I've only ever seen ; in tactic mode.
Kevin Buzzard (Mar 27 2018 at 20:33):
oh we are in tactic mode?
Kevin Buzzard (Mar 27 2018 at 20:33):
Then my question is "what is this from in tactic mode?"
Kevin Buzzard (Mar 27 2018 at 20:34):
and now I hover over it and find out.
Chris Hughes (Mar 27 2018 at 20:34):
You can use from instead of exact, if you want to save one character.
Kevin Buzzard (Mar 27 2018 at 20:34):
I think that's the main reason they put it in.
Kevin Buzzard (Mar 27 2018 at 20:34):
Chris do you know about pyth? (as in "pithy")
Kevin Buzzard (Mar 27 2018 at 20:34):
https://esolangs.org/wiki/Pyth
Kenny Lau (Mar 27 2018 at 20:35):
you bunch are ridiculous
Kenny Lau (Mar 27 2018 at 20:35):
ok to be fair I use pyth when I need to compute something quickly
Kenny Lau (Mar 27 2018 at 20:35):
and it's far more convenient than other programming languages
Kevin Buzzard (Mar 27 2018 at 20:36):
ha ha "you bunch are ridiculous" "actually I use it IRL"
Mario Carneiro (Mar 27 2018 at 20:36):
The ; there is actually in tactic mode
Kevin Buzzard (Mar 27 2018 at 20:36):
yes it all dawned on me later
Kenny Lau (Mar 27 2018 at 20:36):
wait what?
Kevin Buzzard (Mar 27 2018 at 20:36):
I hadn't seen from in tactic mode before
Kenny Lau (Mar 27 2018 at 20:37):
@Kevin Buzzard he's saying that ; itself is in tactic mode
Mario Carneiro (Mar 27 2018 at 20:37):
it's just so you can write have x, from y in tactic mode
Kevin Buzzard (Mar 27 2018 at 20:37):
I think we need "coz"
Kevin Buzzard (Mar 27 2018 at 20:37):
which is from but one fewer letter
Kevin Buzzard (Mar 27 2018 at 20:37):
I'll file an issue
Mario Carneiro (Mar 27 2018 at 20:38):
I prefer exact over from when it's not used after show, have, suffices or let tactics
Mario Carneiro (Mar 27 2018 at 20:39):
As for the golfing, I won't enter the ring. I'd emphasize good lemmas in this instance so you can write each individual theorem very concisely
Kevin Buzzard (Mar 27 2018 at 20:40):
Aah I see. Perhaps double n = n * 2 or 2 * n would be worth proving before we launch into trying to prove stuff like this
Patrick Massot (Mar 27 2018 at 20:40):
I hope the new parser will allow Kevin to define coz by adding one line near the top of his file
Patrick Massot (Mar 27 2018 at 20:41):
Do code-golf belong to the target of "domain specific language handling"?
Mario Carneiro (Mar 27 2018 at 20:42):
You can define coz in one line today
Kenny Lau (Mar 27 2018 at 20:42):
@Kevin Buzzard I've been a member of PPCG for 3 years
Kenny Lau (Mar 27 2018 at 20:42):
the people in the chat know me
Mario Carneiro (Mar 27 2018 at 20:42):
meta def tactic.interactive.coz := tactic.interactive.from
Patrick Massot (Mar 27 2018 at 20:43):
message stared
Kenny Lau (Mar 27 2018 at 20:44):
lol
Kenny Lau (Mar 27 2018 at 20:44):
and a solution a la Mario:
lemma double.aux (n : ℕ) : double (n+1) = double n + 2 := nat.succ_add _ _ lemma ev_double (n : ℕ) : ev (double n) := nat.rec ev_0 (λ n h, (double.aux n).symm ▸ ev_SS _ h) n
Kevin Buzzard (Mar 27 2018 at 20:49):
By the way, we have a new nice example of a real world theorem built purely on trusting the big guys in the field: https://arxiv.org/abs/1803.07997 There are three ingredients: one was announced in 2001 and never written. One has a draft written in 2012 but the author doesn't want to make it into a publishable paper. The third one is published but none of the experts except the author understand the proof.
@Patrick Massot as long as the experts are happy, we're all happy, right?
Kevin Buzzard (Mar 27 2018 at 20:50):
I would be most concerned about the third assumption I guess.
Patrick Massot (Mar 27 2018 at 20:50):
Right. But there are not all happy about the third ingredient.
Patrick Massot (Mar 27 2018 at 20:50):
Because the third ingredient was proved by an obscure polish mathematician
Kevin Buzzard (Mar 27 2018 at 20:50):
so you'll have to hope that the referees are either optimists or lazy
Patrick Massot (Mar 27 2018 at 20:51):
Who didn't even get the Crafoord prize.
Patrick Massot (Mar 27 2018 at 20:52):
We have two more elaborate plans actually. First we'd like to try to read the Polish proof. And we have a backup plan which is to use an earlier weaker result (about diffeomorphisms, ) to get a correspondingly weaker (but still new) result
Patrick Massot (Mar 27 2018 at 20:53):
How do you get LaTeX rendering on this website?
Kevin Buzzard (Mar 27 2018 at 20:54):
two $s
Patrick Massot (Mar 27 2018 at 20:54):
weird
Kevin Buzzard (Mar 27 2018 at 20:54):
ooh Coq has an inversion tactic
Patrick Massot (Mar 27 2018 at 20:54):
inverting what?
Kenny Lau (Mar 27 2018 at 20:54):
is there a subversion tactic?
Patrick Massot (Mar 27 2018 at 20:55):
nooo subversion is dead
Patrick Massot (Mar 27 2018 at 20:55):
all cool kids use git nowadays
Kevin Buzzard (Mar 27 2018 at 20:55):
Theorem evSS_ev : ∀ n, ev (S (S n)) → ev n. Proof. intros n E. inversion E as [| n' E']. (* We are in the E = ev_SS n' E' case now. *) apply E'. Qed.
Kevin Buzzard (Mar 27 2018 at 20:56):
induction n would not go down well here
Kevin Buzzard (Mar 27 2018 at 20:57):
Coq knows that the only way to prove ev (S S n) is to prove ev n and deduce ev (S S n)
Kenny Lau (Mar 27 2018 at 20:58):
is this the same as coinduction?
Kevin Buzzard (Mar 27 2018 at 20:58):
The question in full:
Kevin Buzzard (Mar 27 2018 at 20:59):
inductive ev : nat → Prop | ev_0 : ev 0 | ev_SS : ∀ n : nat, ev n → ev (n+2) open ev example : ∀ n, ev (n+2) → ev n := sorry
Kevin Buzzard (Mar 27 2018 at 21:04):
oh no way, intros n H, cases H works!
Kevin Buzzard (Mar 27 2018 at 21:04):
Yay, we have an inversion tactic!
Patrick Massot (Mar 27 2018 at 21:05):
I still don't understand what this inversion tactic is meant to do.
Kevin Buzzard (Mar 27 2018 at 21:05):
example : ¬ (ev 1) := begin intro H, cases H, end
Patrick Massot (Mar 27 2018 at 21:05):
(but I'm writing lecture notes on convex integration without integration in parallel of reading Zulip)
Kenny Lau (Mar 27 2018 at 21:06):
@Kevin Buzzard I have a solution: do you want to see it?
Kevin Buzzard (Mar 27 2018 at 21:06):
inversion says "You are assuming ev (n+2) and the only way to prove this would be by proving ev(n) and tehen applying ev_SS
Kenny Lau (Mar 27 2018 at 21:06):
btw what you call "inversion" is just induction on the inductive predicate "ev"
Kenny Lau (Mar 27 2018 at 21:06):
(it's called inductive because you can do induction)
Kevin Buzzard (Mar 27 2018 at 21:06):
it's what software foundations calls inversion
Sebastian Ullrich (Mar 27 2018 at 21:08):
"rule inversion" is what computer scientists say when they mean "case analysis"
Kenny Lau (Mar 27 2018 at 21:08):
@Kevin Buzzard for a second I thought this is something Lean doesn't have
Sebastian Ullrich (Mar 27 2018 at 21:08):
(well, it's specific to inductive definitions usually)
Kevin Buzzard (Mar 27 2018 at 21:08):
So did I, that's why I mentioned it here
Sebastian Ullrich (Mar 27 2018 at 21:10):
case (hah) in point
example : ∀ n, ev (n+2) → ev n | n (ev_SS _ h) := h
Patrick Massot (Mar 27 2018 at 21:11):
Kevin and Kenny, have you managed to prove an affine scheme is a scheme?
Kenny Lau (Mar 27 2018 at 21:11):
if we're allowed to assume false, then we've proved it
Kenny Lau (Mar 27 2018 at 21:12):
@Sebastian Ullrich hmm, I still have much to learn
Kenny Lau (Mar 27 2018 at 21:12):
you gave a 2-line solution
Kenny Lau (Mar 27 2018 at 21:12):
mine had 10 lines
Sebastian Ullrich (Mar 27 2018 at 21:12):
I considered formatting it as one line
Kenny Lau (Mar 27 2018 at 21:21):
@Kevin Buzzard do you have a link?
Kevin Buzzard (Mar 27 2018 at 21:22):
For schemes? I think we're in the wrong topic. We are plenty of lemmas short of proving that an affine scheme is a scheme.
Kevin Buzzard (Mar 27 2018 at 21:22):
Tom Hales told me he was going to mention it in his talk at AITP today
Kevin Buzzard (Mar 27 2018 at 21:23):
so Kenny and I and Chris were hard at work trying to get it done
Kevin Buzzard (Mar 27 2018 at 21:23):
and then Tom broke his toe and couldn't go to the conference :-/
Kevin Buzzard (Mar 27 2018 at 21:23):
so I decided to leave the undergraduates alone so they can revise for their exams!
Kenny Lau (Mar 27 2018 at 21:23):
as if they would really do so
Kevin Buzzard (Mar 27 2018 at 21:23):
Are you not revising mechanics?
Kenny Lau (Mar 27 2018 at 21:24):
I'm building the function X -> T
Patrick Massot (Mar 27 2018 at 21:24):
There are not revising and you are code golfing...
Patrick Massot (Mar 27 2018 at 21:24):
Go back to schemes!
Patrick Massot (Mar 27 2018 at 21:24):
:wink:
Kenny Lau (Mar 27 2018 at 21:25):
Are you not revising mechanics
Kenny Lau (Mar 27 2018 at 21:25):
Let's look at my latest test scores
Kenny Lau (Mar 27 2018 at 21:25):
M1M2 100%
Kenny Lau (Mar 27 2018 at 21:25):
M1P2 100%
Kenny Lau (Mar 27 2018 at 21:25):
M1A1 100%
Kenny Lau (Mar 27 2018 at 21:25):
conclusion: continue building the map
Kevin Buzzard (Mar 27 2018 at 21:26):
are you arguing by induction?
Kevin Buzzard (Mar 27 2018 at 21:26):
This is a dangerous technique :-)
Kevin Buzzard (Mar 27 2018 at 21:26):
The final exam is worth 18 times more than the tests so you need to work 18 times as hard, right?
Patrick Massot (Mar 27 2018 at 21:26):
This AITP looks interesting
Kenny Lau (Mar 27 2018 at 21:26):
what is AITP?
Patrick Massot (Mar 27 2018 at 21:26):
why did nobody mentioned that when we discussed ITP?
Patrick Massot (Mar 27 2018 at 21:27):
http://aitp-conference.org/2017/
Kevin Buzzard (Mar 27 2018 at 21:27):
a conference on the top of a mountain
Kevin Buzzard (Mar 27 2018 at 21:27):
That link might be last year's...
Patrick Massot (Mar 27 2018 at 21:27):
That where @Sebastian Ullrich must be then!
Kevin Buzzard (Mar 27 2018 at 21:27):
just at a guess
Andrew Ashworth (Mar 27 2018 at 21:27):
conferences are always best when they are in a desireable location
Kevin Buzzard (Mar 27 2018 at 21:27):
I never think that
Kevin Buzzard (Mar 27 2018 at 21:27):
My favourite conferences are in big cities
Kevin Buzzard (Mar 27 2018 at 21:27):
that way I don't miss home so much
Kevin Buzzard (Mar 27 2018 at 21:28):
I have been asked to go to exotic conferences in exotic places like Hawaii and have declined
Andrew Ashworth (Mar 27 2018 at 21:28):
think of your graduate students who attend who can't afford holidays abroad without work kicking in a bit :)
Kevin Buzzard (Mar 27 2018 at 21:28):
because I was not sure I could handle a week there
Kevin Buzzard (Mar 27 2018 at 21:28):
Last three conferences I went to were in Boston, Berkeley and LA
Patrick Massot (Mar 27 2018 at 21:29):
Indeed I was probably looking for http://aitp-conference.org/2018/
Sebastian Ullrich (Mar 27 2018 at 21:29):
@Patrick Massot wait what
Patrick Massot (Mar 27 2018 at 21:30):
Oh, it's in Aussois!
Sebastian Ullrich (Mar 27 2018 at 21:30):
I try to avoid going skiing in March, February is way better
Patrick Massot (Mar 27 2018 at 21:31):
I could have gone there easily (except that I'm teaching this week)
Patrick Massot (Mar 27 2018 at 21:31):
I read "Robert Lewis: Toward AI for Lean, via metaprogramming"
Patrick Massot (Mar 27 2018 at 21:32):
Looks like some people got proper training in grant proposal writing
Patrick Massot (Mar 27 2018 at 21:32):
I would fund that one
Matt Wilson (Mar 27 2018 at 21:34):
is that paper available publicly?
Patrick Massot (Mar 27 2018 at 21:34):
I also like the spirit of the schedule:
March 25
19:30 dinner
March 26
...
Sebastian Ullrich (Mar 27 2018 at 21:39):
Oh, I didn't know Rob had a new paper
Sebastian Ullrich (Mar 27 2018 at 21:39):
I love that the conference page concludes with ski rental prices
Patrick Massot (Mar 27 2018 at 21:40):
Does talking in this conference imply new paper?
Patrick Massot (Mar 27 2018 at 21:41):
(I'm trying to learn CS academic life)
Andrew Ashworth (Mar 27 2018 at 21:41):
you have to hope that your labmates ski though; not one of mine in graduate school did
Patrick Massot (Mar 27 2018 at 21:44):
There is http://aitp-conference.org/2018/aitp18-proceedings.pdf but it contains only one page by Rob
Patrick Massot (Mar 27 2018 at 21:45):
But it contains question relevant to Lean 4 (stuff about the VM)
Patrick Massot (Mar 27 2018 at 21:48):
I'd be curious to know what Hales intended to say
Kevin Buzzard (Mar 27 2018 at 21:48):
He was probably going to let out the secret.
Patrick Massot (Mar 27 2018 at 21:49):
Which one? There are so many secrets
Kevin Buzzard (Mar 27 2018 at 21:49):
He just got a big grant to fund formal abstracts
Patrick Massot (Mar 27 2018 at 21:49):
Oooh
Kevin Buzzard (Mar 27 2018 at 21:50):
and talking of secrets
Patrick Massot (Mar 27 2018 at 21:50):
Fund what exactly?
Kevin Buzzard (Mar 27 2018 at 21:50):
today I heard i'd been awarded a rather smaller grant to find my 13 undergraduates this summer
Kevin Buzzard (Mar 27 2018 at 21:50):
I think Hales is going to pay people to type in statements of theorems in the Annals or whatever.
Kevin Buzzard (Mar 27 2018 at 21:51):
into Lean
Patrick Massot (Mar 27 2018 at 21:51):
Where will he find those people?
Kevin Buzzard (Mar 27 2018 at 21:51):
If he's sitting at home with a broken toe he should come here and tell us the details :-)
Rob Lewis (Mar 27 2018 at 22:02):
Hah, I guessed from the email I just got that I was mentioned here. There's no new paper, just a talk about some experiments that Minchao and I have been doing in our free time. Nothing very deep.
Rob Lewis (Mar 27 2018 at 22:03):
The slides will eventually be online. The wifi here barely works, it took me ten minutes to email a picture of the scenery so I'm not gonna try to upload them now.
Patrick Massot (Mar 27 2018 at 22:03):
Is this hammer thing the same as the stuff Isabelle users always talk about?
Rob Lewis (Mar 27 2018 at 22:04):
Yeah. There's a recent paper that translates the idea to Coq.
Patrick Massot (Mar 27 2018 at 22:05):
Great!
Patrick Massot (Mar 27 2018 at 22:06):
Do you have a public demo?
Patrick Massot (Mar 27 2018 at 22:07):
And, while you're here: are you considering have your Mathematica stuff turned into a Sage stuff?
Rob Lewis (Mar 27 2018 at 22:11):
We've only worked out the relevance filter component, and it isn't quite fast enough for practical use yet. This is really just experimenting right now. There's some messy jumble of code on github but nothing you want to look at. Johannes and I have been talking to a masters student who is interested in this kind of automation though, so with some luck, the three of us will make some progress soon.
Rob Lewis (Mar 27 2018 at 22:11):
The ideas behind the link will transfer easily enough. The engineering is another story, and I've never actually used Sage.
Rob Lewis (Mar 27 2018 at 22:12):
It could happen, particularly with an application in mind, but it isn't at the top of my to-do list.
Patrick Massot (Mar 27 2018 at 22:15):
I don't have any specific application in mind. But I was surprised by your paper because I know no Mathematica user, everybody uses Sage around me, and teaches Sage to students
Patrick Massot (Mar 27 2018 at 22:16):
And Lean is open source software so it looks strange to choose Mathematica as a partner
Patrick Massot (Mar 27 2018 at 22:17):
(well Lean 4 development is not yet open source, but let's hope for the best)
Patrick Massot (Mar 27 2018 at 22:18):
But I should be sleeping. Tomorrow I need to teach old fashioned algebraic geometry in Sage (computing projections of algebraic sets using resultants).
Patrick Massot (Mar 27 2018 at 22:18):
Bye
Rob Lewis (Mar 27 2018 at 22:19):
I had the opposite experience as an undergrad, they taught us Mathematica and nothing else. Most of the people I asked said similar, but it was definitely a biased sample. And there were people at Wolfram who were already interested in Lean, so it made sense at the time, heh.
Rob Lewis (Mar 27 2018 at 22:19):
I should also call it a night!
Kevin Buzzard (Mar 27 2018 at 22:24):
I'm still sitting here idly trying software foundations.
Kevin Buzzard (Mar 27 2018 at 22:25):
namespace hidden
inductive le : nat → nat → Prop
| le_n : ∀ n, le n n
| le_S : ∀ n m, (le n m) → (le n (nat.succ m))
local infix ` lq ` :50 := λ m n, le m n
open le
lemma n_le_m__Sn_le_Sm : ∀ n m,
n lq m → nat.succ n lq nat.succ m :=
begin
intros n m H,
cases H with NOT_USED NOT_USED_EITHER q Hnq,
repeat {admit},
end
Kevin Buzzard (Mar 27 2018 at 22:26):
cases is throwing away my variable names
Kevin Buzzard (Mar 27 2018 at 22:27):
(I called it lq to avoid confusion with already-defined-things)
Kevin Buzzard (Mar 27 2018 at 23:31):
I proved 2+2 isn't 6
Kevin Buzzard (Mar 27 2018 at 23:31):
definition S (n : ℕ) := nat.succ n inductive R : nat → nat → nat → Prop | c1 : R 0 0 0 | c2 : ∀ m n o, R m n o → R (S m) n (S o) | c3 : ∀ m n o, R m n o → R m (S n) (S o) open R example : R 1 1 2 := c3 _ _ _ (c2 _ _ _ c1) example : ¬ (R 2 2 6) := begin intro H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, cases H with H H H H H H H H, end
Kevin Buzzard (Mar 27 2018 at 23:33):
Cases eats far too many variables which makes the proof look even more ridiculous
Kevin Buzzard (Mar 27 2018 at 23:34):
Cut and paste from VS Code into zulipchat (ubuntu, firefox) isn't great. I get extra spaces, extra carriage returns
Mario Carneiro (Mar 27 2018 at 23:38):
I'm not sure what's up with zulip paste. I don't think it was doing that when we first moved
Mario Carneiro (Mar 27 2018 at 23:38):
Here's a shorter way to write that proof:
example : ¬ (R 2 2 6) | H := by casesm * [R _ _ _]
Mario Carneiro (Mar 27 2018 at 23:39):
but if you look at the resulting proof, it's rather involved
Mario Carneiro (Mar 27 2018 at 23:40):
You can simplify the proof if you define R to avoid having both c2 and c3; the proof length here increases exponentially
Mario Carneiro (Mar 27 2018 at 23:45):
cases is throwing away my variable names
I tried once to make a version of cases that doesn't throw away names, but it's tough. What happens is that the names are allotted first, in the case splits, and then some cases are eliminated outright by inversion so you never see those names. I just put _ for those
Kenny Lau (Mar 29 2018 at 09:18):
@Kevin Buzzard did you do the 4-star exercise proving that the two notions of evenness are equivalent?
Kevin Buzzard (Mar 29 2018 at 09:18):
Three notions :-)
Kevin Buzzard (Mar 29 2018 at 09:18):
I must be ahead of you ;-)
Kevin Buzzard (Mar 29 2018 at 09:19):
Link?
Kevin Buzzard (Mar 29 2018 at 09:20):
Use cases or induction on the inductive prop, if that's the issue. This blew my mind.
Kenny Lau (Mar 29 2018 at 09:20):
https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab206
Kevin Buzzard (Mar 29 2018 at 09:20):
Yes I did that one
Kevin Buzzard (Mar 29 2018 at 09:21):
I did the exercise before that one as well, which IIRC I used.
Kevin Buzzard (Mar 29 2018 at 09:27):
Here's what I think Kenny is asking:
Kenny Lau (Mar 29 2018 at 09:27):
All I'm asking is " did you do the 4-star exercise proving that the two notions of evenness are equivalent? "
Kevin Buzzard (Mar 29 2018 at 09:27):
def S := nat.succ inductive ev : nat → Prop | ev_0 : ev 0 | ev_SS : ∀ n : nat, ev n → ev (S (S n)) inductive ev' : nat → Prop | ev'_0 : ev' 0 | ev'_2 : ev' 2 | ev'_sum : ∀ n m, ev' n → ev' m → ev' (n + m) theorem ev'_ev : ∀ n, ev' n ↔ ev n := sorry
Kenny Lau (Mar 29 2018 at 09:27):
right
Kevin Buzzard (Mar 29 2018 at 09:27):
and the answer is "yes, I did it whilst watching the football on Tuesday"
Kenny Lau (Mar 29 2018 at 09:28):
did you use term mode or tactic mode?
Kevin Buzzard (Mar 29 2018 at 09:28):
tactic
Kenny Lau (Mar 29 2018 at 09:28):
why am i not surprised
Kevin Buzzard (Mar 29 2018 at 09:28):
I really like Software Foundations, because I can do the exercises no matter how many stars they have, which is a good confidence boost :-)
Kevin Buzzard (Mar 29 2018 at 09:29):
The first time I saw a 5-star one I thought "oh gosh", and then I just sat down and did it, and thought "maybe I already know what they're trying to teach me here"
Kenny Lau (Mar 29 2018 at 09:29):
maybe they're teaching you to quit using tactic mode
Kevin Buzzard (Mar 29 2018 at 09:29):
rofl
Andrew Ashworth (Mar 29 2018 at 09:30):
Coq is big on tactic mode
Andrew Ashworth (Mar 29 2018 at 09:30):
Term mode is favored by mathematicians who work in isabelle
Andrew Ashworth (Mar 29 2018 at 09:31):
Ish. Obviously there are exceptions
Kevin Buzzard (Mar 29 2018 at 09:31):
Lean docs seem to push term mode a lot at the start.
Kevin Buzzard (Mar 29 2018 at 09:31):
I did notice that Software foundations instantly starts with "OK so here are some easy things, let's prove them in tactic mode".
Andrew Ashworth (Mar 29 2018 at 09:31):
You mean Jeremy pushes term mode in TIPL :simple_smile:
Kevin Buzzard (Mar 29 2018 at 09:31):
As did a Coq tutorial I did before I came to Lean.
Kevin Buzzard (Mar 29 2018 at 09:32):
I think that mathematicians should start with tactic mode
Kevin Buzzard (Mar 29 2018 at 09:32):
because they typically have no idea what a functional language is or what a lambda is
Kenny Lau (Mar 29 2018 at 09:32):
mathematicians should start with formal proofs...
Kenny Lau (Mar 29 2018 at 09:32):
fitch, hilbert, whatever
Kevin Buzzard (Mar 29 2018 at 09:32):
right
Kevin Buzzard (Mar 29 2018 at 09:32):
via tactic mode
Kenny Lau (Mar 29 2018 at 09:32):
via writing it down on pen and paper
Andrew Ashworth (Mar 29 2018 at 09:34):
You can get pretty far writing everything out with assume, show, and calc in lean
Kenny Lau (Mar 29 2018 at 09:35):
as far as Zeno got?
Kevin Buzzard (Mar 29 2018 at 09:36):
whenever I do a tactic proof I don't indent the line after begin and I can hear Johannes' voice in my head telling me that I can't get it PR'ed to mathlib that way
Andrew Ashworth (Mar 29 2018 at 09:36):
Not familiar with his proofs, unfortunately
Andrew Ashworth (Mar 29 2018 at 09:37):
Haha, best fix your style or else you'll get another nasty email asking you to teach your students the mathlib style
Kevin Buzzard (Mar 29 2018 at 09:37):
It's the voices in my head I have to deal with
Andrew Ashworth (Mar 29 2018 at 09:39):
be the compiler, be the journal editor... these voices are quite talented
Kevin Buzzard (Mar 29 2018 at 09:39):
yeah I have some pretty high-class voices in my head.
Andrew Ashworth (Mar 29 2018 at 09:43):
Did you skip over the 5 star pumping lemma? That was quite an exercise
Andrew Ashworth (Mar 29 2018 at 09:44):
Actually even the one on palindromes in the same chapter was involved
Kevin Buzzard (Mar 29 2018 at 09:44):
I looked at that when I didn't have access to a computer
Kevin Buzzard (Mar 29 2018 at 09:44):
and decided that mathematicians didn't care about pumping lemmas.
Kevin Buzzard (Mar 29 2018 at 09:44):
I did do the 5 star constructive mathematics exercise even though the first time I saw it I figured mathematicians didn't care about that either.
Kenny Lau (Mar 29 2018 at 09:45):
@Kevin Buzzard try doing regex :P
Kevin Buzzard (Mar 29 2018 at 09:45):
I did the 4 star even question again just now, because I couldnt' find my original solution and Kenny asking it made me concerned I'd missed something.
Kevin Buzzard (Mar 29 2018 at 09:45):
I saw that regex stuff. I am not convinced I need to learn this sort of skill. I'm sure I'd find it a lot of fun
Kevin Buzzard (Mar 29 2018 at 09:45):
but I need to focus on other things.
Kevin Buzzard (Mar 29 2018 at 09:47):
Kenny, my evenness proof is just repeat {induction *, exact *}
Kevin Buzzard (Mar 29 2018 at 09:47):
well, perhaps not quite that
Kenny Lau (Mar 29 2018 at 20:03):
I have a 4-line 223-character solution
Kenny Lau (Mar 29 2018 at 20:03):
inductive ev : nat → Prop | ev_0 : ev 0 | ev_SS : ∀ n, ev n → ev (n + 2) inductive ev' : nat → Prop | ev'_0 : ev' 0 | ev'_2 : ev' 2 | ev'_sum : ∀ n m, ev' n → ev' m → ev' (n + m) open ev open ev' theorem ev'_ev.standalone : ∀ n, ev' n ↔ ev n := Line 1 Line 2 Line 3 Line 4
Kenny Lau (Mar 29 2018 at 20:03):
Let's see who can beat me
Kenny Lau (Mar 29 2018 at 20:04):
(I used appropriate spacings and I counted them in)
Andrew Ashworth (Mar 29 2018 at 20:11):
i'm surprised there's so much interest in the "three different definitions of even" exercise
Kenny Lau (Mar 29 2018 at 20:11):
@Andrew Ashworth beat me :P
Andrew Ashworth (Mar 29 2018 at 20:11):
i thought the most interesting ones in that chapter were the subseq and palindrome problems
Andrew Ashworth (Mar 29 2018 at 20:12):
i would give it a shot except i'm currently supposedly doing work at the moment
Andrew Ashworth (Mar 29 2018 at 20:14):
and i think the nodup and nostutter predicates are interesting since they are related to how finite sets are implemented in lean
Ching-Tsun Chou (Mar 29 2018 at 20:38):
I would be interested to know if anyone can prove the pigeonhole principle (last exercise of the IndProp chapter) without excluded_middle.
Last updated: Dec 20 2023 at 11:08 UTC