## Stream: general

### Topic: Decidability nightmare

#### Sebastien Gouezel (Feb 26 2020 at 20:35):

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 (Feb 26 2020 at 20:36):

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

#### Rob Lewis (Feb 26 2020 at 20:36):

Maybe something should be irreducible.

#### Sebastien Gouezel (Feb 26 2020 at 20:49):

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 (Feb 26 2020 at 20:55):

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

#### Sebastien Gouezel (Feb 26 2020 at 20:59):

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

Last updated: May 15 2021 at 23:13 UTC