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.
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: Oct 13 2024 at 01:02 UTC