Zulip Chat Archive

Stream: general

Topic: simp unfolding `has_mem` for filters


view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 20:26):

simp only with no lemmas unfolds s ∈ f to s in f.sets. How can I prevent this?

view this post on Zulip Mario Carneiro (Oct 27 2020 at 20:29):

what does simplify.rewrite say?

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 20:42):

#mwe:

import order.filter.basic

open filter

set_option trace.simplify.rewrite true
example (f₁ f₂ : filter ) (s : set ) : s  f₁  f₂ := by { simp only [mem_sup_sets],  }

Output:

6:62: 0. [simplify.rewrite] [filter.mem_sup_sets]: s  (f₁  f₂).sets ==> s  f₁  s  f₂

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 20:43):

Tactic state after simp shows .sets

view this post on Zulip Mario Carneiro (Oct 27 2020 at 20:47):

By process of elimination, setting {proj := ff} turns off the behavior

view this post on Zulip Mario Carneiro (Oct 27 2020 at 20:51):

The problem is that filter.has_mem is marked @[reducible]

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 20:53):

I'll try to remove this.


Last updated: May 15 2021 at 02:11 UTC