fixes #1797 (add cvg_dnbhs_at_right)

[affeldt-aist]

Motivation for this change

fixes #1797

I do not remember exactly why we needed these lemmas (@agontard ?)
but that seems natural and does not seem to hurt, hence this PR.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

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

[affeldt-aist]

Here is the ssprove error:

[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]File "./theories/Crypt/jasmin_word.v", line 189, characters 49-54:
Error: The variable mulwE was not found in the current environment.

make[2]: *** [Makefile.rocq:818: theories/Crypt/jasmin_word.vo] Error 1
make[2]: *** [theories/Crypt/jasmin_word.vo] Deleting file 'theories/Crypt/jasmin_word.glob'
make[2]: *** Waiting for unfinished jobs....

It looks unrelated to this PR (fyi: @4ever2 )

[4ever2]

Here is the ssprove error:

[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]File "./theories/Crypt/jasmin_word.v", line 189, characters 49-54:
Error: The variable mulwE was not found in the current environment.

make[2]: *** [Makefile.rocq:818: theories/Crypt/jasmin_word.vo] Error 1
make[2]: *** [theories/Crypt/jasmin_word.vo] Deleting file 'theories/Crypt/jasmin_word.glob'
make[2]: *** Waiting for unfinished jobs....

It looks unrelated to this PR (fyi: @4ever2 )

SSProve dev needs mathcomp-word >= 3.3, probably the reason for the error.

[agontard]

These lemmas were used along with cvg_at_right_left_dnbhs and left_right_continuousP to obtain

forall f0 x0, f0 x @[x --> x0] --> f0 x0 <-> f0 x @[x --> x0^'] --> f0 x0

Here the lhs corresponds to the definition of pointwise continuousness in mathcomp and the rhs to the one in HOL Light.

By the way, adding the proof of this equivalence to mathcomp could also make sense I suppose ?

[affeldt-aist]

These lemmas were used along with cvg_at_right_left_dnbhs and left_right_continuousP to obtain

forall f0 x0, f0 x @[x --> x0] --> f0 x0 <-> f0 x @[x --> x0^'] --> f0 x0

Ah, thanks, I now remember the context ^_^.

Here the lhs corresponds to the definition of pointwise continuousness in mathcomp and the rhs to the one in HOL Light.

By the way, adding the proof of this equivalence to mathcomp could also make sense I suppose ?

Since you have an application, this is a good indication that this equivalence should be somewhere I guess, but I am not sure where.

1. Maybe it is less likely to be used within MathComp-Analysis, so is it ok to bury it along other lemmas in an existing file?
2. Do we want to have it in a dedicated file that will serve as an interface mostly, a little bit like the coq-mathcomp-reals-stdlib package? Or in one of the showcase subdirectories?
3. Should it live outside MathComp-Analysis because it will by essentially used by your project? (But even in that case, we may want a reverse dependency in the CI to prevent breakage.)

What do you think? Since you ask the question here, maybe you were thinking of 2.?

[agontard]

I am not sure about the structure and habits in mathcomp. This is very similar to left_right_continuousP, so I see two main possibilities:

• Either it should be treated similarly to left_right_continuousP
• Or in mathcomp it is prefered in such cases to use the x^+ and x^- filters jointly rather than using the x^' filter. In this case, maybe I should preferably translate HOL Light's definition of limit over reals using the first option. I only chose the second option because it corresponded exactly to how HOL Light does it, but they are equivalent.

Would it be simpler for a mathcomp-analysis user to use f x @[x --> x0^'] --> l or f x @[x --> x0^+] --> l /\ f x @ [x --> x0^-] l ?

[affeldt-aist]

* Either it should be treated similarly to `left_right_continuousP`

I think that we are rather in this situation.
Yet, as of right now, left_right_continuousP, cvg_at_right_left_dnbhs, and the newly added cvg_dnbhs_at_{right,left} do not have the same level of generality (the type of their arguments). So I added another commit that, at least, put these lemmas in the same topology_theory subdirectory.

* Or in mathcomp it is prefered in such cases to use the `x^+` and `x^-` filters jointly rather than using the `x^'` filter. 

Would it be simpler for a mathcomp-analysis user to use f x @[x --> x0^'] --> l or f x @[x --> x0^+] --> l /\ f x @ [x --> x0^-] l ?

I am not sure we thought much about that but I suspect the shorter, the better.

In this case, maybe I should preferably translate HOL Light's definition of limit over reals using the first option.
I only chose the second option because it corresponded exactly to how HOL Light does it, but they are equivalent.

Yes, and it looks fine to me. Maybe there is a difference in that HOL Light is a bit more specialized to real analysis (I guess).
This reminds of this issue #1067 by @t6s :
If we had such a file, then the alignment with HOL Light will be clearer.

[affeldt-aist]

@agontard in any case, does this PR help in any way? that would help use deciding to merge it

[agontard]

@agontard in any case, does this PR help in any way? that would help use deciding to merge it

Well, it simply means we do not have to reprove these lemmas.

For potential end-users, it is advantageous if these lemmas not directly related to the HOL Light translation are found in mathcomp directly as it makes more sense and makes them easier to find, but this is only true for limits (cvg_dnbhs_at_[right/left] + cvg_at_right_left_dnbhs).
Indeed, for continuousness, the equivalence proof is only needed for the alignment, then end-users will only see lemmas talking about mathcomp's definition of continuousness, which does not involve the _^' filter.