Is there a push_neg attribute?

Stream: new members

[Rida Hamadani]

I would like to have docs#not_nonempty_iff apply automatically after push_neg or !, such as at contrapose!. Is there a way to make this happen similar to how simp or norm_num attributes are added? Note that adding push_neg as an attribute gives an unknown attribute error.

[Johan Commelin]

Currently push_neg uses a hard-coded list of lemmas. See Mathlib/Tactic/PushNeg.lean

[Rida Hamadani]

Thank you!

[Rida Hamadani]

I was trying to add that lemma to the hard-coded list, but Mathlib/Tactic/PushNeg.leandoes not even import IsEmpty, is there a way to make push_neg use lemmas such as docs#not_nonempty_iff, without making it import many files?

[Johan Commelin]

I think it will need a redesign for that to happen. cc @Patrick Massot who is the original author.

[Patrick Massot]

I think this could be added without too much trouble.

[Rida Hamadani]

Patrick Massot said:

I think this could be added without too much trouble.

Adding that particular lemma, or the ability to add lemmas without having to import more files in PushNeg.lean?

[Patrick Massot]

The ability to add lemmas.