In `Reals`

, the two orders `<=`

and `>=`

do not unify. This can sometimes be painful. I was thinking of something like this:

```
Require Import RIneq.
Open Scope R.
(* This fails
Lemma plop (r1 r2 : R) : r1 <= r2 -> r2 >= r1.
Proof. intros H. exact H. Qed.
*)
Coercion Rge_of_le (r1 r2 : R) (h : r1 <= r2) := (Rle_ge r1 r2 h).
(* This succeeds *)
Lemma plop (r1 r2 : R) : r1 <= r2 -> r2 >= r1.
Proof. intros H. exact H. Qed.
(* These fail
Lemma plop (r1 r2 : R) : r1 <= r2 -> r2 >= r1.
Proof. intros H. apply H. Qed.
Lemma plop (r1 r2 : R) : r1 <= r2 -> r2 >= r1.
Proof. now intros H. Qed.
*)
```

but, as you can see, the coercion is only used by the `exact`

tactic, not by `apply`

or `easy`

.

- Is there a way to make this coercion work in proofs?
- If not possible, is there any other way to make coq unify
`r1 <= r2`

with`r2 >= r1`

?

I fear there is not much to do (beside changing the definition which would break way too much things).

Users tend to take the habit to never write "a >= b" and write "a <= b" (or otherwise use a more modern alternative to the stdlib like MathComp ;) ).

The definition of `Rge`

was a mistake. It should have been defined so as to be convertible to `Rle`

. My recommendation is the same as Pierre: never use `Rge`

and life becomes much easier.

Well, maybe one can (locally) change the notation "a >= b" to mean "b <= a" and then never use Rge while still being able to "write" it?

I've heard the advice before, but didn't know it was so serious. Is this even documented anywhere? Refman?

Imho, never using `Rge`

is not really possible. If I want to write that `x`

is non-negative, I write `x >= 0`

because it is a statement about `x`

. For the moment I can live with it though, `Rge_le`

and `Rle_ge`

are short enough that I can use them in intro patterns with `%`

. But it would have been nice if the coercion worked. Do you have any idea as to why it fails ? Or how to add some "unification hint" ?

Pierre Roux said:

(or otherwise use a more modern alternative to the stdlib like MathComp ;) ).

I like that Reals is simple enough that I can use them with first year students at university. Not so sure it's possible with MathComp at the moment.

Karl Palmskog said:

I've heard the advice before, but didn't know it was so serious. Is this even documented anywhere? Refman?

I don't think so. Do you think a note in https://coq.inria.fr/distrib/current/refman/language/coq-library.html#notations-for-real-numbers would be appropriate?

Pierre Rousselin said:

never using

`Rge`

is not really possible

But are you really using `Rge`

? Aren't you just using the notation? If so, as Pierre proposed, just redefine the notation:

```
Notation "a >= b" := (Rle b a) (only parsing).
```

Pierre Roux said:

Karl Palmskog said:

I've heard the advice before, but didn't know it was so serious. Is this even documented anywhere? Refman?

I don't think so. Do you think a note in https://coq.inria.fr/distrib/current/refman/language/coq-library.html#notations-for-real-numbers would be appropriate?

I was thinking about writing a small manual, maybe in Rbase, with things like :

- < is convertible to >
- <= is not convertible to >= (use Rle_ge and Rge_le)
- how you can use left or right to prove an inequality with <= or >=

Pierre Rousselin said:

I like that Reals is simple enough that I can use them with first year students at university. Not so sure it's possible with MathComp at the moment.

Fair enough, it's probably harder to use MathComp without background on the algebraic hierarchy (knowing where to search lemmas about rings or fields and not a single R type).

I think the small manual entry @Pierre Rousselin suggests sounds good, but we really need some special box with "Warning" "Recommendation" or similar, to use `Rle`

over `Rge`

I'll submit you a draft version when things quiet down at work.

FWIW, easy can be extended via hints: it calls trivial, so 0-cost hints in core would help. And I don't know anyway to extend apply like you want.

For shadowing: I guess one could define "Rge' x y := Rle y x" and use Rge' in the notation?

Last updated: Jun 25 2024 at 19:01 UTC