feat(Mathlib/Tactic/PushNeg): implement the `push_neg` tactic

[dupuisf]

trafficstars

This PR implements the push_neg tactic. This code is based on https://github.com/leanprover-community/mathlib4/pull/193/ and on the original Lean 3 push_neg code. It notably implements a new feature: if set_option push_neg.use_distrib true is set, then it performs (¬ (p ∧ q)) = (¬ p ∨ ¬ q) instead of (¬ (p ∧ q)) = (p → ¬ q).

Note: I'm not too sure what the conventions are for options (i.e. is push_neg.use_distrib an appropriate name?). Also, I don't know what the "group" string of the option is for, so I left it blank.

Co-authored-by: @j-loreaux

[dupuisf]

I just implemented the suggestions, and changing the main loop to return an Option (Simp.Step), to be able to distinguish the case where we find nothing to push from the case when we do but the proof is rfl.

[dupuisf]

Note that I uncovered a missing case when doing one last check: given an expression like ¬(x = 0 → y = 0), we have to check that the left side of the arrow is a prop, otherwise it is treated like a for-all. This is now fixed.

[gebner]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build