derive_fintype

Stream: mathlib4

[Heather Macbeth]

The mathlib3 file tactic.derive_fintype doesn't seem to be on the porting status list -- I guess because it's in the tactic directory -- but I also don't see it as a task on the tactic porting issue (!4#430). Has this slipped through the cracks? Or is this functionality provided differently in Lean 4 -- if so, what do I need to import?

[Scott Morrison]

I think this has slipped through the cracks. If anyone wants to look at this, there are lots of examples in core Lean, in src/Lean/Elab/Deriving/*.

[Scott Morrison]

I would like a ToExpr derive handler, too.

[Adam Topaz]

While we're at it, a ConcreteCategory deriving handler is missing as well.

[Adam Topaz]

or at least it didn't work in !4#3105

[Adam Topaz]

where can I find an up-to-date tactic porting status list?

[Adam Topaz]

I'm actually confused now about how things like deriving LargeCategory work. Where can I find the deriving handler for that?

[Eric Wieser]

I think that's just the delta reduction handler.

[Eric Wieser]

In Lean 3, I think

@[derive random_class]
def foo := bar

falls back to "just unfold foo and use the instances on bar"

[Adam Topaz]

yeah, that's what it should be, but I'm surprised this didn't work for ConcreteCategory in the PR I mentioned above.

[Adam Topaz]

Do you know where I can find the code for this in lean4?

[Mario Carneiro]

delta deriving doesn't work in lean 4

[Mario Carneiro]

the issue is that delta deriving applies to arbitrary typeclasses and the deriving handler framework for lean 4 wants to key on specific typeclasses

[Eric Wieser]

Does the deriving syntax even exist for def?

[Mario Carneiro]

it does

[Adam Topaz]

So where can I find the deriving handler for LargeCategory? I looked in mathlib4 and in lean4 in the folder Scott mentioned, but didn’t find it. Any pointers @Mario Carneiro ?

[Mario Carneiro]

a grep for deriving LargeCategory in mathlib4 turns up empty

[Mario Carneiro]

from what I can tell, every delta derive in mathlib4 is commented out

[Adam Topaz]

@Mario Carneiro https://github.com/leanprover-community/mathlib4/blob/13e2b8c83e2f62854bb14ce6813af030061a8de9/Mathlib/Algebra/Category/Ring/Basic.lean#L80

[Adam Topaz]

not in master, but it works.

[Mario Carneiro]

Aha, it appears that delta deriving has been hard-coded into the derive framework:
https://github.com/leanprover/lean4/blob/583e023/src/Lean/Elab/Deriving/Basic.lean#L107-L109

[Mario Carneiro]

The second limitation of lean 4 derive is that it applies to classes given as Name rather than Expr, which means you can't do e.g. @[derive module real]. My guess is that this is the problem for ConcreteCategory, if it isn't a unary typeclass then it won't be triggered

[Mario Carneiro]

It looks like the real error is a suppressed error message of the form

failed to synthesize
  @ConcreteCategory (Bundled Semiring)

[Adam Topaz]

Ah! okay I see. Thanks!

[Mario Carneiro]

I think the @ there is load-bearing: it really is ConcreteCategory applied only to its first argument, and I can confirm that the typeclass search fails:

#synth @ConcreteCategory (Bundled Semiring) -- fails
#synth ConcreteCategory (Bundled Semiring) -- ok

[Mario Carneiro]

in other words, this is not really a unary typeclass as far as lean is concerned

[Adam Topaz]

okay, so perhaps I'll try to write a custom derive handler for ConcreteCategory

[Mario Carneiro]

this particular example looks like a bug in processDefDeriving

[Mario Carneiro]

it's attempting to synthesize an instance of something which isn't even a type

[Kyle Miller]

@Heather Macbeth mathlib4#3198

[Scott Morrison]

@Kyle Miller , could we factor out the construction of the equivalence with the proxy type, as a separate term elaborator / tactic? It seems exposing this part would be very useful for other derive handlers.

[Eric Wieser]

Does it make sense to skip the sum/sigma construction and jump directly to making the w-type equivalence?

[Kyle Miller]

@Scott Morrison Sure, now we have a proxy_equiv% elaborator. For example, proxy_equiv% (Option α) : Unit ⊕ α ≃ Option α

[Kyle Miller]

@Eric Wieser The idea with using a sum/sigma construction is to make use of mathlib's pre-existing Fintype instances. There don't seem to be any for w-types.

[Eric Wieser]

Ah, that makes sense

[Eric Wieser]

A related idea would be to have a variant that inserts Lex terms to help build a LinearOrder (Lex MyType) instance

[Eric Wieser]

That is, allow hooks of some kind to allow Sum and Sigma to be swapped for types with other properties

[Scott Morrison]

I wonder if you can make a cheap ToExpr derive handler out of this. To turn an x : X into an expression, run let e ← toExpr ((proxy_equiv% _) x), and then return q((proxy_equiv% _).symm $e). Maybe a round of simplification to unfold the definition of the equiv, and you'd actually get what you want.