Zulip Chat Archive

Stream: new members

Topic: negation of a formula in prenex normal form

Gihan Marasingha (Nov 10 2019 at 19:24):

Is there a Lean mechanism that, given the negation of a formula in prenex normal form, returns a proof of an equivalent formula, in prenex normal form?

Kevin Buzzard (Nov 10 2019 at 19:28):

Does the push_neg tactic help?

Gihan Marasingha (Nov 10 2019 at 19:31):

I'll look into it, thanks!

Gihan Marasingha (Nov 10 2019 at 19:38):

OK, this does exactly what I want. Thanks again.

Last updated: Dec 20 2023 at 11:08 UTC