rcases quotient

Stream: metaprogramming / tactics

[Yury G. Kudryashov]

@Mario Carneiro @Floris van Doorn How hard would it be to make rcases use custom function instead of quot.mk? Can we reuse the same trick tactic#simps uses to get custom functions instead of projections? It would be nice to get (a) custom mk if exists (e.g., multisets should use coe, and cardinals should use cardinal.mk); (b) quotient.mk if possible; (c) quot.mk if (a) and (b) fail.

[Mario Carneiro]

Ideally, we would do whnf on the type in stages, unfolding one definition at a time and looking up to see if any of the intermediate types have a custom recursor (let's say we have a data structure to track these by type name). If it doesn't, we unfold and try again, until we get to quot or an inductive type at which point we use the builtin recursor

[Mario Carneiro]

I think I can see how to do this using delta and whnf_no_delta, but the other problem is that doing cases with a custom recursor doesn't always turn out well

[Yury G. Kudryashov]

Why do you need a custom recursor?

[Mario Carneiro]

isn't that the proposal?

[Mario Carneiro]

rcases never directly constructs tuples or constructor applications itself

[Mario Carneiro]

that is all a consequence of the foo.cases_on theorem

[Yury G. Kudryashov]

I thought about something like def cardinal.rcases_quot := cardinal.mk. It seems that my understanding of how it works was very wrong.

[Mario Carneiro]

I'm thinking something like this:

namespace cardinal
@[rcases]
protected def cases_on {β : cardinal → Prop} : ∀ q, (∀ (α : Type*), β (mk α)) → β q :=
@quotient.induction_on _ cardinal.is_equivalent _

[Mario Carneiro]

and then assuming we can teach cases to use this theorem instead of the default one we're set

[Mario Carneiro]

In the case of quotient-like theorems, we're already doing something custom to get this quot behavior, and we call induction internally (which has a slot for the custom induction principle to use), so that's okay. For inductive types, though, we call cases_core which has no such option

[Yury G. Kudryashov]

If you can quickly fix quotient types, this would be already a nice improvement, even without custom handling of inductive types.
P.S.: I hope, some day we'll have a way to override the default induction principle for a type (I mean, make induction automatically use finset.induction_on for finsets etc).

[Yury G. Kudryashov]

But I'm not sure that it makes sense to do it in Lean 3.

[Johan Commelin]

Yeah, it would be great to use ideal.quotient.mk, so that you have a ring hom applied to x, instead of some low-level quotient constructor.