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`

, and`aLc: 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.

```
```

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.
```

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 _ _) _ _`

?

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.

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?

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

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: Sep 28 2023 at 11:01 UTC