alternative normal form for push_neg

Stream: metaprogramming / tactics

[Heather Macbeth]

Would it be possible to have some global (within a file, or for all files downstream of a certain file) setting which changes push_neg and contrapose! to use a different logical normal form? In the current implementation ¬ (p ∧ q) gets normalized to p → ¬ q (see here in source) and for teaching I'd love to permanently set it so that this is instead normalized to ¬ p ∨ ¬ q.

I can think of a few different mechanisms -- maybe it could be something you arrange with a flag in set_option? Maybe one could do something with local attribute?

[Patrick Massot]

Note that what you ask was the original behavior which was changed in https://github.com/leanprover-community/mathlib/pull/3362

[Patrick Massot]

It should be pretty easy to choose this with an option

[Heather Macbeth]

I finally got around to implementing this, in #16586.