Zulip Chat Archive

Stream: general

Topic: having existential statements


Scott Morrison (Feb 14 2019 at 22:21):

My student @Aditya Agarwal has some code that has many instances of the following pattern:

have h2_irred : ∃(c' : α) (d' : polynomial α), (primitive d') ∧ ((C c') * d' = d) := has_primitive_factorisation d,
apply exists.elim h2_irred,
intros c' hc',
apply exists.elim hc',
intros d' hd',

Is there a more efficient means to achieve this have/apply exists.elim/intros effect?

Mario Carneiro (Feb 14 2019 at 22:24):

what is the goal?

Rob Lewis (Feb 14 2019 at 22:28):

rcases has_primitive_factorization_d with <c', d', hc', hd'>?

Mario Carneiro (Feb 14 2019 at 22:28):

I think the apply exists.intro/intros can be combined into cases or rcases. Thus:

rcases has_primitive_factorisation d with c', d', primd, rfl,

Patrick Massot (Feb 14 2019 at 22:29):

Mario is really getting old

Rob Lewis (Feb 14 2019 at 22:29):

He took the time to type it with the proper angle brackets.

Mario Carneiro (Feb 14 2019 at 22:29):

I went for coffee :)

Patrick Massot (Feb 14 2019 at 22:31):

Those rintro and rcases really give me trouble with my students. I wanted to use a minimal set of tactics, at least in the beginning. So I didn't introduce those. But it's too painful...

Mario Carneiro (Feb 14 2019 at 22:37):

I think it's better to learn rcases style than cases. You can start by saying it's the same as cases but with funny brackets, and then work it up to bigger tuples later

Mario Carneiro (Feb 14 2019 at 22:38):

I think it's pretty intuitive if you haven't seen cases yet

Kevin Buzzard (Feb 15 2019 at 10:03):

Those rintro and rcases really give me trouble with my students. I wanted to use a minimal set of tactics, at least in the beginning. So I didn't introduce those. But it's too painful...

Patrick this is something I was alluding to yesterday. We know so many tactics and function names that we have forgotten how completely intimidating it is for beginners.

Mario Carneiro (Feb 15 2019 at 10:13):

We're teaching tactics this week in ITP class, and it's a struggle indeed. We need a better cheat sheet

Mario Carneiro (Feb 15 2019 at 10:14):

If you tell people about intro, cases, apply, exact, by_cases, contradiction, by_contradiction, split, existsi already their heads are exploding

Mario Carneiro (Feb 15 2019 at 10:14):

it's difficult to just hold them all in short term memory

Johan Commelin (Feb 15 2019 at 10:15):

If you tell people about intro, cases, apply, exact, by_cases, contradiction, by_contradiction, split, existsi already their heads are exploding

existsi use

Mario Carneiro (Feb 15 2019 at 10:15):

We haven't started on mathlib yet

Johan Commelin (Feb 15 2019 at 10:15):

Poor students.

Mario Carneiro (Feb 15 2019 at 10:15):

the head exploding will only get worse

Mario Carneiro (Feb 15 2019 at 10:17):

also left, right, constructor

Mario Carneiro (Feb 15 2019 at 10:17):

and this is just for proving little FOL goals

Mario Carneiro (Feb 15 2019 at 10:19):

Of course once we move to mathlib the common tactic list gets a bit different: use, rintro, rcases, tauto,tidy,finish

Mario Carneiro (Feb 15 2019 at 10:21):

oh also have and show of course. I'm teaching this stuff and I can't even remember them all

Kenny Lau (Feb 15 2019 at 10:21):

you mean simp only, use, rintro, rcases, rw

Mario Carneiro (Feb 15 2019 at 10:21):

oh right rw and simp too

Kenny Lau (Feb 15 2019 at 10:22):

simp doesn't exist

Mario Carneiro (Feb 15 2019 at 10:22):

These are new kids, no way I can explain compile times

Mario Carneiro (Feb 15 2019 at 10:22):

better to have blasty stuff first

Mario Carneiro (Feb 15 2019 at 10:23):

seriously the information overload is palpable

Kevin Buzzard (Feb 15 2019 at 10:29):

They're mathematicians in some cases, so the blasty stuff includes linarith, norm_num and ring

Kevin Buzzard (Feb 15 2019 at 10:29):

all three of those are a very small subset of by schoolkid

Kevin Buzzard (Feb 15 2019 at 10:30):

I don't know if the word has the same connotations in the US -- in the UK this means "someone who has not gone to university yet and is still in the K-12 school system"

Kevin Buzzard (Feb 15 2019 at 10:30):

but they learn (a+b)^3=a^3+... there

Mario Carneiro (Feb 15 2019 at 10:31):

I'm not sure what we will do about teaching the heavy hitter tactics. We've only discussed simp so far

Kevin Buzzard (Feb 15 2019 at 10:31):

I'm not talking about the lies they learn, like the definition of sine and that its derivative is cosine, I'm talking about the facts they do learn which we allow them to use at university like the expansion of (a+b)^3

Kevin Buzzard (Feb 15 2019 at 10:32):

In fact as a student perhaps it's really bewildering -- for them (a+b)^3=a^3+... and derivative of sine is cosine are both "stuff we learnt at school", so how some one of them is valid in the analysis class and the other one suddenly isn't?

Mario Carneiro (Feb 15 2019 at 10:33):

I'm not sure what you're getting at

Mario Carneiro (Feb 15 2019 at 10:34):

We're going bottom up. One assignment this week was proving log (x * y) = log x + log y given exp (x + y) = exp x * exp y and log/exp inverse laws

Mario Carneiro (Feb 15 2019 at 10:34):

it's all calc blocks and rw

Mario Carneiro (Feb 15 2019 at 10:34):

no blasty stuff

Kevin Buzzard (Feb 15 2019 at 10:34):

I'm just thinking about how my own students must be confused when they come to university, because we tell them to unlearn a random subset of what they have learnt

Kenny Lau (Feb 15 2019 at 10:35):

to learn something you must first unlearn it

Mario Carneiro (Feb 15 2019 at 10:35):

since we tightly control the facts they have available to use, it's clear what is and isn't usable for the proof

Kevin Buzzard (Feb 15 2019 at 10:35):

Isn't there a chicken and egg problem there?

Kevin Buzzard (Feb 15 2019 at 10:36):

We're going bottom up. One assignment this week was proving log (x * y) = log x + log y given exp (x + y) = exp x * exp y and log/exp inverse laws

That's a nice question. Are your problem sets available online? It's time we made a resource for this stuff. Basic Lean questions. In the teaching thread maybe.

Mario Carneiro (Feb 15 2019 at 10:36):

I think starting from all of math and whittling down to things that are in mathlib seems like an exercise in frustration, but probably is the path that the advanced mathematicans go through in coming to lean

Mario Carneiro (Feb 15 2019 at 10:37):

Not online, on Cocalc. @Jeremy Avigad is leading the class, ask him

Mario Carneiro (Feb 15 2019 at 10:37):

I'm just the TA


Last updated: Dec 20 2023 at 11:08 UTC