error about instances

Stream: new members

[Arjun Pitchanathan]

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]

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]

Thanks Chris! I went with the convert option.

[Arjun Pitchanathan]

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]

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

[Arjun Pitchanathan]

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]

(and I still can't rewrite, either)