Stream: math-comp analysis

Topic: interval and interval property


view this post on Zulip Yves Bertot (Jul 21 2021 at 12:49):

File normedtype.v provides theorems interval_is_interval and is_intervalPle but I find the latter cumbersome to use. If we know that aI : a \in I and bI : b \in I for some (math-comp) interval I, andaLc: a < c and cLb : c< b, then we can prove c \in I by just typing

by rewrite (interval_is_interval aI bI) ?aLc.

On the other hand, if we only know aLc' : a <= c and cLb' : c <= b instead of aLc and cLb, we have to go through the much more cumbersome proof:

by have := @interval_is_interval _ I; rewrite is_intervalPle => /(_ _ _ aI bI c); rewrite aLc'; apply.

Life would be much easier if the definition of is_interval used large comparisons instead of strict ones: the proof for the second goal would only be:

rewrite (interval_is_interval aI bI) ?aLc'

and the proof for the first case would be:

rewrite (interval_is_interval aI bI) ?ltW

So I am advocating for a change in the definition is_interval and the accompanying lemmas.


view this post on Zulip Reynald Affeldt (Jul 21 2021 at 13:41):

On the other hand, we can also write:

Lemma test (R : numDomainType) (I : interval R) a b c
  (aI : a \in I) (bI : b \in I) (ac : a <= c) (cb : c <= b) :
  c \in I.
Proof.
by rewrite ((is_intervalPle _).1 (@interval_is_interval _ _) _ _ aI bI) ?ac.
Qed.

view this post on Zulip Reynald Affeldt (Jul 21 2021 at 13:42):

So what about adjusting the implicit arguments of is_intervalPle and interval_is_interval and/or providing some definition to act as the string (is_intervalPle _).1 (@interval_is_interval _ _) _ _ ?

view this post on Zulip Yves Bertot (Jul 21 2021 at 14:40):

I still think the definition of is_interval is wrong one, because it makes the theorem less usable. Having to prove a < b when one has a <= b is impossible, the other way round is easy.

view this post on Zulip Yves Bertot (Jul 29 2021 at 11:11):

I am in the process of testing a new version of analysis where the definition of is_interval is based on large inequalities. Everything compiles, including the PR on continuous inverses, and the PR on trigonometric function on top of that. I am looking for other PRs that may have uses of is_interval. @Reynald Affeldt, can you point me to relevant work?

view this post on Zulip Reynald Affeldt (Jul 29 2021 at 11:42):

i would say PR 371 (the Lebesgue measure) (sorry, I am not in a front of a computer right now)

view this post on Zulip Yves Bertot (Jul 29 2021 at 13:20):

I updated the branch lebesgue_measure to accommodate the change of definition for is_interval that I am advocating. I produced a branch that combines the current PR on continuity for inverse functions, the change of definition of is_interval, and this branch on Lebesgue measure. The branch is available as https://github.com/ybertot/analysis/tree/ctv-itv-meas. The necessary changes to your work are quite minimal.


Last updated: Aug 19 2022 at 20:03 UTC