Zulip Chat Archive

Stream: general

Topic: simp_rw


view this post on Zulip Michael Beeson (Aug 31 2020 at 19:36):

simp_rw is supposed to rewrite under quantifiers. But: I have
h1 : ∀ (u a : M), u ∈ x ∧ ¬a ∈ u → u ∪ single a ∈ x
and
simp_rw and_comm at h1,
fails. Why?

The error message is "simplify tactic failed to simplify".

I expected and_comm to rewrite once. But maybe it just rewrites to what it considers "canonical order".
That is, I thought, if it gets b /\ a it should produce a /\ b and vice-versa, but maybe it always produces a /\ b?

view this post on Zulip Kenny Lau (Aug 31 2020 at 19:38):

#backticks

view this post on Zulip Kenny Lau (Aug 31 2020 at 19:39):

also could you describe the error in more detail than "fails"?

view this post on Zulip Kenny Lau (Aug 31 2020 at 19:39):

you can start by copying the error message

view this post on Zulip Floris van Doorn (Aug 31 2020 at 20:25):

simp and simp_rw simplify until they hit a normal form. Since and_comm can be applied over and over again, it has to decide whether u ∈ x ∧ ¬a ∈ u is simpler or (¬a ∈ u) ∧ u ∈ x is simpler. I think it decided the former, and therefore didn't rewrite.

You could try simp_rw and_comm (_ ∈ x) at h1. If that doesn't work, please give a #mwe.


Last updated: May 14 2021 at 04:22 UTC