From f9ef87453212f021b8ae352b2eaa45e89f52615f Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 19 Jul 2021 17:10:39 +0200
Subject: [PATCH] Add setoid rewrite
---
scripts/wordlist.pws | 5 +++-
util/all.v | 1 +
util/setoid.v | 69 ++++++++++++++++++++++++++++++++++++++++++++
3 files changed, 74 insertions(+), 1 deletion(-)
create mode 100644 util/setoid.v
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index 355d82b53..48cb9fea3 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -62,4 +62,7 @@ superadditive
subadditivity
subadditive
ad
-hoc
\ No newline at end of file
+hoc
+mailinglist
+Gonthier
+setoid
\ No newline at end of file
diff --git a/util/all.v b/util/all.v
index c80df7935..cdc1a9d95 100644
--- a/util/all.v
+++ b/util/all.v
@@ -16,3 +16,4 @@ Require Export prosa.util.minmax.
Require Export prosa.util.supremum.
Require Export prosa.util.nondecreasing.
Require Export prosa.util.rewrite_facilities.
+Require Export prosa.util.setoid.
diff --git a/util/setoid.v b/util/setoid.v
new file mode 100644
index 000000000..f6bd2d8e6
--- /dev/null
+++ b/util/setoid.v
@@ -0,0 +1,69 @@
+(** 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).
+Proof. move: a b => [|] [|]; firstorder. Qed.
+
+Instance : PreOrder leb.
+Proof. split => [[|]|[|][|][|][?][?]]; try exact: Leb. Qed.
+
+Instance : Proper (leb ==> leb ==> leb) andb.
+Proof. move => [|] [|] [A] c d [B]; exact: Leb. Qed.
+
+Instance : Proper (leb ==> leb ==> leb) orb.
+Proof. move => [|] [|] [A] [|] d [B]; exact: Leb. Qed.
+
+Instance : Proper (leb ==> impl) is_true.
+Proof. move => a b []. exact: implyP. Qed.
+
+Instance : Proper (le --> le ++> leb) leq.
+Proof. move => n m /leP ? n' m' /leP ?. apply/leb_eq => ?. eauto using leq_trans. Qed.
+
+Instance : Proper (le ==> le ==> le) addn.
+Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_add. Qed.
+
+Instance : Proper (le ++> le --> le) subn.
+Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_sub. Qed.
+
+Instance : Proper (le ==> le) S.
+Proof. move => n m /leP ?. apply/leP. by rewrite ltnS. Qed.
+
+Instance : RewriteRelation le.
+Defined.
+
+Definition leqRW {m n} : m <= n -> le m n := leP.
+
+(** To see the benefits, consider the following example. *)
+(*
+[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. ]
+*)
+
+(** Another benefit of [leqRW] is that it allows
+ to avoid unnecessary [eapply leq_trans]. *)
+(*
+[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. ]
+*)
--
GitLab