Zulip Chat Archive

Stream: general

Topic: idly trying software foundations


view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 19:48):

theorem ev_plus4 : ∀ n, ev n → ev (n + 4) := λ _ _,ev_SS _ (ev_SS _ _)

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 19:48):

I thought there was every chance :-)

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 19:49):

but I get

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 19:49):

don't know how to synthesize placeholder
context:
_x : ℕ,
_x : ev _x
⊢ ev _x

view this post on Zulip Kenny Lau (Mar 27 2018 at 19:57):

what is software foundations?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 19:58):

a book on the web

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 19:58):

https://softwarefoundations.cis.upenn.edu/

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 19:59):

They have exercises like this:

view this post on Zulip Gabriel Ebner (Mar 27 2018 at 19:59):

You need to plug in the assumption for ev n somewhere.

view this post on Zulip 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})

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 19:59):

I wanted the elaborator to guess where. I have it as an underscore

view this post on Zulip Gabriel Ebner (Mar 27 2018 at 20:00):

The underscores won't find it because it is not determined by unification.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:01):

it's the same reason #check λ n : nat, (rfl : _ + 4 = (_ + 2) + 2) fails, I think

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:01):

(obviously it's n!!)

view this post on Zulip Gabriel Ebner (Mar 27 2018 at 20:01):

It could also be 0, or 1, or...

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 20:01):

Or n!! :smile:

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:02):

but #check λ n : nat, (rfl : _ + 4 = (_ + 4)) works...

view this post on Zulip Gabriel Ebner (Mar 27 2018 at 20:02):

But I hope you get a metavariable and not n, right?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:04):

ha ha

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:04):

#check (rfl : _ = _ + 0)

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:04):

didn't give what I expected

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:05):

but probably did give what everyone else expected.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:08):

@Kenny Lau my proof of ev_double is lame. Can you do better?

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:10):

@Patrick Massot "of course it's even, you just doubled it!"

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:10):

I mean asking about real proofs

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:11):

@Kevin Buzzard are you aiming for length?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:12):

brevity

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:14):

One day, proof assistants will change all that

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:14):

how is this?

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:15):

we all know there's so many things we need to do

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:15):

we need to prove the equality somehow

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:15):

and we need to use recursion

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:15):

well

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:16):

Johannes has a bad influence on Chris

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:16):

changing the definition of double is called cheating :P

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 20:16):

I see an unused eta contraction

view this post on Zulip Chris Hughes (Mar 27 2018 at 20:16):

What's the definition of double?

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:16):

definition double (n : ℕ) := n + n

view this post on Zulip 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 _)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:27):

do we count brevity by characters?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:27):

or by tokens

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:27):

this is ridiculous

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:28):

or by file size

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:28):

if your goal is to save time, you should stick with what you have

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:28):

(so then probably fancy unicode characters cost more)

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:29):

and he opened nat! Is that allowed? you have to put nat.succ_add

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:33):

oh we are in tactic mode?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:33):

Then my question is "what is this from in tactic mode?"

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:34):

and now I hover over it and find out.

view this post on Zulip Chris Hughes (Mar 27 2018 at 20:34):

You can use from instead of exact, if you want to save one character.

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:34):

I think that's the main reason they put it in.

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:34):

Chris do you know about pyth? (as in "pithy")

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:34):

https://esolangs.org/wiki/Pyth

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:35):

you bunch are ridiculous

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:35):

ok to be fair I use pyth when I need to compute something quickly

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:35):

and it's far more convenient than other programming languages

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:36):

ha ha "you bunch are ridiculous" "actually I use it IRL"

view this post on Zulip Mario Carneiro (Mar 27 2018 at 20:36):

The ; there is actually in tactic mode

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:36):

yes it all dawned on me later

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:36):

wait what?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:36):

I hadn't seen from in tactic mode before

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:37):

@Kevin Buzzard he's saying that ; itself is in tactic mode

view this post on Zulip Mario Carneiro (Mar 27 2018 at 20:37):

it's just so you can write have x, from y in tactic mode

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:37):

I think we need "coz"

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:37):

which is from but one fewer letter

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:37):

I'll file an issue

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:41):

Do code-golf belong to the target of "domain specific language handling"?

view this post on Zulip Mario Carneiro (Mar 27 2018 at 20:42):

You can define coz in one line today

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:42):

@Kevin Buzzard I've been a member of PPCG for 3 years

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:42):

the people in the chat know me

view this post on Zulip Mario Carneiro (Mar 27 2018 at 20:42):

meta def tactic.interactive.coz := tactic.interactive.from

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:43):

message stared

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:44):

lol

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:50):

I would be most concerned about the third assumption I guess.

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:50):

Right. But there are not all happy about the third ingredient.

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:50):

Because the third ingredient was proved by an obscure polish mathematician

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:50):

so you'll have to hope that the referees are either optimists or lazy

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:51):

Who didn't even get the Crafoord prize.

view this post on Zulip 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 CrC^r diffeomorphisms, r1+dim(V)/2r \leq 1+\dim(V)/2) to get a correspondingly weaker (but still new) result

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:53):

How do you get LaTeX rendering on this website?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:54):

two $s

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:54):

weird

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:54):

ooh Coq has an inversion tactic

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:54):

inverting what?

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:54):

is there a subversion tactic?

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:55):

nooo subversion is dead

view this post on Zulip Patrick Massot (Mar 27 2018 at 20:55):

all cool kids use git nowadays

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:56):

induction n would not go down well here

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:58):

is this the same as coinduction?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:58):

The question in full:

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:04):

oh no way, intros n H, cases H works!

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:04):

Yay, we have an inversion tactic!

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:05):

I still don't understand what this inversion tactic is meant to do.

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:05):

example : ¬ (ev 1) :=  begin
intro H,
cases H,
end

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:05):

(but I'm writing lecture notes on convex integration without integration in parallel of reading Zulip)

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:06):

@Kevin Buzzard I have a solution: do you want to see it?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:06):

btw what you call "inversion" is just induction on the inductive predicate "ev"

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:06):

(it's called inductive because you can do induction)

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:06):

it's what software foundations calls inversion

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 21:08):

"rule inversion" is what computer scientists say when they mean "case analysis"

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:08):

@Kevin Buzzard for a second I thought this is something Lean doesn't have

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 21:08):

(well, it's specific to inductive definitions usually)

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:08):

So did I, that's why I mentioned it here

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 21:10):

case (hah) in point

example : ∀ n, ev (n+2) → ev n
| n (ev_SS _ h) := h

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:11):

Kevin and Kenny, have you managed to prove an affine scheme is a scheme?

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:11):

if we're allowed to assume false, then we've proved it

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:12):

@Sebastian Ullrich hmm, I still have much to learn

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:12):

you gave a 2-line solution

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:12):

mine had 10 lines

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 21:12):

I considered formatting it as one line

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:21):

@Kevin Buzzard do you have a link?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:22):

Tom Hales told me he was going to mention it in his talk at AITP today

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:23):

so Kenny and I and Chris were hard at work trying to get it done

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:23):

and then Tom broke his toe and couldn't go to the conference :-/

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:23):

so I decided to leave the undergraduates alone so they can revise for their exams!

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:23):

as if they would really do so

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:23):

Are you not revising mechanics?

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:24):

I'm building the function X -> T

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:24):

There are not revising and you are code golfing...

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:24):

Go back to schemes!

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:24):

:wink:

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:25):

Are you not revising mechanics

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:25):

Let's look at my latest test scores

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:25):

M1M2 100%

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:25):

M1P2 100%

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:25):

M1A1 100%

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:25):

conclusion: continue building the map

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:26):

are you arguing by induction?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:26):

This is a dangerous technique :-)

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:26):

This AITP looks interesting

view this post on Zulip Kenny Lau (Mar 27 2018 at 21:26):

what is AITP?

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:26):

why did nobody mentioned that when we discussed ITP?

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:27):

http://aitp-conference.org/2017/

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:27):

a conference on the top of a mountain

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:27):

That link might be last year's...

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:27):

That where @Sebastian Ullrich must be then!

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:27):

just at a guess

view this post on Zulip Andrew Ashworth (Mar 27 2018 at 21:27):

conferences are always best when they are in a desireable location

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:27):

I never think that

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:27):

My favourite conferences are in big cities

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:27):

that way I don't miss home so much

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:28):

because I was not sure I could handle a week there

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:28):

Last three conferences I went to were in Boston, Berkeley and LA

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:29):

Indeed I was probably looking for http://aitp-conference.org/2018/

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 21:29):

@Patrick Massot wait what

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:30):

Oh, it's in Aussois!

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 21:30):

I try to avoid going skiing in March, February is way better

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:31):

I could have gone there easily (except that I'm teaching this week)

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:31):

I read "Robert Lewis: Toward AI for Lean, via metaprogramming"

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:32):

Looks like some people got proper training in grant proposal writing

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:32):

I would fund that one

view this post on Zulip Matt Wilson (Mar 27 2018 at 21:34):

is that paper available publicly?

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:34):

I also like the spirit of the schedule:

March 25
19:30 dinner
March 26
...

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 21:39):

Oh, I didn't know Rob had a new paper

view this post on Zulip Sebastian Ullrich (Mar 27 2018 at 21:39):

I love that the conference page concludes with ski rental prices

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:40):

Does talking in this conference imply new paper?

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:41):

(I'm trying to learn CS academic life)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:45):

But it contains question relevant to Lean 4 (stuff about the VM)

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:48):

I'd be curious to know what Hales intended to say

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:48):

He was probably going to let out the secret.

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:49):

Which one? There are so many secrets

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:49):

He just got a big grant to fund formal abstracts

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:49):

Oooh

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:50):

and talking of secrets

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:50):

Fund what exactly?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 21:51):

into Lean

view this post on Zulip Patrick Massot (Mar 27 2018 at 21:51):

Where will he find those people?

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 27 2018 at 22:03):

Is this hammer thing the same as the stuff Isabelle users always talk about?

view this post on Zulip Rob Lewis (Mar 27 2018 at 22:04):

Yeah. There's a recent paper that translates the idea to Coq.

view this post on Zulip Patrick Massot (Mar 27 2018 at 22:05):

Great!

view this post on Zulip Patrick Massot (Mar 27 2018 at 22:06):

Do you have a public demo?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 27 2018 at 22:16):

And Lean is open source software so it looks strange to choose Mathematica as a partner

view this post on Zulip Patrick Massot (Mar 27 2018 at 22:17):

(well Lean 4 development is not yet open source, but let's hope for the best)

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Mar 27 2018 at 22:18):

Bye

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Mar 27 2018 at 22:19):

I should also call it a night!

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 22:24):

I'm still sitting here idly trying software foundations.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 22:26):

cases is throwing away my variable names

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 22:27):

(I called it lq to avoid confusion with already-defined-things)

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 23:31):

I proved 2+2 isn't 6

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 23:33):

Cases eats far too many variables which makes the proof look even more ridiculous

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 _ _ _]

view this post on Zulip Mario Carneiro (Mar 27 2018 at 23:39):

but if you look at the resulting proof, it's rather involved

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:18):

Three notions :-)

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:18):

I must be ahead of you ;-)

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:19):

Link?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:20):

https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab206

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:20):

Yes I did that one

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:21):

I did the exercise before that one as well, which IIRC I used.

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:27):

Here's what I think Kenny is asking:

view this post on Zulip 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? "

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:27):

right

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:27):

and the answer is "yes, I did it whilst watching the football on Tuesday"

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:28):

did you use term mode or tactic mode?

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:28):

tactic

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:28):

why am i not surprised

view this post on Zulip 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 :-)

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:29):

maybe they're teaching you to quit using tactic mode

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:29):

rofl

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:30):

Coq is big on tactic mode

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:30):

Term mode is favored by mathematicians who work in isabelle

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:31):

Ish. Obviously there are exceptions

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:31):

Lean docs seem to push term mode a lot at the start.

view this post on Zulip 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".

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:31):

You mean Jeremy pushes term mode in TIPL :simple_smile:

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:31):

As did a Coq tutorial I did before I came to Lean.

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:32):

I think that mathematicians should start with tactic mode

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:32):

because they typically have no idea what a functional language is or what a lambda is

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:32):

mathematicians should start with formal proofs...

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:32):

fitch, hilbert, whatever

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:32):

right

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:32):

via tactic mode

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:32):

via writing it down on pen and paper

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:34):

You can get pretty far writing everything out with assume, show, and calc in lean

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:35):

as far as Zeno got?

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:36):

Not familiar with his proofs, unfortunately

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:37):

It's the voices in my head I have to deal with

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:39):

be the compiler, be the journal editor... these voices are quite talented

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:39):

yeah I have some pretty high-class voices in my head.

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:43):

Did you skip over the 5 star pumping lemma? That was quite an exercise

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 09:44):

Actually even the one on palindromes in the same chapter was involved

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:44):

I looked at that when I didn't have access to a computer

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:44):

and decided that mathematicians didn't care about pumping lemmas.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Mar 29 2018 at 09:45):

@Kevin Buzzard try doing regex :P

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:45):

but I need to focus on other things.

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:47):

Kenny, my evenness proof is just repeat {induction *, exact *}

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 09:47):

well, perhaps not quite that

view this post on Zulip Kenny Lau (Mar 29 2018 at 20:03):

I have a 4-line 223-character solution

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 29 2018 at 20:03):

Let's see who can beat me

view this post on Zulip Kenny Lau (Mar 29 2018 at 20:04):

(I used appropriate spacings and I counted them in)

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 20:11):

i'm surprised there's so much interest in the "three different definitions of even" exercise

view this post on Zulip Kenny Lau (Mar 29 2018 at 20:11):

@Andrew Ashworth beat me :P

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 20:11):

i thought the most interesting ones in that chapter were the subseq and palindrome problems

view this post on Zulip Andrew Ashworth (Mar 29 2018 at 20:12):

i would give it a shot except i'm currently supposedly doing work at the moment

view this post on Zulip 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

view this post on Zulip 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: May 12 2021 at 04:19 UTC