Decidability nightmare

Stream: general

[Sebastien Gouezel]

I should have solved a goal, but this doesn't work because decidability instances are not the same. I have tried to be rather careful, avoiding open_locale classical, but still here is what I get

invalid type ascription, term has type
  @disjoint (finset (Π (a : ι), a ∈ @finset.univ ι _inst_8 → (λ (a : ι), α a) a))
    (@finset.lattice.semilattice_inf_bot (Π (a : ι), a ∈ @finset.univ ι _inst_8 → (λ (a : ι), α a) a)
       (λ (a b : Π (a : ι), a ∈ @finset.univ ι _inst_8 → (λ (a : ι), α a) a),
          @finset.decidable_eq_pi_finset ι (@finset.univ ι _inst_8) (λ (a : ι), (λ (a : ι), α a) a)
            (λ (a : ι) (a_1 b : (λ (a : ι), α a) a), (λ (i₀ : ι) (a b : α i₀), _inst_10 i₀ a b) a a_1 b)
            a
            b))
    (@finset.pi ι (λ (a : ι), (λ (a : ι), α a) a) (λ (a b : ι), (λ (a b : ι), _inst_9 a b) a b)
       (@finset.univ ι _inst_8)
       B)
    (@finset.pi ι (λ (a : ι), (λ (a : ι), α a) a) (λ (a b : ι), (λ (a b : ι), _inst_9 a b) a b)
       (@finset.univ ι _inst_8)
       C)
but is expected to have type
  @disjoint (finset (Π (a : ι), a ∈ @finset.univ ι _inst_8 → α a))
    (@finset.lattice.semilattice_inf_bot (Π (a : ι), a ∈ @finset.univ ι _inst_8 → α a)
       (λ (a b : Π (a : ι), a ∈ @finset.univ ι _inst_8 → α a),
          @fintype.decidable_pi_fintype ι (λ (a : ι), a ∈ @finset.univ ι _inst_8 → α a) _inst_8
            (λ (a : ι) (a_1 b : a ∈ @finset.univ ι _inst_8 → α a),
               @function.decidable_eq_pfun (a ∈ @finset.univ ι _inst_8)
                 (@finset.decidable_mem ι (λ (a b : ι), _inst_9 a b) a (@finset.univ ι _inst_8))
                 (λ (hp : a ∈ @finset.univ ι _inst_8), α a)
                 (λ (hp : a ∈ @finset.univ ι _inst_8) (a_1 b : α a), _inst_10 a a_1 b)
                 a_1
                 b)
            a
            b))
    (@finset.pi ι (λ (a : ι), α a) (λ (a b : ι), _inst_9 a b) (@finset.univ ι _inst_8) B)
    (@finset.pi ι (λ (a : ι), α a) (λ (a b : ι), _inst_9 a b) (@finset.univ ι _inst_8) C)

convert works, but takes more than 30 seconds, so this is not really acceptable. Is there a trick to make things better? (And sorry, no MWE).

[Rob Lewis]

Can you figure out what unification problem is making convert take so long?

[Rob Lewis]

Maybe something should be irreducible.

[Sebastien Gouezel]

I don't know, but at least I have been able to cook up a MWE:

import data.fintype

namespace finset

variables {α : Type*} [decidable_eq α] {δ : α → Type*} [∀ a : α, decidable_eq (δ a)]

lemma pi_disjoint_of_disjoint {s : finset α}
  (t₁ t₂ : Πa, finset (δ a)) {a : α} (ha : a ∈ s)
  (h : disjoint (t₁ a) (t₂ a)) : disjoint (s.pi t₁) (s.pi t₂) :=
disjoint_iff_ne.2 $ λ f₁ hf₁ f₂ hf₂ eq₁₂,
  disjoint_iff_ne.1 h (f₁ a ha) (mem_pi.mp hf₁ a ha) (f₂ a ha) (mem_pi.mp hf₂ a ha)
  $ congr_fun (congr_fun eq₁₂ a) ha

end finset

lemma zou {α : Type*} [fintype α] [decidable_eq α] {δ : α → Type*} [∀ a : α, decidable_eq (δ a)]
  (a₀ : α) (B C : Π a : α, finset (δ a)) (h : disjoint (B a₀) (C a₀)) :
  disjoint (finset.pi finset.univ B) (finset.pi finset.univ C) :=
begin
  have Z := finset.pi_disjoint_of_disjoint B C (finset.mem_univ a₀) h,
  exact Z -- fails
end

If I replace exact with convert, I get a timeout.

[Yury G. Kudryashov]

Can you try assume decidable_eq on the type where s.pi t lives instead of alpha?

[Sebastien Gouezel]

You're brilliant! Adding the assumption [decidable_eq (Πa∈s, δ a)] makes all the problems go away.