Coercing to option

Stream: new members

[Abhimanyu Pallavi Sudhir]

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

[Mario Carneiro]

what does subtraction mean?

[Mario Carneiro]

I don't think option has a has_sub instance

[Abhimanyu Pallavi Sudhir]

But option N does.

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Mario Carneiro]

option doesn't have an add or 1 either

[Mario Carneiro]

what are you doing?

[Abhimanyu Pallavi Sudhir]

Degrees of polynomials.

[Abhimanyu Pallavi Sudhir]

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

[Mario Carneiro]

Isn't it with_bot N or something?

[Abhimanyu Pallavi Sudhir]

Yeah.

[Mario Carneiro]

that's a different thing

[Abhimanyu Pallavi Sudhir]

Ok, because with_bot has additional structure.

[Mario Carneiro]

with_bot has an addition, option doesn't

[Abhimanyu Pallavi Sudhir]

But how do I coerce to with_bot?

[Abhimanyu Pallavi Sudhir]

I mean, are there lemmas about it in mathlib?

[Mario Carneiro]

I think you want with_bot.coe_add

[Abhimanyu Pallavi Sudhir]

Ah, I see.

[Mario Carneiro]

the lemmas are in algebra.ordered_group

[Mario Carneiro]

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

[Abhimanyu Pallavi Sudhir]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.