## Stream: math-comp devs

### Topic: bounds in interval

#### Yves Bertot (Jul 21 2021 at 07:30):

In one of my proofs, I felt the need to have the following theorems:

``````Lemma itvlc (a b : R) : (a \in `[a, b]) = (a <= b).
Proof.  by rewrite in_itv /= lexx. Qed.

Lemma itvcr (a b : R) : (b \in `[a, b]) = (a <= b).
Proof. by rewrite in_itv /= lexx andbT. Qed.
``````

I then wondered if these theorems should be added in `interval.v` and I found that the need was somehow (but only clumsily) covered by the multi-rule `bound_in_itv`. This is unsatisfactory, because it leaves me with goals of the shape

``````(BRight a <= BRight b)%O
``````

This is convertible with (a <= b), but not recognized as a rewrite location. For instance, if I have `aLb : a <= b` in the context, I cannot rewrite with `aLb`.
so if I want this to be exhibited, I need to include the unfold directive `/Order.le` in my rewrite sequence. This feels rather clumsy. Do you have any opinion on this topic? Should theorems `itvlc` and `itvrc` be included in the multi-rule bound_in_itv? Do users really need to see the comparison between interval bounds? It feels to me that final users of math-comp need only to be aware of the comparison between intervals, and the comparison between numbers, but the comparison between bounds should only be used for internal lemmas.

#### Yves Bertot (Jul 21 2021 at 07:37):

So, the lemma that should be provided to users should be as follows (with the proof).

``````Lemma bound_in_itv' (a b : R): ((a \in `[a, b]) = (a <= b)) *
((b \in `[a, b]) = (a <= b)) *
((a \in `[a, b[) = (a < b)) *
((b \in `]a, b]) = (a < b)) *
(a \in `[a, +oo[ ) *
(a \in `]-oo, a]).
Proof.
by rewrite !bound_in_itv /=.
Qed.
``````

#### Yves Bertot (Jul 21 2021 at 07:53):

I am actually advocating renaming `bound_in_itv` to be the statement I propose, and let the other multi-rule unnamed, just `(boundl_in_intv, boundr_in_itv), for the rare places where it is being used.

#### Reynald Affeldt (Jul 21 2021 at 09:38):

This is unsatisfactory, because it leaves me with goals of the shape

``````(BRight a <= BRight b)%O
``````

This is convertible with (a <= b), but not recognized as a rewrite location. For instance, if I have `aLb : a <= b` in the context, I cannot rewrite with `aLb`.

Not an answer but a related element of discussion. I ended up using

``````Variable R : numDomainType.

Local Lemma BLft_ltE (x y : R) : (BLeft x < BLeft y)%O = (x < y).
Proof. by []. Qed.
Local Lemma BRight_leE (x y : R) : (BRight x <= BRight y)%O = (x <= y).
Proof. by []. Qed.
Local Lemma BRight_BLeft_leE (x y : R) : (BRight x <= BLeft y)%O = (x < y).
Proof. by []. Qed.
Local Lemma BLeft_BRight_ltE (x y : R) : (BLeft x < BRight y)%O = (x <= y).
Proof. by []. Qed.
Local Lemma BRight_BSide_ltE (x y : R) b : (BRight x < BSide b y)%O = (x < y).
Proof. by case: b. Qed.
Local Lemma BLeft_BSide_leE (x y : R) b : (BLeft x <= BSide b y)%O = (x <= y).
Proof. by case: b. Qed.

Definition lte_bnd := (BLeft_ltE, BLeft_BRight_ltE, BRight_BSide_ltE,
BLeft_BSide_leE, BRight_BLeft_leE, BRight_leE)
``````

to dispose of such goals.

#### Yves Bertot (Jul 21 2021 at 10:49):

So would it make sense to have bound_in_itv be (boundr_in_itv, boundl_in_itv, lte_bnd). instead of my initial proposal?

#### Yves Bertot (Jul 21 2021 at 10:50):

yuck! it is only the same behavior if we use repetition.

Last updated: Sep 28 2023 at 11:01 UTC