Zulip Chat Archive

Stream: new members

Topic: Coercing to option


view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:14):

Where can I find lemmas about coercing to option (e.g. to option ℕ)? I want basic things like ↑(n - m) = ↑n - ↑m.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:15):

what does subtraction mean?

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:15):

I don't think option has a has_sub instance

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:17):

But option N does.

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:18):

Oh wait, you mean ↑n - ↑m won't be defined at all.

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:18):

What about something like 1 + ↑(n - 1) = ↑n? That's what I actually need to prove.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:18):

option doesn't have an add or 1 either

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:18):

what are you doing?

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:19):

Degrees of polynomials.

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:19):

You can add degrees of polynomials, but they're defined via option.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:19):

Isn't it with_bot N or something?

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:19):

Yeah.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:19):

that's a different thing

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:20):

Ok, because with_bot has additional structure.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:20):

with_bot has an addition, option doesn't

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:20):

But how do I coerce to with_bot?

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:20):

I mean, are there lemmas about it in mathlib?

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:22):

I think you want with_bot.coe_add

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:22):

Ah, I see.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:22):

the lemmas are in algebra.ordered_group

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:22):

but if n : nat then 1 + \u(n - 1) = \u n is false at 0

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 15 2019 at 21:23):

Yeah, I have an n > 1 hypothesis, that's alright.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:23):

if you cases on n then the zero case is impossible and the succ case is by refl

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:24):

oh wait, not refl, you have to commute the 1+ first

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 21:36):

that's a different thing

It's a definitionally equal thing. Definitional equality is a subtle beast. At times you should just treat definitionally equal things as the same, but at other times you shouldn't, and this is one of those times. This came up today in my M1P1 talk. We tried linarith to finish the proof that any two limits of a sequence were equal, and it failed, because we had hypotheses of the form l < m -> false. When we changed them to the definitionally equal \not (l < m) linarith suddenly worked! What is going on, I guess, is that linarith is looking at what "kind" of an expression it can see, and l < m -> false is "just some function" to linarith, whereas \not (l < m) is "a linear inequality that I can use". Similarly type class inference for + is going to trigger on with_bot nat but perhaps not on option nat even though they're definitionally equal. I hope I've got this mostly right. These things might be definitionally equal, but they are different expressions so tactics or other bits of Lean might treat them in different ways. For unification they will be the same but for rewrites they won't. etc etc.


Last updated: May 11 2021 at 23:11 UTC