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).
#[global] Instance : PreOrder leb.
#[global] Instance : Proper (leb ==> leb ==> leb) andb.
#[global] Instance : Proper (leb ==> leb ==> leb) orb.
#[global] Instance : Proper (leb ==> impl) is_true.
#[global] Instance : Proper (le --> le ++> leb) leq.
#[global] Instance : Proper (le ==> le ==> le) addn.
#[global] Instance : Proper (le ++> le --> le) subn.
#[global] Instance : Proper (le ==> le) S.
#[global] 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.
*)
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.
*)
(*
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.
*)
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.
*)