Ssreflect Users Discussion List

[François Pottier <>]

Hi Enrico,

> Could you check if your problem is an instance of this one? >   https://github.com/math-comp/math-comp/issues/18

Apparently yes. Robert's magic line seems to fix my problems (see
attached file). I am not sure what it does, though.

What's the official doctrine regarding rewriting with inequalities
in ssreflect? Is there a documentation or examples anywhere?

Thanks,

--
François Pottier

http://gallium.inria.fr/~fpottier/

Require Import Arith NPeano.

Require Import Coq.Program.Basics. (* [flip] *)
Require Export Coq.Setoids.Setoid. (* required for [rewrite] *)
Require Export Coq.Classes.Morphisms.
Require Import Omega.
Obligation Tactic := idtac.

(* Addition is covariant in both arguments. *)

Program Instance proper_plus: Proper (le ++> le ++> le) plus.
Next Obligation.
  intros x1 y1 h1 x2 y2 h2. omega.
Qed.

(* Robert's test in plain Coq. *)

Lemma foo x y z : x <= y -> y <= z -> x <= z.
Proof.
  intros H1 H2.
  rewrite H1.
  rewrite H2.
  apply le_refl.
Qed.

(* Robert's test in ssreflect. *)

Require Import ssreflect. (* 1.5 *)

Lemma bar x y z : x <= y -> y <= z -> x <= z.
Proof.
  move=> H1 H2.
  Fail rewrite H1.
  (* Error: not a rewritable relation: (x <= y) in rule H1 *)
Abort.

(* Robert's magic line. *)

Instance: Coq.Classes.RelationClasses.RewriteRelation le.

(* Now everything works. *)

Lemma bar x y z : x <= y -> y <= z -> x <= z.
Proof.
  move=> H1 H2.
  by rewrite H1 H2.
Qed.

Lemma quux x y : x <= y -> x + 1 <= y + 1.
Proof.
  move=> H.
  by rewrite H.
Qed.