[Merged by Bors] - feat: Fintype deriving handler
#3198
Conversation
| return true | ||
|
|
||
| /-- Derive a `Fintype` instance for enum types. These come with a `toCtorIdx` function. | ||
| The strategy is to (1) create a list `enumList` of all the constructors, (2) prove that this |
There was a problem hiding this comment.
Perhaps it would make sense to implement a FinEnum instance derive handler here too?
There was a problem hiding this comment.
I'd suggest making a separate deriving handler for this, since the List isn't so useful for the equivalence.
Note that there's already an inverse function for toCtrIdx defined by the DecidableEq deriving handler for enum types. https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Deriving/DecEq.lean#L110
There was a problem hiding this comment.
Is the list useful for anything? Why do we want a special path for enum types?
There was a problem hiding this comment.
It's significantly less expensive in both space and time, if we're going to do any computations with it. 63 lines seems like a small price to pay for that.
There was a problem hiding this comment.
When is the cost paid for computing the elements of a fintype? Every time you use finset.sum, or just once when the instance is added to the environment?
There was a problem hiding this comment.
It depends on what kind of computing you're doing. I think if it's in the compiled code, an instance with no arguments (like for types with no parameters) will be evaluated at program initialization. But otherwise, for VM evaluation or symbolic evaluation (like for Decidable-like inference or fin_cases) I think it's more like the elements get computed from scratch at every use.
| so mapping to and from `Cᵢ` requires looking through `i` levels of `Sum` constructors. | ||
| Ignoring time spent looking through these constructors, the construction of `Finset.univ` | ||
| contributes linear time with respect to the cardinality of the type since the instances | ||
| involved compute the underlying `List` for the `Finset` as `l₁ ++ (l₂ ++ (⋯ ++ lₙ))` with |
There was a problem hiding this comment.
What makes l₁ ++ (l₂ ++ (⋯ ++ lₙ)) quadratic complexity? Isn't it
There was a problem hiding this comment.
List.append agrees that xs ++ ys is
There was a problem hiding this comment.
Right, the point is that l₁ ++ (l₂ ++ (⋯ ++ lₙ)) takes linear time in the total length of the resulting list. ((l₁ ++ l₂) ++ ⋯ ) ++ lₙ would be quadratic time, which is why it's associated the way it is.
But, there's quadratic time (with respect to n) that's still there from needing to deal with all the Sum constructors. Fintype.ofEquiv maps over the resulting list.
Mathlib/Tactic/DeriveFintype.lean
Outdated
| | c (x : Fin n) : Fin x → foo n α | ||
| | d : Bool → α → foo n α | ||
| ``` | ||
| the proxy type it generates is `Unit ⊕ Bool ⊕ (x : Fin n) × Fin x ⊕ (_ : Bool) × α` and |
There was a problem hiding this comment.
Can we have proxy_type% to generate this term?
There was a problem hiding this comment.
I'm not sure if proxy_type% is very useful, since the type is meaningless without the equivalence. Everything's factored out where it'd be easy to add if anyone wants it, but I'd rather not add it without a clear need for it.
semorrison
added
the
merge-conflict
…lib4 into kmill_deriving_fintype
semorrison
removed
the
merge-conflict
|
bors merge |
github-actions
bot
added
ready-to-merge
Adds a handler to derive `Fintype` instances for non-recursive types without indices. Has an optimized implementation for enum types as well where it produces an underlying list (`enumList`) of its elements. For non-enum types, the `Fintype` instance comes from an equivalence to a "proxy type" made from `Sum`, `Sigma`, `PLift`, `Empty`, and `Unit`. Also adds a `derive_fintype%` elaborator to derive `Fintype` instances in the middle of terms. This is useful in case, for example, a `Fintype` instance needs an additional `DecidableEq` instance. This elaborator is defined in terms of a `proxy_equiv%` elaborator that constructs the proxy type and the the equivalence from it. The machinery for `proxy_equiv%` is made to be somewhat configurable.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Fintype deriving handlerFintype deriving handler
Adds a handler to derive `Fintype` instances for non-recursive types without indices. Has an optimized implementation for enum types as well where it produces an underlying list (`enumList`) of its elements. For non-enum types, the `Fintype` instance comes from an equivalence to a "proxy type" made from `Sum`, `Sigma`, `PLift`, `Empty`, and `Unit`. Also adds a `derive_fintype%` elaborator to derive `Fintype` instances in the middle of terms. This is useful in case, for example, a `Fintype` instance needs an additional `DecidableEq` instance. This elaborator is defined in terms of a `proxy_equiv%` elaborator that constructs the proxy type and the the equivalence from it. The machinery for `proxy_equiv%` is made to be somewhat configurable.
Adds a handler to derive
Fintypeinstances for non-recursive types without indices. Has an optimized implementation for enum types as well where it produces an underlying list (enumList) of its elements. For non-enum types, theFintypeinstance comes from an equivalence to a "proxy type" made fromSum,Sigma,PLift,Empty, andUnit.Also adds a
derive_fintype%elaborator to deriveFintypeinstances in the middle of terms. This is useful in case, for example, aFintypeinstance needs an additionalDecidableEqinstance. This elaborator is defined in terms of aproxy_equiv%elaborator that constructs the proxy type and the the equivalence from it. The machinery forproxy_equiv%is made to be somewhat configurable.