le is not a Rewriteable Relation

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4549
From: @gares
Reported version: 8.5
CC: @robbertkrebbers, @mattam82, @RalfJung

[coqbot]

Comment author: @gares

In ssreflect we use Rewrite.is_applied_rewrite_relation to detects if a relation symbol can be handled by the setoid rewrite machinery. Such API tries to resolve a TC instance for (RewriteRelation le) and fails.

See math-comp/math-comp#18

Declaring the instance by hand solves the problem.

I'd add the declaration myself, but I'm not sure if:

1. would it impact other code?
2. are there other ways to go that are less error prone? How does Coq's rewrite detect le is a rewritable relation?

Best

[coqbot]

Comment author: @robbertkrebbers

The situation became considerable worse in 8.6. Example:

(** BEGIN **)
Require Import mathcomp.ssreflect.ssreflect.
Require Import Setoid.

Class Comm {A} (R : relation A) (f : A -> A -> A) :=
  comm : forall x y, R (f x y) (f y x).

Instance plus_comm : Comm eq plus. Admitted.

Lemma foo x y : x + y = y + x.
Proof.
  Fail rewrite comm.
  (* Error: not a rewritable relation: (_ (_ _ _) (_ _ _))
     in rule comm *)

  rewrite ->comm.
  (* works *)
Restart.

  (* Removing the following hint makes it work *)
  Remove Hints RewriteRelation_instance_2 : typeclass_instances.

  rewrite comm. 
  (* works *)
(** END *)

My analysis of the problem:

• In order to decide whether to use setoid rewriting, ssreflect calls type class search to find an instance of:

    RewriteRelation R

• In case of rewrite with something like comm, it does not know the relation, so it looks for an instance of:

    RewriteRelation ?R

  where ?R is an evar.

• It then uses some arbitrary instance, in the example RewriteRelation_instance_2, which creates yet another (shelved) evar.

• Since Coq commit 9830537, when a non type-class shelved goal remains during type class search, it fails globally, and it does not back track on other instances.

[CohenCyril]

@mattam82 is this issue still a current?

[mattam82]

I believe so