(** 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.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]

(** 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.

#[global] Instance : PreOrder leb.
PreOrder leb
Proof.
PreOrder leb split => [[|]|[|][|][|][?][?]]; try exact: Leb. Qed.

#[global] 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.

#[global] Instance : Proper (leb ==> leb ==> leb) orb.
Proper (leb ==> leb ==> leb) orb
Proof.
Proper (leb ==> leb ==> leb) orb move => [|] [|] [A] [|] d [B]; exact: Leb. Qed.

#[global] 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.

#[global] 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.

#[global] 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.

#[global] 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.

#[global] 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.

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