Zulip Chat Archive

Stream: new members

Topic: rw can't find pattern

Bruno Bandeira Monteiro (Dec 05 2021 at 03:43):

I'm still leaning to use lean. So I'm trying to formalize some basic theorems.
I can often use rw without any problems, but in a particular situation it seems to not find the pattern.

This is the state in the middle of a proof:

Notice that the consequent of the hypothesis dni1 almost matches the goal, but it says x is not in the complement of P. To rewrite this part of dni1 into "x is in P", i wrote a lemma (probably already in mathlib):

lemma notin_compl_iff_in (a : set N) (x : N): (x  a.compl)  x  a := begin split, by_cases (a x), intro, exact h, intro b, exfalso, exact b h, intros h1 h2, exact h2 h1, end

Using the command

rw notin_compl_iff_in at dni1,

It rewrites the antecedent of dni1 "z \notin P.compl" into "z \in P", but using the same command again it gives me an error, even though there is a second occurrence of the same pattern. The error I get:

The only difference I can see is that x is a bound variable, and z is a free variable, but I dont see why this would matter.
Any help is appreciated

Reid Barton (Dec 05 2021 at 03:59):

That's right, rw cannot rewrite under binders (like this forall). Try tactic#simp_rw instead.

Bruno Bandeira Monteiro (Dec 05 2021 at 04:04):

It says it failed to simplify.

Bruno Bandeira Monteiro (Dec 05 2021 at 04:06):

Do you see a simple way to solve this without having to eliminate these quantifiers?

Last updated: Dec 20 2023 at 11:08 UTC