Typeclass automatic synthesising for statements a la op...

Stream: mathlib4

[Wrenna Robson]

A question that arose while I was working on #9145: so if you have i j : Fin (n + 1), with i ≠ j, then it follows that n ≠ 0, and so in particular you have an instance of NeZero n. This is relevant because, essentially, given i j : Fin (n + 1), with i ≠ j, 0 : Fin n always makes sense. This does come up somewhere: in particular, sometimes in #9145 I have i j : Fin (n + 1), with i ≠ j, and I want to use 0 : Fin n in the statement, and I couldn't.

What I'm wondering is how to efficiently and elegantly use this fact: I don't think I can use optParam in the same way that I might if I wanted a proof of n ≠ 0 in the statement, because what I want is a typeclass synthesised from a hypothesis. Is that even possible?

Alternatively, in some ways this reduces to the two following facts:

• Given i j : Fin (n + 1), with i ≠ j, I can always produce some p: Fin n.
• If I have p : Fin n, the notation 0 : Fin n always makes sense (it may or may not be p).

So can I do either of those more elegantly? Do "typeclasses automatically synthesised from hypotheses" even make sense?

[Notification Bot]

Wrenna Robson has marked this topic as resolved.

[Notification Bot]

Wrenna Robson has marked this topic as unresolved.

[Kyle Miller]

Typeclass synthesis doesn't look at hypotheses, but something you do is make a function neZeroOfFinNe : {i j : Fin (n + 1)} -> i ≠ j -> NeZero n and then given h : i ≠ j write have := neZeroOfFinNe h either in your proof or as a line of a definition.

[Wrenna Robson]

Hmm, how do you fit it into a definition? Like that can be part of a statement?

[Kyle Miller]

You can use haveI := neZeroOfFinNe h; ... in a statement and have it be eliminated from the type. You can't use it for variables before the colon though.

[Wrenna Robson]

Thanks, that is perfect.

[Wrenna Robson]

Any suggestions where such a neZeroOfFinNe would go? Data/Fin/Basic?

[Emilie (Shad Amethyst)]

I would also have something of the likes of instance neZero_of_nonTrivial_fin_succ (nt : Nontrivial (Fin n.succ)) : NeZero n

[Emilie (Shad Amethyst)]

You also have that NeZero n ↔ NonEmpty (Fin n) ↔ Nontrivial (Fin n.succ), though I don't know if the typeclass solver can handle loops. The left equivalence is covered by docs#Fin.pos_iff_nonempty already and the right equivalence can be derived from docs#Fin.nontrivial_iff_two_le

[Wrenna Robson]

If we had instance neZero_of_nonTrivial_fin_succ [Nontrivial (Fin n.succ)] : NeZero n, would that then let the solver do the inference (taking it as a typeclass)?

I suspect what you want is instance [Nontrivial (Fin n.succ)] : NonEmpty (Fin n) and instance [NonEmpty (Fin n)] : NeZero n, and that way avoid the loop in the typeclass solver.

[Eric Wieser]

That second instance already exists in reverse

[Wrenna Robson]

Oops. I knew we had docs#Fin.pos_iff_nonempty but didn't realise we had the instance.

[Wrenna Robson]

That feels like... the less useful order in some ways? Idk.

[Eric Wieser]

Well, it follows from the fact that when n is not zero, there is a Zero

[Wrenna Robson]

Indeed.

[Wrenna Robson]

It's just one of those slightly troublesome things where frankly it's basically trivial except somehow it isn't.

[Wrenna Robson]

Annoyingly it's slightly asymmetrical as well, in the sense that you don't have a similar issue for last (precisely because last n is in Fin (n +1), I.e. there's no analogy of "NeZero means you have a last".

[Eric Wieser]

I think generalizing last in that way spoiled be reasonable?

[Eric Wieser]

Oh, I guess it maybe ends up with a bad defeq

[Wrenna Robson]

Yeah the issue is, what would you define last 0 as? In a sense the better notation is arguably \top

[Wrenna Robson]

Though obviously in general using \bot instead of 0 would be... eccentric.

[Wrenna Robson]

Of course you could define last : Fin n as rev 0.

[Eric Wieser]

Wrenna Robson said:

Yeah the issue is, what would you define last 0 as?

False.elim _

[Wrenna Robson]

Hmm I'm not sure that works.

[Emilie (Shad Amethyst)]

It's the equivalent of unreachable!() in rust

[Wrenna Robson]

right...

[Mario Carneiro]

the equivalent of unreachable!() in rust is unreachable!, the equivalent of False.elim in rust is match x {}

[Wrenna Robson]

I just don't quite follow what you're eliminating.

[Mario Carneiro]

Fin0.elim is like False.elim but it takes an element of Fin 0 instead

[Wrenna Robson]

Right.

[Mario Carneiro]

you can also just pattern match on it, the compiler knows it is empty

[Wrenna Robson]

But I asked what you'd define last 0 as if you made last n a member of Fin n.

[Mario Carneiro]

oh, I was thinking this was a function that takes a Fin n, of course if it's just producing a Fin n from nothing then you are in trouble for n = 0

[Wrenna Robson]

Indeed. But you can make it work if you add a [NeZero n] typeclass.

[Wrenna Robson]

I was just remarking that that isn't currently an option.

[Emilie (Shad Amethyst)]

An instance of instance [NeZero n] : OrderTop (Fin n) would be nice to have, I think.
Also, speaking of option, you could wrap the result in an Option

[Wrenna Robson]

Yeah I don't know if the OrderTop instance currently works for that, I think we just have the one for n +1. It can be a bit of a pain writing lemmas (in the zero case) because I never know if I should have two versions or just the [NeZero] one.

[Yaël Dillies]

We agreed a long time ago that instances about Fin (n + 1) should instead be instances about Fin n where NeZero n. Feel free to fix whatever instances are not following that rule.

[Wrenna Robson]

Oh really?

[Wrenna Robson]

Then I think the best strategy would be to change last n so that instead it's just called last, make it a member of Fin n, and define it as Fin.rev 0 as a bonus.

[Yaël Dillies]

Why not just use ⊤ then?

[Wrenna Robson]

I was just typing that!

[Wrenna Robson]

Well, I don't know why we decided to have last in the first place.

[Yaël Dillies]

I think it's because it's easier to type (last n) than (⊤ : Fin (n + 1)) when the expected type is unavailable.

[Wrenna Robson]

As I was saying yesterday, arguably one could also use \bot instead of 0 in a lot of places but that is a little eccentric.

[Yaël Dillies]

Yeah but that's a different situation: 0 has an algebraic meaning that last n doesn't have.

[Wrenna Robson]

Yaël Dillies said:

I think it's because it's easier to type (last n) than (⊤ : Fin (n + 1)) when the expected type is unavailable.

I suppose you could define last n as the same, make the n explicit.

[Wrenna Robson]

Yaël Dillies said:

Yeah but that's a different situation: 0 has an algebraic meaning that last n doesn't have.

Yes I agree - but we tend to use 0 even in the order-theoretic places for Fin.

[Wrenna Robson]

Which I'm not necessarily disagreeing with, to be clear.

[Wrenna Robson]

But e.g. Fin.cases and Fin.lastCases are somewhat more about ordering than they are about algebraic properties.

[Yaël Dillies]

I'm just arguing that 0 and last n can't be thought about symmetrically because they have differing algebraic relevance (even though they have identical order theoretic relevance).

[Wrenna Robson]

Ah I see what you mean

[Wrenna Robson]

Yes, indeed. I suppose you could talk about the algebraic properties of last n (for one thing, it's the additive inverse of 1...) but I can't ever see why that would be easier.

[Yaël Dillies]

Well that wouldn't be last n, right? That would be -1. Spelling matters.

[Wrenna Robson]

True, true.

[Wrenna Robson]

As you say, 0 is a bit special.

[Mario Carneiro]

-1 is a bit pathological though, because it does something weird on Fin 1

[Wrenna Robson]

Does it?

[Wrenna Robson]

I mean it's also 0, obviously.

[Yaël Dillies]

How so? It's still the additive inverse of 1.

[Mario Carneiro]

well 1 : Fin n is 1 for every n except for n = 1, where it is 0 instead

[Wrenna Robson]

yes I'm not quite sure why it's not also 1.

[Yaël Dillies]

You mean (1 : Fin n).val.

[Wrenna Robson]

Oh I see what you mean.

[Mario Carneiro]

It works out up to (propositional) equality, but it's less uniform compared to last which is n - 1 for every n > 0

[Wrenna Robson]

Yes that can occasionally trip one up. Clearly the solution is to start things at Fin 2. Fin 1 and Fin 0 are silly types: let's never go there ;)

[Wrenna Robson]

Mario Carneiro said:

It works out up to (propositional) equality, but it's less uniform compared to last which is n - 1 for every n > 0

Yes in this sense last is closer to 0 (which makes sense!) in that it's only pathological at 0 (where nothing exists anyway).

[Mario Carneiro]

too bad we don't have a ~ operator

[Mario Carneiro]

does ~~~0 work?

[Wrenna Robson]

as I say this is why I think I like rev 0 as its definition.

[Wrenna Robson]

What would ~ do?

[Mario Carneiro]

rev

[Wrenna Robson]

Right. Yeah, would be nice.

[Mario Carneiro]

I mean it as in the C bitwise negation operator

[Mario Carneiro]

which is -n-1

[Wrenna Robson]

Right right. Do we use that notation for anything?

[Mario Carneiro]

bitwise ops

[Wrenna Robson]

Which... I think this would be consistent with (on Fin (2^m)?)

[Wrenna Robson]

@Yaël Dillies yeah it looks like the bounded order instance on Fin is for Fin (n + 1) instead of NeZero n. That wants changing, right?

[Wrenna Robson]

Unfortunately the definition of last is in std so it can't really change. We could have a last' that works more as we might want...

[Yaël Dillies]

NeZero might make it to Std eventually

[Wrenna Robson]

That would be nice