Stream: Coq users

Topic: Coercions in proofs

Pierre Rousselin (Jan 20 2023 at 16:12):

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.

1. Is there a way to make this coercion work in proofs?
2. If not possible, is there any other way to make coq unify r1 <= r2 with r2 >= r1 ?

Pierre Roux (Jan 20 2023 at 16:36):

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 ;) ).

Guillaume Melquiond (Jan 20 2023 at 16:37):

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.

Pierre Roux (Jan 20 2023 at 16:39):

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?

Karl Palmskog (Jan 20 2023 at 16:40):

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

Pierre Rousselin (Jan 20 2023 at 16:43):

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 Rousselin (Jan 20 2023 at 16:44):

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.

Pierre Roux (Jan 20 2023 at 16:46):

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?

Guillaume Melquiond (Jan 20 2023 at 16:47):

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 Rousselin (Jan 20 2023 at 16:49):

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 Roux (Jan 20 2023 at 16:50):

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

Karl Palmskog (Jan 20 2023 at 16:50):

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

Pierre Rousselin (Jan 20 2023 at 17:52):

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

Paolo Giarrusso (Jan 20 2023 at 22:04):

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.

Paolo Giarrusso (Jan 20 2023 at 23:46):

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

Last updated: Oct 04 2023 at 23:01 UTC