# Zulip Chat Archive

## Stream: new members

### Topic: error about instances

#### Arjun Pitchanathan (Feb 23 2020 at 02:06):

I have this:

import data.list noncomputable theory open_locale classical universe u variables {α : Type u} (a : α) (l : list α) theorem count_eq_countp : l.count a = l.countp (λ x, a = x) := sorry theorem count_eq_countp' : l.count a = l.countp (λ x, x = a) := begin conv in (_ = a) { rw eq_comm, }, exact (count_eq_countp a l), -- error here end

And I get this mystifying error:

invalid type ascription, term has type @list.count α (λ (a b : α), classical.prop_decidable (a = b)) a l = @list.countp α (λ (x : α), a = x) (λ (a_1 : α), classical.prop_decidable ((λ (x : α), a = x) a_1)) l but is expected to have type @list.count α (λ (a b : α), classical.prop_decidable (a = b)) a l = @list.countp α (λ (x : α), a = x) (@eq.rec (α → Prop) (λ (x : α), x = a) (λ (p : α → Prop), @decidable_pred α p) (λ (a_1 : α), classical.prop_decidable ((λ (x : α), x = a) a_1)) (λ (x : α), a = x) _) l state: α : Type u, a : α, l : list α ⊢ list.count a l = list.countp (λ (x : α), a = x) l

What is happening, and how do I fix it?

#### Chris Hughes (Feb 23 2020 at 04:23):

What's happening is that when you `rw eq_comm`

it has to change the type of the `decidable_pred`

instance from ` (λ x, x = a)`

to ` (λ x, a = x)`

. This is done using `eq.rec`

. The problem is that the decidable instance in `countp_eq_countp`

comes from `classical.prop_decidable`

, and the decidable instance in your goal is a cast of the decidable instance for `(λ x, x = a)`

. These two instances are not definitionally equal. There are a couple of solutions to this. One is to change the statement of `countp_eq_countp`

to

theorem count_eq_countp {h : decidable_pred (λ x, a = x)} : l.count a = l.countp (λ x, a = x)

This way the decidable instance is an argument that will be filled in with whatever instance is in your goal. This approach has a downside if you try to use this with `rw`

then Lean will not be able to infer the argument `h`

.

Another approach is to use `convert`

instead of `exact`

. This will use the fact that `decidable_pred (λ x, x = a)`

is a subsingleton to close the goal.

#### Arjun Pitchanathan (Feb 24 2020 at 13:44):

Thanks Chris! I went with the `convert`

option.

#### Arjun Pitchanathan (Feb 24 2020 at 14:24):

What's the best way to `convert`

while rewriting? For example I have to following error when trying to rewrite with `count_eq_countp'`

rewrite tactic failed, did not find instance of the pattern in the target expression @multiset.countp α (λ (x_1 : α), x_1 = @prod.fst α α x) (λ (a : α), classical.prop_decidable ((λ (x_1 : α), x_1 = @prod.fst α α x) a)) (@finset.val α (@V α g)) state: [snip] ⊢ @multiset.countp α (λ (x_1 : α), x_1 = @prod.fst α α x) (@eq.rec (α → Prop) (λ (x_1 : α), (x_1, v) = x) (λ (p : α → Prop), @decidable_pred α p) (λ (a : α), @prod.decidable_eq α α (λ (a b : α), classical.prop_decidable (a = b)) (λ (a b : α), classical.prop_decidable (a = b)) (a, v) x) (λ (x_1 : α), x_1 = @prod.fst α α x) _) (@finset.val α (@V α g)) = 1

(without implicit parameters the goal lhs and the pattern appear identical)

My current fix is

suffices : @multiset.countp α (λ (x_1 : α), x_1 = @prod.fst α α x) (λ (a : α), classical.prop_decidable ((λ (x_1 : α), x_1 = @prod.fst α α x) a)) (@finset.val α (@V α g)) = 1, by convert this, rw ← @multiset.count_eq_countp' _ g.V.val x.fst,

But is there a better way?

#### Chris Hughes (Feb 24 2020 at 21:39):

The usual solution to that is to do the `{h : decidable_pred... `

approach.

#### Arjun Pitchanathan (Feb 24 2020 at 23:24):

It doesn't seem to work, I still need to use `convert`

. This

import data.list universe u variables (α : Type u) (a : α) (l : list α) theorem count_eq_countp {h : decidable_pred (λ x, a = x)} {heq : decidable_eq α} : l.count a = l.countp (λ x, a = x) := sorry theorem count_eq_countp' {h : decidable_pred (λ x, a = x)} {h' : decidable_pred (λ x, x = a)} {heq : decidable_eq α} : l.count a = l.countp (λ x, x = a) := begin conv in (_ = a) { rw eq_comm, }, exact (@count_eq_countp _ a l h _), -- error, works with convert end

fails with a similar error:

invalid type ascription, term has type @list.count α (λ (a b : α), ?m_1 a b) a l = @list.countp α (λ (x : α), a = x) (λ (a_1 : α), ?m_1 a a_1) l but is expected to have type @list.count α (λ (a b : α), heq a b) a l = @list.countp α (λ (x : α), a = x) (@eq.rec (α → Prop) (λ (x : α), x = a) (λ (p : α → Prop), @decidable_pred α p) (λ (a_1 : α), heq a_1 a) (λ (x : α), a = x) _) l state: α : Type u, a : α, l : list α, h : decidable_pred (λ (x : α), a = x), h' : decidable_pred (λ (x : α), x = a), heq : decidable_eq α ⊢ list.count a l = list.countp (λ (x : α), a = x) l

#### Arjun Pitchanathan (Feb 24 2020 at 23:35):

(and I still can't rewrite, either)

Last updated: May 14 2021 at 00:42 UTC