(* This library defines some notions that involve functions and order,
   such as the property of being monotonic. *)

Set Implicit Arguments.
Require Import Coq.Classes.Morphisms Coq.micromega.Lia.
From TLC Require Import LibTactics.

(* -------------------------------------------------------------------------- *)

(* Definitions. *)

(* [within okA okB f] holds iff [f] maps [okA] into [okB]. *)

Definition within A B (okA : A -> Prop) (okB : B -> Prop) (f : A -> B) :=
  forall a,
  okA a ->
  okB (f a).

Definition preserves A (okA : A -> Prop) (f : A -> A) :=
  within okA okA f.

(* [monotonic leA leB f] holds iff [f] is monotonic with respect to
   the relations [leA] and [leB], i.e., [f] maps [leA] to [leB]. *)

Definition monotonic A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :=
  forall a1 a2,
  leA a1 a2 ->
  leB (f a1) (f a2).

(* [inverse_monotonic leA leB f] holds iff [f^-1] maps [leB] to [leA]. *)

Definition inverse_monotonic A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :=
  forall a1 a2,
  leB (f a1) (f a2) ->
  leA a1 a2.

(* [inflationary okA leA] holds iff [a] is less than [f a], with
   respect to the relation [leA], and for every [a] in [okA]. *)

Definition inflationary A (okA : A -> Prop) (leA : A -> A -> Prop) (f : A -> A) :=
  forall a,
  okA a ->
  leA a (f a).

(* If [leB] is a relation on [B], then [pointwise okA leB] is a relation
   on [A -> B]. *)

Definition pointwise A B (okA : A -> Prop) (leB : B -> B -> Prop) (f g : A -> B) :=
  forall a,
  okA a ->
  leB (f a) (g a).

(* -------------------------------------------------------------------------- *)

(* If [f] is monotonic, then rewriting in the argument of [f] is permitted. *)

(* Note: in order for [rewrite] to work properly, the lemmas that are able to
   prove [monotonic] assertions should be added to [typeclass_instances]. *)

(* TEMPORARY maybe this should be the *definition* of [monotonic] *)

Program Instance monotonic_Proper
  A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :
  monotonic leA leB f -> Proper (leA ++> leB) f.

(* -------------------------------------------------------------------------- *)

(* Letting [eauto] exploit [monotonic] and [inverse_monotonic]. *)

Lemma use_monotonic:
  forall B (leB : B -> B -> Prop) A (leA : A -> A -> Prop) (f : A -> B),
  monotonic leA leB f ->
  forall a1 a2,
  leA a1 a2 ->
  leB (f a1) (f a2).
Proof using.
  unfold monotonic. eauto.
Qed.

(* This variant is useful when the function has two arguments and one
   wishes to exploit monotonicity in the first argument. *)

Lemma use_monotonic_2:
  forall B (leB : B -> B -> Prop) A (leA : A -> A -> Prop) C (f : A -> C -> B) a1 a2 c,
  monotonic leA leB (fun a => f a c) ->
  leA a1 a2 ->
  leB (f a1 c) (f a2 c).
Proof using.
  unfold monotonic. eauto.
Qed.

Lemma use_inverse_monotonic:
  forall A (leA : A -> A -> Prop) B (leB : B -> B -> Prop) (f : A -> B),
  inverse_monotonic leA leB f ->
  forall a1 a2,
  leB (f a1) (f a2) ->
  leA a1 a2.
Proof using.
  unfold inverse_monotonic. eauto.
Qed.

(* It seems that these lemmas can be used as a hint only if we pick a
   specific instance of the ordering relation that appears in the
   conclusion. Furthermore, picking a specific instance of the
   ordering relation that appears in the premise can help apply
   [lia] to the premise. *)

Hint Resolve (@use_monotonic nat le nat le) (@use_monotonic nat lt nat lt)
: monotonic typeclass_instances.

Hint Resolve (@use_monotonic_2 nat le nat le) (@use_monotonic_2 nat lt nat lt)
: monotonic typeclass_instances.

Hint Resolve (@use_inverse_monotonic nat le nat le)
(@use_inverse_monotonic nat lt nat lt) : monotonic typeclass_instances.

(* -------------------------------------------------------------------------- *)

(* A little fact. If [f], viewed as a function of [A] into [B -> C], is
   monotonic, then its specialized version [fun a => f a b], which is a
   function of [A] to [C], is monotonic as well. And the converse holds. *)

Lemma monotonic_pointwise_specialize:
  forall A B C leA okB leC (f : A -> B -> C),
  monotonic leA (pointwise okB leC) f ->
  forall b, okB b -> monotonic leA leC (fun a => f a b).
Proof using.
  unfold monotonic, pointwise. auto.
Qed.

Lemma monotonic_pointwise_generalize:
  forall A B C leA (okB : B -> Prop) leC (f : A -> B -> C),
  (forall b, okB b -> monotonic leA leC (fun a => f a b)) ->
  monotonic leA (pointwise okB leC) f.
Proof using.
  unfold monotonic, pointwise. auto.
Qed.

(* -------------------------------------------------------------------------- *)

Require Import Coq.Arith.Arith.

(* The following tactics allow proving implications between inequalities
   by contraposition, while exploiting the fact that the negation of a
   strict inequality is a large inequality. *)

Ltac prove_le_le_by_contraposition :=
  match goal with h: ?a <= ?b |- ?x <= ?y =>
    (destruct (le_gt_dec x y); [ assumption | ]);
    assert (b < a); [ clear h | lia ]
  end.

Ltac prove_lt_lt_by_contraposition :=
  match goal with h: ?a < ?b |- ?x < ?y =>
    (destruct (le_gt_dec y x); [ false | lia ]);
    assert (b <= a); [ clear h | lia ]
  end.

(* If a function of type [nat -> nat] is strictly monotonic, then
   [f x1 <= f x2] implies [x1 <= x2]. The two assertions are in
   fact equivalent, since a strictly monotonic function is a
   fortiori a monotonic function. *)

Lemma monotonic_lt_lt_implies_inverse_monotonic_le_le:
  forall f : nat -> nat,
  monotonic lt lt f ->
  inverse_monotonic le le f.
Proof using.
  intros f ? x y ?. prove_le_le_by_contraposition. eauto.
Qed.

Lemma monotonic_lt_lt_implies_monotonic_le_le:
  forall f : nat -> nat,
  monotonic lt lt f ->
  monotonic le le f.
Proof using.
  introv h. intros x1 x2 ?.
  destruct (eq_nat_dec x1 x2).
    { assert (f x1 = f x2). congruence. lia. }
    { assert (f x1 < f x2). eapply h; lia. lia. }
Qed.

Hint Resolve monotonic_lt_lt_implies_inverse_monotonic_le_le
monotonic_lt_lt_implies_monotonic_le_le : monotonic typeclass_instances.

Goal
  forall f : nat -> nat,
  monotonic lt lt f ->
  forall x1 x2,
  f x1 <= f x2 <-> (* equivalence *)
  x1 <= x2.
Proof using.
  split; eauto with monotonic.
Qed.

(* If a function of type [nat -> nat] is monotonic, then
   [f x1 < f x2] implies [x1 < x2]. The converse is false. *)

Lemma monotonic_le_le_implies_inverse_monotonic_lt_lt:
  forall f : nat -> nat,
  monotonic le le f ->
  inverse_monotonic lt lt f.
Proof using.
  intros f ? x y ?. prove_lt_lt_by_contraposition. eauto.
Qed.

Hint Resolve monotonic_le_le_implies_inverse_monotonic_lt_lt :
monotonic typeclass_instances.
