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.

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

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.

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.

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

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

Last updated: Sep 28 2023 at 11:01 UTC