Zulip Chat Archive

Stream: general

Topic: rewriting


view this post on Zulip Pablo Le Hénaff (Jun 08 2018 at 14:03):

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

view this post on Zulip Pablo Le Hénaff (Jun 08 2018 at 14:04):

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

view this post on Zulip Simon Hudon (Jun 08 2018 at 14:09):

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

view this post on Zulip Chris Hughes (Jun 08 2018 at 20:35):

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

view this post on Zulip Simon Hudon (Jun 08 2018 at 20:38):

rewriting decidable is tricky because of how dependent those types are

view this post on Zulip Simon Hudon (Jun 08 2018 at 20:41):

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

view this post on Zulip Chris Hughes (Jun 08 2018 at 21:11):

Yes. I always have this problem with fintype.


Last updated: May 16 2021 at 05:21 UTC