(** 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.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

(** 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).
a, b: bool
leb a b <-> (a -> b)
Proof.
a, b: bool
leb a b <-> (a -> b) move: a b => [|] [|]; firstorder. Qed.

Instance : PreOrder leb.
PreOrder leb
Proof.
PreOrder leb split => [[|]|[|][|][|][?][?]]; try exact: Leb. Qed.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

Instance : Proper (leb ==> leb ==> leb) andb.
Proper (leb ==> leb ==> leb) andb
Proof.
Proper (leb ==> leb ==> leb) andb move => [|] [|] [A] c d [B]; exact: Leb. Qed.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

Instance : Proper (leb ==> leb ==> leb) orb.
Proper (leb ==> leb ==> leb) orb
Proof.
Proper (leb ==> leb ==> leb) orb move => [|] [|] [A] [|] d [B]; exact: Leb. Qed.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

Instance : Proper (leb ==> impl) is_true.
Proper (leb ==> impl) is_true
Proof.
Proper (leb ==> impl) is_true move => a b [].
a, b: bool
a ==> b -> impl a b exact: implyP. Qed.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

Instance : Proper (le --> le ++> leb) leq.
Proper (le --> le ==> leb) leq
Proof.
Proper (le --> le ==> leb) leq move => n m /leP ? n' m' /leP ?.
n, m: nat
__view_subject_1_: m <= n
n', m': nat
__view_subject_3_: n' <= m'
leb (n <= n') (m <= m') apply/leb_eq => ?.
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. Qed.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

Instance : Proper (le ==> le ==> le) addn.
Proper (le ==> le ==> le) addn
Proof.
Proper (le ==> le ==> le) addn move => n m /leP ? n' m' /leP ?.
n, m: nat
__view_subject_1_: n <= m
n', m': nat
__view_subject_3_: n' <= m'
(n + n' <= m + m')%coq_nat apply/leP.
n, m: nat
__view_subject_1_: n <= m
n', m': nat
__view_subject_3_: n' <= m'
n + n' <= m + m' exact: leq_add. Qed.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

Instance : Proper (le ++> le --> le) subn.
Proper (le ==> le --> le) subn
Proof.
Proper (le ==> le --> le) subn move => n m /leP ? n' m' /leP ?.
n, m: nat
__view_subject_1_: n <= m
n', m': nat
__view_subject_3_: m' <= n'
(n - n' <= m - m')%coq_nat apply/leP.
n, m: nat
__view_subject_1_: n <= m
n', m': nat
__view_subject_3_: m' <= n'
n - n' <= m - m' exact: leq_sub. Qed.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

Instance : Proper (le ==> le) S.
Proper (le ==> le) succn
Proof.
Proper (le ==> le) succn move => n m /leP ?.
n, m: nat
__view_subject_1_: n <= m
(n.+1 <= m.+1)%coq_nat apply/leP.
n, m: nat
__view_subject_1_: n <= m
n < m.+1 by rewrite ltnS. Qed.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

Instance : RewriteRelation le.
Defined.
The default value for instance locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding instances outside of sections without
specifying an explicit locality attribute is therefore
deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example:
"#[export] Instance Foo : Bar := baz."
[deprecated-instance-without-locality,deprecated]

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.                                                                      ]
*)