Typeclass inference on option.rec

Stream: general

[Pierre-Alexandre Bazin]

universes u v
variables {ι : Type u} {α : Type v} {β : ι → Type v}

section
variables [has_zero α] [Π i, has_zero (β i)]
instance inst0 : Π i, has_zero (option.rec α β i) :=
λ i, option.rec infer_instance infer_instance i --doesn't find it otherwise
end

section
variables [add_monoid α] [Π i, add_monoid (β i)]
instance inst : Π i, add_monoid (option.rec α β i) :=
λ i, option.rec infer_instance infer_instance i --doesn't find it otherwise

instance inst' : add_monoid (Π₀ i, option.rec α β i) :=
@dfinsupp.add_monoid (option ι) (λ i, option.rec α β i) inst --doesn't work
end

The reason it doesn't work is because the first Π₀ i, option.rec α β iis actually @dfinsupp (option ι) (λ i, option.rec α β i) inst0,
whereas @dfinsupp.add_monoid (option ι) (λ i, option.rec α β i) inst actually gives an add_monoid structure to
@dfinsupp (option ι) (λ i, option.rec α β i) (λ i, @add_monoid.to_has_zero _ (inst i)). (actually there's an extra step between add_monoid and has_zero but it doesn't matter)

The two Π i, has_zero (option.rec α β i) instances should be defeq but it doesn't see it (probably because it need some helper instances to build these). How can I avoid getting this error ?

[Eric Wieser]

I don't think using recursors to define typeclass instances is safe

[Pierre-Alexandre Bazin]

but how can I avoid this ?

[Eric Wieser]

The problem is roughly the same as the fact that (λ n, 2 * nat.rec x f n) is not the same as (λ n, nat.rec (2 * x) (2 * f) n)

[Eric Wieser]

Lean can't unfold the recursor unless it knows i

[Eric Wieser]

Which means it can't unify diamonds in the typeclass heirarchy for a general i

[Eric Wieser]

I tried something similar with sum.elim a while ago, see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Instances.20on.20.60sum.2Eelim.20A.20B.20i.60/near/218484619

[Pierre-Alexandre Bazin]

this is indeed exactly the problem, as unfolding everything it's basically λ i, add_comm_monoid.to_has_zero (option.rec α β i) vs λ i, option.rec (add_comm_monoid.to_has_zero α) (add_comm_monoid.to_has_zero β) i

[Pierre-Alexandre Bazin]

But I don't know how I could avoid the use of option.rec

[Eric Wieser]

Can you give some more context?

[Pierre-Alexandre Bazin]

I'm trying to add one term to a dfinsupp/direct sum

[Eric Wieser]

Once way you could avoid this is to use option.rec to define has_zero, has_one, etc:

instance : has_zero (option.rec α β i) := { zero := option.rec 0 0 i }

[Eric Wieser]

And then build add_monoid by using option.rec in each proof field

[Pierre-Alexandre Bazin]

so I have a noncomputable def equiv_prod_dfinsupp : (Π₀ i, option.rec α β i) ≃ α × Π₀ i, β i := ... and I want to extend it to an ≃+

[Eric Wieser]

The key thing is to push the option.rec inside all the constructors

[Eric Wieser]

(Π₀ i : fin n.succ, α i) ≃ α × Π₀ i : fin n, α i.succ would be one way out

[Eric Wieser]

Or (Π₀ i : option X, α i) ≃ α none × Π₀ i : X, α (some i)

[Pierre-Alexandre Bazin]

the latter seems better because it also works with infinite direct sums

[Eric Wieser]

I'd go for that option first, and come back to option.rec instances if that has issues

[Pierre-Alexandre Bazin]

(but actually the former is my use case so I was considering doing only this first at some point)