Motive not type correct

Stream: new members

[Bhavik Mehta]

I'm getting the error rewrite tactic failed, motive is not type correct, and I can't figure out why...

import data.finset
open finset

set_option trace.check true

lemma test {n : ℕ} {a : finset (fin n)} : card a ∈ range (n + 1) :=
begin
  have q : finset.card (elems (fin n)) = n := card_fin n,
  rw [mem_range, nat.lt_succ_iff, ← q],
end

The "additional details" from the trace says:
[check] application type mismatch at card a argument type finset (fin n) expected type finset (fin _a)

[Mario Carneiro]

The backward rewrite is replacing n inside the expression @card (fin n) a, turning it into @card (fin (finset.card (elems (fin n)))) a which is no longer well typed because a still has the original type finset (fin n)

[Bhavik Mehta]

I see... Is there a way to avoid this, or do I just restructure the proof?

[Mario Carneiro]

you can use conv to focus on the RHS

[Mario Carneiro]

I would try to avoid rewriting with n = ... because there are too many triggers around

[Mario Carneiro]

you can often just stick to rewrites in the other direction to simplify composite terms

[Bhavik Mehta]

conv looks super useful, thanks!

[Kevin Buzzard]

(I changed imports/open)

import data.fintype
open fintype finset

set_option trace.check true

lemma test {n : ℕ} {a : finset (fin n)} : card a ∈ range (n + 1) :=
begin
  have q : finset.card (elems (fin n)) = n := card_fin n,
  rw [mem_range, nat.lt_succ_iff], -- ⊢ card a ≤ n
  conv begin
    to_rhs,
    rw ←q,
  end,
  sorry,
end

See conv docs (and feel free to add stuff to them). This stuff is not covered in TPIL but is occasionally a lifesaver.

[Bhavik Mehta]

Yeah that makes sense, I just rewrote it like this:

lemma test {n : ℕ} {a : finset (fin n)} : card a ∈ range (n + 1) :=
begin
  rw [mem_range, nat.lt_succ_iff],
  by calc card a ≤ card (fin n) : card_le_of_subset (subset_univ _)
          ... = n : card_fin n
end

[Kevin Buzzard]

When you run into an issue like this you can either make your argument work or restructure your argument. I guess my instinct is usually to make my argument work, which might mean why I sometimes write lousy code.