Library prosa.util.setoid
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 13)
a, b : bool
============================
leb a b <-> (a -> b)
----------------------------------------------------------------------------- *)
Proof. move: a b ⇒ [|] [|]; firstorder.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : PreOrder leb.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 15)
============================
PreOrder leb
----------------------------------------------------------------------------- *)
Proof. split ⇒ [[|]|[|][|][|][?][?]]; try exact: Leb.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : Proper (leb ==> leb ==> leb) andb.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 25)
============================
Proper (leb ==> leb ==> leb) andb
----------------------------------------------------------------------------- *)
Proof. move ⇒ [|] [|] [A] c d [B]; exact: Leb.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : Proper (leb ==> leb ==> leb) orb.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
============================
Proper (leb ==> leb ==> leb) orb
----------------------------------------------------------------------------- *)
Proof. move ⇒ [|] [|] [A] [|] d [B]; exact: Leb.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : Proper (leb ==> impl) is_true.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
============================
Proper (leb ==> impl) is_true
----------------------------------------------------------------------------- *)
Proof. move ⇒ a b [].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 53)
a, b : bool
============================
a ==> b -> impl a b
----------------------------------------------------------------------------- *)
exact: implyP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : Proper (le --> le ++> leb) leq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 54)
============================
Proper (le --> le ==> leb) leq
----------------------------------------------------------------------------- *)
Proof. move ⇒ n m /leP ? n' m' /leP ?.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 161)
n, m : nat
__view_subject_1_ : m <= n
n', m' : nat
__view_subject_3_ : n' <= m'
============================
leb (n <= n') (m <= m')
----------------------------------------------------------------------------- *)
apply/leb_eq ⇒ ?.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 238)
n, m : nat
__view_subject_1_ : m <= n
n', m' : nat
__view_subject_3_ : n' <= m'
_Hyp_ : n <= n'
============================
m <= m'
----------------------------------------------------------------------------- *)
eauto using leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : Proper (le ==> le ==> le) addn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
============================
Proper (le ==> le ==> le) addn
----------------------------------------------------------------------------- *)
Proof. move ⇒ n m /leP ? n' m' /leP ?.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 171)
n, m : nat
__view_subject_1_ : n <= m
n', m' : nat
__view_subject_3_ : n' <= m'
============================
(n + n' <= m + m')%coq_nat
----------------------------------------------------------------------------- *)
apply/leP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 219)
n, m : nat
__view_subject_1_ : n <= m
n', m' : nat
__view_subject_3_ : n' <= m'
============================
n + n' <= m + m'
----------------------------------------------------------------------------- *)
exact: leq_add.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : Proper (le ++> le --> le) subn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
============================
Proper (le ==> le --> le) subn
----------------------------------------------------------------------------- *)
Proof. move ⇒ n m /leP ? n' m' /leP ?.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
n, m : nat
__view_subject_1_ : n <= m
n', m' : nat
__view_subject_3_ : m' <= n'
============================
(n - n' <= m - m')%coq_nat
----------------------------------------------------------------------------- *)
apply/leP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 232)
n, m : nat
__view_subject_1_ : n <= m
n', m' : nat
__view_subject_3_ : m' <= n'
============================
n - n' <= m - m'
----------------------------------------------------------------------------- *)
exact: leq_sub.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : Proper (le ==> le) S.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 83)
============================
Proper (le ==> le) succn
----------------------------------------------------------------------------- *)
Proof. move ⇒ n m /leP ?.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 137)
n, m : nat
__view_subject_1_ : n <= m
============================
(n.+1 <= m.+1)%coq_nat
----------------------------------------------------------------------------- *)
apply/leP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 185)
n, m : nat
__view_subject_1_ : n <= m
============================
n < m.+1
----------------------------------------------------------------------------- *)
by rewrite ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Instance : RewriteRelation le.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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. ]
*)
[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. ]
*)
[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. ]
*)