Library prosa.util.setoid
Setoid Rewriting with boolean inequalities of ssreflect. Solution
suggested by Georges Gonthier (ssreflect mailinglist @ 18.12.2016)
From Stdlib Require Import Basics Setoid Morphisms.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
This construction allows us to "rewrite" inequalities with ≤.
The following establishes a number of "plumbing facts" that are necessary to
interface leb with the rewrite tactic.
leb expresses an implication.
leb is a preorder.
#[global] Instance : Proper (leb ==> leb ==> leb) andb.
Proof. move ⇒ [|] [|] [A] c d [B]; exact: Leb. Qed.
Proof. move ⇒ [|] [|] [A] c d [B]; exact: Leb. Qed.
#[global] Instance : Proper (leb ==> leb ==> leb) orb.
Proof. move ⇒ [|] [|] [A] [|] d [B]; exact: Leb. Qed.
Proof. move ⇒ [|] [|] [A] [|] d [B]; exact: Leb. Qed.
Relation with leq.
#[global] Instance : Proper (le --> le ++> leb) leq.
Proof. move ⇒ n m /leP ? n' m' /leP ?. apply/leb_eq ⇒ ?. eauto using leq_trans. Qed.
Proof. move ⇒ n m /leP ? n' m' /leP ?. apply/leb_eq ⇒ ?. eauto using leq_trans. Qed.
Relation with addn.
#[global] Instance : Proper (le ==> le ==> le) addn.
Proof. move ⇒ n m /leP ? n' m' /leP ?. apply/leP. exact: leq_add. Qed.
Proof. move ⇒ n m /leP ? n' m' /leP ?. apply/leP. exact: leq_add. Qed.
Relation with subn.
#[global] Instance : Proper (le ++> le --> le) subn.
Proof. move ⇒ n m /leP ? n' m' /leP ?. apply/leP. exact: leq_sub. Qed.
Proof. move ⇒ n m /leP ? n' m' /leP ?. apply/leP. exact: leq_sub. Qed.
Relation with the successor constructor.
#[global] Instance : Proper (le ==> le) S.
Proof. move ⇒ n m /leP ?. apply/leP. by rewrite ltnS. Qed.
Proof. move ⇒ n m /leP ?. apply/leP. by rewrite ltnS. Qed.
Establishing le as a rewrite relation.
Wrapper for use in rewrite steps:
To see the benefits, consider the following example.
Another benefit of leqRW is that it allows
to avoid unnecessary eapply leq_trans.
Goal forall 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 forall 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.