(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** * Order Theory with Classes.

   This module implements classes for different varieties of orders: preorders,
   partial orders, total partial orders, strict orders and total strict orders.

   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Coq.Program.Program.
Require Export Setoid Morphisms.
Require Export Coq.Classes.RelationClasses Coq.Classes.Equivalence.
Require Import Coq.Classes.Morphisms_Relations.

Require Import Coq.Logic.Decidable.

Open Scope equiv_scope.

Ltac obligation_tactic ::= eauto with typeclass_instances || program_simpl.

Class Decidable (P : Prop) :=
  is_decidable : decidable P.

(* Dual preorder, just by reversing the arrows. We have to be careful about 
   applying this hint only when the goal requests it, having an (inverse _) index
   already, otherwise it's always applicable. *)
  
Program Definition preorder_dual `(pre : PreOrder A R) :
  PreOrder (inverse R).
Proof. constructor ; typeclasses eauto. Qed.

Inductive applied (A : Type) (t : A) := is_applied.

Tactic Notation "class_apply_once" ident(c) := class_apply c ; trivial.
  (* match goal with *)
  (*   | [ _ : @applied _ ?T |- _ ] => match T with c => fail 2 | _ => fail 1 end *)
  (*   | _ => let H := fresh "applied" in assert(H:=@is_applied _ c) ; class_apply c *)
  (* end. *)

Ltac check_not_inverse_evar c :=
  match c with
    | ?R => first [ not_evar R | fail 2 ]
    | _ => idtac
  end.

Hint Extern 2 (PreOrder _) => class_apply_once preorder_dual : typeclass_instances.

(** We dualize the construction again. *)

Lemma partial_order_dual : forall `(po : PartialOrder A eqA R), PartialOrder eqA (flip R).
Proof.
  intros ; constructor ; firstorder.
Qed.

Hint Extern 2 (PartialOrder _ _) => class_apply_once partial_order_dual : typeclass_instances.

Instance partial_order_morphism `(PartialOrder A eqA R) :
   Proper (eqA ==> eqA ==> iff) R. 
Proof with auto.
  intros.
  rewrite (partial_order_equivalence (eqA:=eqA)).
  unfold relation_conjunction, predicate_intersection. 
  simpl. simpl_relation. split.
    transitivity x... transitivity x0...
    transitivity y... transitivity y0...
Qed.

(** We define overloaded notations for relations which have an instance of PartialOrder. *)

Definition le `{PartialOrder A eqA R} : _ := R.
Infix "<=" := le (at level 70, no associativity)  : order_scope.
Notation " x >= y " := (le (R:=flip _) x y) (at level 70, no associativity)  : order_scope.

Open Local Scope order_scope.

Lemma partial_order_antisym_inv `{PartialOrder A eqA R} :
  forall x y : A, x === y -> x <= y /\ y <= x.
Proof.
  intros.
  rewrite H0. firstorder reflexivity.
Qed.

(* Lemma partial_order_antisym'' `(PartialOrder A eqA R) :  *)
(*   forall x y : A, x <= y -> y <= x -> x === y. *)
(* Proof. *)
(*   intros.  *)
(*   repeat red in H. *)
(*   rewrite H0. split ; reflexivity. *)
(* Qed. *)

(** The dual order. Just [unfold flip] to get back from dual.
   A more complicated version requiring the dual order instance could be used instead but that would only 
   complicate the tactics. *)

Notation " x >= y " := (flip le x y) (at level 70, no associativity)  : order_scope.

(** **** Decidability of the order in [Prop] and [Set]. 
   Note that this does not imply totality, as two elements may still be incomparable. *)

Class DecidablePartialOrder `(PartialOrder A) :=
  partial_order_decidable : forall x y : A, decidable (x <= y).

Class ComputablePartialOrder `(PartialOrder A) :=
  partial_order_dec : forall x y : A, { x <= y } + { ~ x <= y }.

Program Instance computable_decidable `{ComputablePartialOrder A} (x y : A) 
  : Decidable (x <= y).

  Next Obligation.
  Proof.
    unfold decidable.
    destruct (partial_order_dec x y) ; intuition.
  Qed.

(** **** Total Partial Order.
   Dichotomous or linear partial orders (chain). *)

Class TotalPartialOrder `(po : PartialOrder A) :=
  partial_order_total : forall x y : A, x <= y \/ x >= y.

(** With a decision procedure instead of a proof. *)

Class DecidableTotalPartialOrder `(po : PartialOrder A) :=
  partial_order_total_dec : forall x y : A, { x <= y } + { x >= y }.

Program Instance deciable_total_partial_order_total `(po : PartialOrder A, ! DecidableTotalPartialOrder po) 
  : TotalPartialOrder po.

  Next Obligation. 
  Proof. destruct (partial_order_total_dec x y) ; intuition. Qed.

(** ** Strict orders
   A strict (weak) order is irreflexive and transitive. *)

Class StrictOrder {A} eqA `{equ : Equivalence A eqA} (R : relation A) :=
  { strict_order_morphism :> Proper (eqA ++> eqA ++> iff) R ;
    strict_order_irrefl :> Irreflexive R ;
    strict_order_trans :> Transitive R }.

(** Again we define a notation [<] for every relation which is a [StrictOrder]. *)

Definition lt `{StrictOrder A equ R} : _ := R.
Infix "<" := lt (at level 70, no associativity) : order_scope.
Notation " x ~< y " := (complement lt x y) (at level 70, no associativity) : order_scope.
Notation " x > y " := (inverse lt x y) (at level 70, no associativity) : order_scope.

Instance lt_morphism `{StrictOrder A} : Proper (equiv ++> equiv ++> iff) lt.
Proof. intros. typeclasses eauto. Qed.

(** *** Dual *)

Program Definition strict_order_dual `(StrictOrder A eqA R) : StrictOrder (inverse R).
Proof. constructor ; typeclasses eauto. Qed.

Hint Extern 2 (StrictOrder _) => solve [ class_apply @strict_order_dual ] : typeclass_instances.

(** *** Trichotomous or total strict order *)

Class TotalStrictOrder `(StrictOrder A) :=
  strict_order_total : forall x y, x < y \/ x === y \/ x > y.

(** A trichotomous or total strict order with a decision procedure is
   the equivalent of Haskell's [Ord] typeclass. *)

(** **** Ordering.
   We define the [ordering] inductive with respect to a [Equivalence] and [StrictOrder] in order to get the
   proper notations. *)

Section Ordering.
  Context `(so : StrictOrder A eqA ord).
  
  Inductive ordering (x y : A) : Set :=
  | Lower : forall (Hlt : x < y), ordering x y
  | Equal : forall (Heq : x === y), ordering x y
  | Greater : forall (Hgt : x > y), ordering x y.

End Ordering.

(** *** Ord.
   The class [Ord] of total strict orders with a decidable [compare] relation. *)

Class Ord `(so : StrictOrder A eqA ord) :=
  compare : forall x y, ordering so x y.

(** This trivially gives us a total strict order. *)

Program Instance decidable_total_strict_order `(Ord A eqA ordA) : TotalStrictOrder _.

  Next Obligation.
  Proof. destruct (compare x y) ; intuition. Qed.
    
(** **** Min and max.
   Minimum and maximum operations in terms of [compare]. 
   As in Haskell, note that [(max x y, min x y)] is either [(x, y)] or [(y, x)]. *)

Definition max `(Ord A) (x y : A) : A :=
  match compare x y with
    | Lower _ => x
    | Equal _ => y
    | Greater _ => y
  end.

Definition min `(Ord A) (x y : A) : A :=
  match compare x y with
    | Lower _ => x
    | Equal _ => x
    | Greater _ => y
  end.

(** Now we turn to properties of these orders. *)

Ltac autoeq := equivify ; equiv_simplify ; auto.
 
Section TotalStrictOrder_Facts.
  Context `(so : StrictOrder A equ ord).
  Implicit Types x y z : A. 
  
  Program Lemma lt_not_eq : forall x y, x < y -> x =/= y.
  Proof. intros; autoeq. elim (irreflexivity (x:=y) H). Qed.

End TotalStrictOrder_Facts.

Ltac orderify_tac :=
  match goal with
    | [ po : @PartialOrder ?A ?eq ?s ?R ?preo, H : ?R ?x ?y |- _ ] => change R with (@le A eq s R preo po) in H
    | [ po : StrictOrder ?R, H : context [ ?R ?x ?y ] |- _ ] => change R with (lt) in H
    | [ po : @PartialOrder ?A ?eq ?s ?R ?preo |- ?T ] => 
      match T with context C [ R ?x ?y ] => change (R x y) with (@le A eq s R preo po x y) | _ => fail 2 end
    | [ po : StrictOrder ?s ?R |- ?T ] => 
      match T with context C [ R ?x ?y ] => change (R x y) with (lt x y) | _ => fail 2 end
  end.

Ltac orderify := equivify ; repeat orderify_tac.

Ltac equiv_tac :=
  match goal with
    | [ H : @complement ?A ?R ?x ?x |- _] => elim (irreflexivity (x:=x) H)
    | [ |- (* ?x === ?x *) _] => reflexivity
  end.

(* (Ir)Reflexivity. *)

Ltac order_refl := 
  match goal with
    | [ H : (?x < ?x)%type |- _] => elim (irreflexivity (x:=x) H)
  end.

Ltac reflex := order_refl || reflexivity.

(* (Anti)Symmetry *)

Ltac order_antisymmetry R := 
  match goal with
    | [ |- @equiv ?A ?eq ?s ?x ?y] => apply (antisymmetry (A:=A) (eqA:=@equiv A eq s) (R:=R) (x:=x) (y:=y))
  end.

Ltac order_antisym := 
  match goal with
    | [ H : @le ?A ?eq ?equ ?R ?pre ?po ?x ?y, H' : ?y <= ?x |- @equiv ?A ?eq ?equ ?x ?y] => 
      apply (antisymmetry (eqA:=@equiv A eq equ) (R:=@le A eq equ R pre po) H H')
  end.

Ltac antisym := order_antisym.

(* Transitivity. *)

Ltac order_trans := 
  match goal with
    | [ H : @lt _ _ _ ?R _ ?x ?y, H' : @lt _ _ _ ?R _ ?y ?z |- (?x < ?z)%type] => apply (transitivity (R:=R) H H')
    | [ H : @le _ _ _ ?R _ ?x ?y, H' : (?y <= ?z)%type |- (?x <= ?z)%type] => apply (transitivity (R:=R) H H')
  end.

(** Immediate resolution of goals on orders. *)

Ltac order_tac := order_refl || order_antisym || order_trans || equiv_tac.

(** Simplify the goal. *)

Ltac strict_order_simplify_one :=
  match goal with
    | [ |- ~ ?x < ?y] => let name := fresh "Hlt" x y in red ; intro name
    | [ |- context [ (?x > ?y)%type]] => unfold flip
    | [ H : ?x > ?y |- _] => unfold flip in H
    | [ |- ?x >= ?y] => unfold flip
    | [ H : context [ (?x >= ?y)%type ] |- _ ] => unfold flip in H
  end.

Ltac order_simplify := repeat (strict_order_simplify_one || equiv_simplify_one).

(** Saturate the goal with deducible (in)equalities. *)

Ltac order_sat_one :=
  match goal with
    | [ H : @le ?A ?eq ?e ?R ?pre ?po ?x ?y, H' : @le ?A ?eq ?e ?R ?pre ?po ?y ?x |- _ ] => 
      let name := fresh "Heq" x y in 
        add_hypothesis name 
        (antisymmetry (A:=A) (eqA:=eq) (equ:=e) (R:=R) H H')

    | [ H : @le ?A ?eq ?e ?R ?pre ?po ?x ?y, H' : @le ?A ?eq ?e ?R ?pre ?po ?y ?z |- _ ] => 
      let name := fresh "Hlt" x z in 
        add_hypothesis name (transitivity (A:=A) (R:=@le A eq e R pre po) (x:=x) (y:=y) (z:=z) H H')

    | [ H : @lt ?A ?eq ?e ?R ?so ?x ?y, H' : @lt ?A ?eq ?e ?R ?so ?y ?z |- _ ] => 
      let name := fresh "Hlt" x z in 
        add_hypothesis name (transitivity (A:=A) (R:=@lt A eq e R so) (x:=x) (y:=y) (z:=z) H H')
    | [ H : @lt ?A ?eq ?e ?R ?so ?x ?y |- _ ] => 
      let name := fresh "Hneq" x y in add_hypothesis name (@lt_not_eq A eq R e so x y H)
  end.

Ltac order_sat := order_sat_one.

(** Combine with [setoid_sat] to get a decision procedure on [==], [<] and [<=]. 
   At each iteration we try to cut the search by applying one of the immediately solving tactics. *)

Ltac order_saturate := try order_tac ;
  repeat (auto ; order_sat ; order_simplify ; auto ; try order_tac ; try contradiction).

(** Just use saturation. *)

Ltac order := intros ; orderify ; order_simplify ; autoeq ; order_saturate.

(** Our little helper tactic. *)

Ltac triv := orderify ; subst* ;
  repeat (red ; intros) ; try contradiction ; try discriminates ; solve [ order ].

Program Instance less_morphism `(o : Ord A eqA less) : Proper (equiv ++> equiv ++> iff) less.

  Next Obligation.
  Proof.
    repeat (red ; intros).
    split ; intros ; order.
  Qed.

(** Conversely, the complement of a partial order is a strict order. *)
(*    We do not use it though. *)

(* Definition partial_order_complement `(PartialOrder A eqA ord) :=  *)
(*   flip partial_order_restriction. *)

(* Program Definition partial_order_complement_strict `(PartialOrder A eqA ord) : *)
(*   StrictOrder _ partial_order_complement := strict_order_dual. *)

(** *** Complementation.

   The complement of a strict order is a partial order. Totality is required
   in the proof of transitivity for example. Complement orders are used by default
   when using "<=" in a context where a strict order is defined or "<" when a partial order is considered.
   *)

Program Instance iff_iff_impl_impl_morphism : Proper (impl --> iff ++> impl) impl.

  Solve Obligations using simpl_relation.

Program Instance strict_complement_preorder `(TotalStrictOrder A eqA ord) : PreOrder (complement ord).

  Next Obligation.
  Proof.
    unfold complement. red. intros.
    destruct(strict_order_total x x) as [Hlt|[Heq|Hgt]]; triv. 
  Qed.

  Next Obligation.
  Proof. 
    unfold complement. red. intros.
    destruct(strict_order_total x y) as [Hlt|[Heq|Hgt]]; triv. 
  Qed.

Program Instance total_strict_partial_order `(TotalStrictOrder A eqA ord) : PartialOrder eqA (complement ord).

  Next Obligation.
  Proof.
    intros. split ; intros. 
    split. rewrite H1. reflexivity.
    rewrite H1. reflexivity.
    destruct H1. 
    destruct(strict_order_total x x0) ; intuition contradiction.
  Qed.

Program Instance total_strict_total_partial_order `(to : TotalStrictOrder A)
  : TotalPartialOrder (total_strict_partial_order to).

  Next Obligation.
  Proof.
    destruct(strict_order_total x y); firstorder order.
  Qed.

Notation " x /< y " := (@le _ _ _ (@complement _ _) _ _ x y) (at level 50).
Notation " x />= y " := ((@flip _ _ _ (@le _ _ _ (@complement _ _) _ _)) x y) (at level 50).

(** *** Extension and restriction. 

   We can extend or restrict using the equality to get stricter or laxer orders. *) 

Unset Implicit Arguments.

Definition partial_order_restriction {A eqA} ord `{po : PartialOrder A eqA ord} : relation A :=
  fun x y => x <= y /\ x =/= y.

Notation " x </= y " := (partial_order_restriction _ x y) (at level 50).
Notation " x </=^ y " := (partial_order_restriction (inverse _) x y) (at level 50).

Lemma flip_restriction : forall `(po : PartialOrder A eqA ord) (x y : A), 
  flip (partial_order_restriction ord) x y === partial_order_restriction (flip ord) x y.
Proof.
  split ; intros H ; destruct H ; split; auto with *. 
Qed.

Lemma restriction_dual : 
  forall `(po : PartialOrder A eqA ord) (x y : A), 
    x </= y <-> y </=^ x.
Proof.
  intros. firstorder auto with relations.
Qed.

Hint Unfold partial_order_restriction flip.

Ltac my_simplify := 
  auto with typeclass_instances ; 
  try red ; unfold flip, impl, arrow ;
  program_simpl ; repeat (red ; intro ; intros) ; try tauto ; try ( solve [ intuition ]).

Ltac obligation_tactic ::= my_simplify.

Program Instance and_sym : Symmetric and. 
Program Instance and_trans : Transitive and.

Program Instance or_sym : Symmetric or.

Program Instance le_equiv_morphism `(PartialOrder A) : Proper (equiv ++> equiv ++> iff) le :=
  proper.

Instance partial_order_restriction_morphism `(PartialOrder A eqA ord) :
  Proper (eqA ==> eqA ==> iff) (partial_order_restriction ord).
Proof. intros. reduce.
  unfold partial_order_restriction. 
  rewrite H0, H1. reflexivity.
Qed.

Instance subrelation_relation_equivalence : subrelation
  (@relation_equivalence A)
  (pointwise_relation A (pointwise_relation A iff)).
Proof. firstorder. Qed.

Lemma partial_order_equiv `{PartialOrder A eqA ord} x y : eqA x y <-> (ord x y /\ ord y x).
Proof. intros. 
  setoid_rewrite (partial_order_equivalence (eqA:=eqA)). 
  firstorder.
Qed.

Program Definition partial_order_restriction_strict `(PartialOrder A eqA ord) : 
  StrictOrder (partial_order_restriction ord).
Proof. constructor ; intros. typeclasses eauto.
  reduce_goal.
  unfold partial_order_restriction in *.
  destruct_conjs. elim (irreflexivity H1).

  reduce_goal.
  unfold partial_order_restriction in *.
  destruct_conjs. 
  assert(x <= z) by (transitivity y ; auto) ; intuition.
  intro. rewrite H5 in H0. destruct H2. rewrite partial_order_equiv. intuition.
Qed.

About partial_order_restriction_strict.
    
Ltac check_not_partial_evar X :=
  match X with
    | partial_order_restriction ?E => first [ not_evar E | fail 2 ]
    | _ => idtac
  end.

Hint Extern 2 (StrictOrder _) => class_apply_once partial_order_restriction_strict : 
  typeclass_instances.

(** We extend a strict order by just including [==] in the relation. *)

Definition strict_order_extension `(so : StrictOrder A eqA ord) (x y : A) :=
  x < y \/ x === y.

Program Instance strict_order_extension_morphism `(so : StrictOrder A eqA ord) : 
  Proper (equiv ++> equiv ++> iff) (strict_order_extension so).

  Next Obligation.
  Proof.
    unfold strict_order_extension ; order. 
  Qed.
    

Typeclasses Opaque strict_order_extension.

Definition strict_order_extension_preorder `(so : StrictOrder A eqA (equ:=equ) ord)
  : PreOrder (strict_order_extension so).
Proof. intros.
  constructor. red. right ; reflexivity.

  red. unfold strict_order_extension in *.
  intuition ; order.
  right ; reflexivity.
Qed.

Ltac check_not_strict_order_extension_evar X :=
  match X with
    | strict_order_extension ?E => first [ not_evar E | fail 2 ]
    | _ => idtac
  end.

Hint Extern 3 (PreOrder _) => class_apply_once strict_order_extension_preorder : typeclass_instances.

Program Definition strict_order_extension_partial_order `(so : StrictOrder A eqA ord)
  : PartialOrder eqA (strict_order_extension so).
Proof. constructor ; intros ; firstorder order. 
  rewrite H. reflexivity.
Qed.

Hint Extern 3 (PartialOrder _ _) => 
  class_apply_once strict_order_extension_partial_order : typeclass_instances.

Notation " x <\/= y " := (le (R:=strict_order_extension _) x y) (at level 50).
Notation " x </= y " := (lt (R:=partial_order_restriction _) x y) (at level 50).

Ltac order_simplify_notations :=
  match goal with
    | [ |- _ </= _ ] => do 2 red ; split
    | [ |- _ <\/= _ ] => do 2 red ; split
    | [ H : ?x </= ?y |- _ ] => destruct H
    | [ H : ?x <\/= ?y |- _ ] => destruct H
  end.

Ltac order_simplify ::= repeat (order_simplify_notations || strict_order_simplify_one || equiv_simplify_one).

Lemma le_not_lt : forall `(ord : PartialOrder A) (x y z : A), x <= y -> ~ (y <= x /\ x =/= y).
Proof with triv.
  intros. intros [ylex xneqy]. elim xneqy. apply (antisymmetry (R:=R)); auto.
Qed.

(** Some heavy duty instance search is going on there, to find the real definition of [<=], given
   by taking the complement order of the [ord] or [<] parameter of [Ord] and finding its instances
   for [PreOrder] and [PartialOrder]. *)

Lemma le_lt_trans : forall `{ord : StrictOrder A} (x y z : A), x <\/= y -> y < z -> x < z.
Proof. order. Qed.

Lemma lt_le_trans : forall `{ord : StrictOrder A} (x y z : A), x < y -> y <\/= z -> x < z.
Proof. order. Qed.

Lemma le_neq : forall `{ord : StrictOrder A} (x y : A), x <\/= y -> x =/= y -> x < y.
Proof. firstorder order. Qed.

(** Saturate the goal with deducible (in)equalities. *)

Ltac order_sat_trans :=
  match goal with
    | [ H : ?x <= ?y, H' : ?y <= ?z |- _ ] => 
      let name := fresh "Hle" x z in add_hypothesis name (transitive H H')
    | [ H : ?x <\/= ?y, H' : ?y < ?z |- _ ] => 
      let name := fresh "Hlt" x z in add_hypothesis name (le_lt_trans H H')
    | [ H : ?x < ?y, H' : ?y <\/= ?z |- _ ] => 
      let name := fresh "Hlt" x z in add_hypothesis name (lt_le_trans H H')
    | [ H : ?x <\/= ?y, H' : ?x =/= ?y |- _ ] => 
      let name := fresh "Hlt" x y in add_hypothesis name (le_neq H H')
  end.

(** Combine with [setoid_sat] to get a decision procedure on [==], [<] and [<=]. 
   At each iteration we try to cut the search by applying one of the immediately solving tactics. *)

Ltac order_sat ::= order_sat_trans || order_sat_one.

Ltac order_simplify ::= repeat (order_simplify_notations || strict_order_simplify_one || equiv_simplify_one).

Ltac order_sats := repeat order_sat.

Ltac false_order := elimtype False; order.

Lemma le_lt_trans_partial : forall `(PartialOrder A) (x y z : A), x <= y -> y < z -> x < z.
Proof.
  intros.
  destruct H1. assert (xlez:=transitivity H0 H1). split. auto. 
  intro. rewrite H3 in H0. apply H2. 
  rewrite (antisymmetry H0 H1). reflexivity.
Qed.

Lemma gt_not_eq : forall `(StrictOrder A) (x y : A), x > y -> ~ x === y.
Proof. order. elim (irreflexivity H0). Qed.
 
Lemma eq_not_lt : forall `(StrictOrder A) (x y : A), x === y -> ~ x < y.
Proof. order. Qed.

Hint Resolve @gt_not_eq @eq_not_lt : ord.

Lemma eq_not_gt : forall `(StrictOrder A) (x y : A), x === y -> ~ x > y.
Proof. order. Qed.

Lemma lt_not_gt : forall `(StrictOrder A) (x y : A), x < y -> ~ x > y.
Proof. order. unfold flip ; intro. assert (xltx:=transitivity H0 H1). apply (irreflexivity xltx). Qed.

Hint Resolve @eq_not_gt @lt_not_gt : ord.

(** Monotonicity and its dual antitonicity. *)

Class Monotone `(pa : PartialOrder A, pb : PartialOrder B) (f : A -> B) :=
  monotonicity : forall x y, x <= y -> f x <= f y.

(* := -> :> for singleton class alias definition *)
Class Antitone `(pa : PartialOrder A, pb : PartialOrder B) (f : A -> B) :=
  antitonicity :> Monotone pa (partial_order_dual pb) f.

Class GaloisConnection `(pa : PartialOrder A, pb : PartialOrder B, ! Monotone pa pb f, ! Monotone pb pa g) :=
  galois_connection : forall (a : A) (b : B), f a <= b <-> a <= g b.