having existential statements

Stream: general

[Scott Morrison]

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]

what is the goal?

[Rob Lewis]

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

[Mario Carneiro]

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]

Mario is really getting old

[Rob Lewis]

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

[Mario Carneiro]

I went for coffee :)

[Patrick Massot]

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]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

We haven't started on mathlib yet

[Johan Commelin]

Poor students.

[Mario Carneiro]

the head exploding will only get worse

[Mario Carneiro]

also left, right, constructor

[Mario Carneiro]

and this is just for proving little FOL goals

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

oh right rw and simp too

[Kenny Lau]

simp doesn't exist

[Mario Carneiro]

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

[Mario Carneiro]

better to have blasty stuff first

[Mario Carneiro]

seriously the information overload is palpable

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

I'm not sure what you're getting at

[Mario Carneiro]

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]

it's all calc blocks and rw

[Mario Carneiro]

no blasty stuff

[Kevin Buzzard]

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]

to learn something you must first unlearn it

[Mario Carneiro]

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]

Isn't there a chicken and egg problem there?

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

I'm just the TA