normedtype.v provides theorems
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
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
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
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: Aug 19 2022 at 20:03 UTC