Add lemmas not_near_inftyP and not_near_ninftyP in normedtype.v

[Yosuke-Ito-345]

Motivation for this change

@affeldt-aist @hoheinzollern
Add the infinite versions of the lemmas not_near_at_rightP and not_near_at_leftP in normedtype.v.

closes issue #1280

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

This is not a review but rather a comment.
I allowed myself to push a commit e2f3e0b to your PR.
When you mentioned not_near_at_rightP and not_near_at_leftP in issue #1273 I thought that one should be derived from the other using some potential useful intermediate lemma. This is indeed possible.
Similarly, for the lemmas not_near_inftyP and not_near_ninftyP: one can be derived from the other, though the proofs are globally not shorter.
I wonder whether a few more lemmas could not benefit from such factorizations.

[affeldt-aist]

Maybe we do not need to distinguish P and f in these lemmas?

[Yosuke-Ito-345]

Wonderful!
Thank you for adding the lemma filterN. This should be useful to my formalization of actuarial mathematics, too.
I also agree with you that P and f need not be distinguished. I wonder why I didn't notice that. \(^o^)/
I will reflect your suggestions in this pull request.

By the way, would it be better to add something like this?

Lemma iff_forall T (U V : T -> Prop) :
  (forall x : T, U x <-> V x) -> ((forall x, U x) <-> (forall x, V x)).

It shortens the proof of not_near_inftyP, but I am not sure whether it is compatible with the mathcomp style.

[hoheinzollern]

@Yosuke-Ito-345 not sure where you would want to use iff_forall, but have you checked out eq_forall?

eq_forall :
  forall [T : Type] [U V : T -> Prop],
    (forall x : T, U x = V x) -> (forall x : T, U x) = (forall x : T, V x)

[Yosuke-Ito-345]

@hoheinzollern
Yes, I know eq_forall. But we have to rewrite -propeqE before eq_forall, and rewrite propeqE after eq_forall.

Lemma not_near_inftyP (P : pred R) :
  ~ (\forall x \near +oo, P x) <->
    forall M : R, M \is Num.real -> exists2 x, M < x & ~ P x.
Proof.
rewrite nearE -forallNP -propeqE; apply: eq_forall => M.
by rewrite propeqE -implypN existsPNP.
Qed.

This feels inefficient to me. If we had iff_forall, the proof could be as follows.

by rewrite nearE -forallNP; apply: iff_forall => M; rewrite -implypN existsPNP.

I would not propose iff_forall if the following proof worked...

rewrite nearE -forallNP -propeqE; apply: eq_forall => M.
Fail rewrite -implypN existsPNP.

[Yosuke-Ito-345]

@affeldt-aist @hoheinzollern
I don't persist in adding iff_forall, so could you merge this pull request if there is no problem in the current code?
(I think I don't have the right to merge this pull request.)

[hoheinzollern]

Ok, the PR looks good to me, I don't think there's a strong reason to add the iff_forall, so I would keep it as is.

[affeldt-aist]

Looks ok to me.