simp_rw

Stream: general

[Michael Beeson]

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?

[Kenny Lau]

#backticks

[Kenny Lau]

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

[Kenny Lau]

you can start by copying the error message

[Floris van Doorn]

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.