Ssreflect Users Discussion List

[François Pottier <>]

Hello again, with another beginner question.

In standard Coq, provided one has declared appropriate instances of the type
class Proper, one can rewrite with an inequality (in fact, with an arbitrary
relation). In ssreflect, I don't know how to make this work (see 
attached file
for an example).

If it can be made to work, will it be compatible with ssreflect's improved
"rewrite" tactic? e.g. can one select which occurrence should be rewritten,
chain rewrites, etc.?

Thanks for your help!

--
François Pottier

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

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.

Goal
  forall x y,
  x <= y ->
  x + 1 <= y + 1.
Proof.
  intros x y h.
  rewrite h.
  apply le_refl.
Qed.

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Goal
  forall x y,
  x <= y ->
  x + 1 <= y + 1.
Proof.
  move => x y h.
  rewrite h.
  apply le_refl.
Qed.