rewriting

Stream: general

[Pablo Le Hénaff]

Hey again,
I'm stuck with this rewriting issue, I don't understand why it won't match :'(

[Pablo Le Hénaff]

set_option pp.all true
example {V : Type} (s : finset V) [decidable_eq V] (x y : V) (h : x ≠ y) :
  finset.filter (λ a : V, a = x ∧ a = y) s = finset.filter (λa, false) s :=
begin
  have : ∀a : V, a = x ∧ a = y ↔ false := sorry,
  rw [this]
end

[Simon Hudon]

use simp instead. rw does not rewrite bound variables. You need congruence lemmas for that and simp can access them.

[Chris Hughes]

How come simp can handle rewriting the type of the decidable_pred instance?

[Simon Hudon]

rewriting decidable is tricky because of how dependent those types are

[Simon Hudon]

Sorry, I misread. You're asking why it can?

[Chris Hughes]

Yes. I always have this problem with fintype.