Library prosa.util.setoid

Setoid Rewriting with boolean inequalities of ssreflect. Solution suggested by Georges Gonthier (ssreflect mailinglist @ 18.12.2016)

From Coq Require Import Basics Setoid Morphisms.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

This construction allows us to "rewrite" inequalities with ≤.

Inductive leb a b := Leb of (a ==> b).

Lemma leb_eq a b : leb a b (a b).

Instance : PreOrder leb.

Instance : Proper (leb ==> leb ==> leb) andb.

Instance : Proper (leb ==> leb ==> leb) orb.

Instance : Proper (leb ==> impl) is_true.

Instance : Proper (le --> le ++> leb) leq.

Instance : Proper (le ==> le ==> le) addn.

Instance : Proper (le ++> le --> le) subn.

Instance : Proper (le ==> le) S.

Instance : RewriteRelation le.
Defined.

Definition leqRW {m n} : m n le m n := leP.

To see the benefits, consider the following example.
(*
Goal  
a b c d x y,
x y
a + (b + (x + c)) + d a + (b + (y + c)) + d.
Proof.
move a b c d x y LE.
 This could be an unpleasant proof, but we can just rewrite LE *)

by rewrite (leqRW LE).  magic here *)
Qed.
*)

Another benefit of leqRW is that it allows to avoid unnecessary eapply leq_trans.
(*
Goal
a b x y z,
a x
b y
x + y z
a + b z.
Proof.
move a b x y z LE1 LE2 LE3.
rewrite -(leqRW LE3) leq_add //.
Qed.
*)