Zulip Chat Archive

Stream: new members

Topic: error about instances


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Arjun Pitchanathan (Feb 24 2020 at 13:44):

Thanks Chris! I went with the convert option.

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Feb 24 2020 at 21:39):

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

view this post on Zulip 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

view this post on Zulip Arjun Pitchanathan (Feb 24 2020 at 23:35):

(and I still can't rewrite, either)


Last updated: May 14 2021 at 00:42 UTC