push_neg of \and

Stream: mathlib4

[Nick Andersen]

[I'm new to Lean 4, and Zulip]
When I use push_neg on a statement like $\lnot (P \land Q)$, I get $P \rightarrow \lnot Q$, but I would like to get $\lnot P \lor \lnot Q$. (I realize that these are equivalent, but they behave differently in Lean, e.g. I can use "left" or "right" on the latter, which I can't do with the former.) Is there some way to get the latter behavior?

[Adam Topaz]

you could rewrite with docs4#not_and_or

[Nick Andersen]

Sure, in this simple example that works great, but in a more complicated expression it would be really nice to just use push_neg, or some variant, to simplify the whole expression. I'm thinking about this from a possible student's perspective mostly.

[Adam Topaz]

In practice the form $P \to \lnot Q$ is more useful because you can use intro hP and that leaves the goal $\lnot Q$, so that's similar to the "right" branch, except you also obtain hP in context.

[Adam Topaz]

Of course, if you wanted the left branch, then that's an issue. But you can use exfalso and revert hP (or some other tricks) to obtain this.

[Kyle Miller]

@Nick Andersen It might seem like push_neg is doing something crazy here, but one of the main uses of it is to negate forall and exists. The proposition $\exists(n > 0), p(n)$ is encoded as $\exists n, n>0 \wedge p(n)$ and $\forall(n>0), p(n)$ as $\forall n, n>0 \to p(n)$, so if you want $\neg\exists(n>0), p(n)$ to be $\forall(n>0),\neg p(n)$ you sort of want $\neg(n>0\wedge p(n))$ to be $n>0\to\neg p(n)$.

[Kyle Miller]

Though I think I remember @Heather Macbeth doing something to push_neg for your use case (for teaching)

[Alex J. Best]

Indeed: if you hover over the tactic push neg and read the docstring at the end it explains that setting set_option push_neg.use_distrib true does what you want

[Heather Macbeth]

The Lean 4 version of this option was done by @Frédéric Dupuis and @Jireh Loreaux as a favour to me; I later backported it to Lean 3.

[Nick Andersen]

Excellent -- that's exactly what I was looking for. Thanks!