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