BitVec Fintype instance

Stream: Is there code for X?

[Ashley Blacquiere]

I have the following Lean3 code

instance fintype : Π (n : ℕ), fintype (bitvec n) := by {intro n, exact vector.fintype}

which I've ported to Lean4 as follows:

instance fintype : ∀ n : ℕ, Fintype (BitVec n) := by intro n; exact Vector.fintype

However, BitVec is no longer reduced to Vector, so the ported code doesn't work as-is. Is there any code that supports BitVec as an instance of Fintype in some capacity?

[Eric Wieser]

deriving instance Fintype for BitVec will do it

[Ashley Blacquiere]

Hm... default handlers have not been implemented yet, class: 'Fintype' types: [BitVec]. There is a reference to this error in Functional Programming in Lean, but I'm otherwise not sure what/where I would find said handlers.

[Eric Wieser]

You are missing an import, but I cannot tell you which one because you didn't tell me which ones you have already! (imports are an important part of #mwe s)

[Eric Wieser]

Adding import Mathlib.Tactic fixes it, but is surely overkill

[Ashley Blacquiere]

MWE is this:

import Mathlib.Probability.Distributions.Uniform

deriving instance Fintype for BitVec
noncomputable def uniformBitvec (n : ℕ) [Fintype (BitVec n)] : PMF (BitVec n) := PMF.uniformOfFintype (BitVec n)

[Ashley Blacquiere]

Does this help track down where the handler is captured along Mathlib.tactic?

[Meta.synthInstance] ✅ Fintype (BitVec n) ▼
  [] new goal Fintype (BitVec n) ▼
    [instances] #[@IsSimpleOrder.instFintype, @Unique.fintype, BitVec.fintype, @instFintypeBitVec, inst✝]
  [] ✅ apply inst✝ to Fintype (BitVec n) ▼
    [tryResolve] ✅ Fintype (BitVec n) ≟ Fintype (BitVec n)
  [] result inst✝

[Meta.synthInstance] ✅ Nonempty (BitVec n) ▼
  [] new goal Nonempty (BitVec n) ▼
    [instances] #[@Zero.instNonempty, @One.instNonempty, infSet_to_nonempty, supSet_to_nonempty, @IrreducibleSpace.toNonempty, @ConnectedSpace.toNonempty, top_nonempty, bot_nonempty, @AddTorsor.nonempty, @Nontrivial.to_nonempty, @instNonempty, @instForAllNonemptyNonempty]
  [] ❌ apply @instForAllNonemptyNonempty to Nonempty (BitVec n) ▼
    [tryResolve] ❌ Nonempty (BitVec n) ≟ Nonempty (?m.2675 ?m.2676)
  [] ✅ apply @instNonempty to Nonempty (BitVec n) ▼
    [tryResolve] ✅ Nonempty (BitVec n) ≟ Nonempty (BitVec n)
    [] new goal Inhabited (BitVec n) ▶
  [] ✅ apply @BitVec.instInhabitedBitVec to Inhabited (BitVec n) ▼
    [tryResolve] ✅ Inhabited (BitVec n) ≟ Inhabited (BitVec n)
  [resume] propagating Inhabited (BitVec n) to subgoal Inhabited (BitVec n) of Nonempty (BitVec n) ▶
  [] result instNonempty

[Eric Wieser]

You need to add import Mathlib.Tactic.DeriveFintype

[Eric Wieser]

@Kyle Miller, do you think it would be easy enough to improve the error message from

default handlers have not been implemented yet, class: 'Fintype' types: [BitVec]

to something like

No handled found for class: 'Fintype' types: [BitVec]. Perhaps you are missing an import?