Ssreflect Users Discussion List

[Georges Gonthier <>]

  It should be a little simpler than that: you should have two order 
relations, one for nat (the pervasive le will do just fine) and one for bool 
(say, leb). It's safer if le and leb are both inductives rather than 
definitions. You can then define instances for, say
  Proper (le ==> le ==> le) addn
  Proper (le --> le ++> le) subn
  Proper (le --> le ++> leb) leq
  Proper (leb ==> leb ==> leb) andb
  Proper (leb ==> impl) is_true.
Thus you don't need steps 1 and 3, translating to and from le: you do step 2 
with rewrite (leqRW H), where
  leqRW m n  : m <= n -> le m n := introT leP.
This assumes H is a ground inequality - you may have to add some trailing _ 
to make it so (or else hack some Ltac-in-term notation to do it for you).

  -- Georges

-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Christian Doczkal
Sent: 18 February 2016 13:02
To: 

Subject: Re: [ssreflect] Rewriting with inequalities?


> Could you expand on what you have in mind? Do you mean that one should 
> introduce a synonym for "m <= n"? Would this approach be essentially 
> equivalent to 1- replacing "m <= n" with "le m n" everywhere; 2- using 
> setoid rewrite on the relation le; 3- performing step 1- in reverse?

This is one way to do it. I was just toying around with your example and here 
is what I ended up with:

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

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

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

Definition le n m := is_true (n <= m).

Instance le_preOrder : PreOrder le.
Proof. split. exact: leqnn. move => ? ? ?. exact: leq_trans. Qed.

Instance proper_addn: Proper (le ++> le ++> le) addn.
Proof. move => x y ? n m ?. exact: leq_add. Qed.

Instance: Coq.Classes.RelationClasses.RewriteRelation le.

Goal
  forall x y,
  x <= y ->
  x + 1 <= y + 1.
Proof.
  move => x y h. rewrite -!/(le _ _) in h *.
  rewrite h.
  reflexivity.
Qed.