Library TLC.LibMin

Set Implicit Arguments.
From TLC Require Import LibTactics LibLogic LibReflect LibOperation
  LibRelation LibOrder LibEpsilon.
Generalizable Variables A.




Definition lower_bound A (le:binary A) (P:A->Prop) (x:A) :=
  forall y, P y -> le x y.


Definition min_element A (le:binary A) (P:A->Prop) (x:A) :=
  P x /\ lower_bound le P x.


Definition mmin `{Inhab A} (le:binary A) (P:A->Prop) :=
  epsilon (min_element le P).



Definition upper_bound A (le:binary A) (P:A->Prop) (x:A) :=
  forall y, P y -> le y x.


Definition max_element A (le:binary A) (P:A->Prop) (x:A) :=
  P x /\ upper_bound le P x.


Definition mmax `{Inhab A} (le:binary A) (P:A->Prop) :=
  epsilon (max_element le P).



Definition lub A (le:binary A) (P:A->Prop) (x:A) :=
  min_element le (upper_bound le P) x.


Definition glb A (le:binary A) (P:A->Prop) (x:A) :=
  max_element le (lower_bound le P) x.


Lemma upper_bound_inverse : forall A (le:binary A),
  upper_bound le = lower_bound (inverse le).
Proof using.
  extens. intros P x. unfolds lower_bound, upper_bound. iff*.
Qed.

Lemma max_element_inverse : forall A (le:binary A) (P:A->Prop) (x:A),
  max_element le P x = min_element (inverse le) P x.
Proof using.
  extens. unfold max_element, min_element. rewrite* upper_bound_inverse.
Qed.

Lemma mmax_inverse : forall `{Inhab A} (le:binary A) (P:A->Prop),
  mmax le P = mmin (inverse le) P.
Proof using.
  intros. applys epsilon_eq. intros x. rewrite* max_element_inverse.
Qed.



Definition bounded_has_minimal A (le:binary A) :=
  
  forall P,
  ex P ->
  ex (lower_bound le P) ->
  ex (min_element le P).


Lemma mmin_spec : forall `{Inhab A} (le:binary A) (P:A->Prop) m,
  m = mmin le P ->
  ex P ->
  ex (lower_bound le P) ->
  bounded_has_minimal le ->
  min_element le P m.
Proof using.
  intros. subst. unfold mmin. epsilon* m.
Qed.


From TLC Require Import LibNat.


Lemma increment_lower_bound_nat : forall (P : nat->Prop) x,
  lower_bound le P x ->
  ~ P x ->
  lower_bound le P (x + 1)%nat.
Proof using.
  introv hlo ?. intros y ?.
  destruct (eq_nat_dec x y).
    { subst. tauto. }
    { forwards: hlo; eauto. nat_math. }
Qed.

Lemma bounded_has_minimal_nat :
  @bounded_has_minimal nat le.
Proof using.
  intros P [ y ? ].
  cut (
    forall (k x : nat), (y + 1 - x)%nat = k ->
    lower_bound le P x ->
    exists z, min_element le P z
  ). { intros ? [ x ? ]. eauto. }
  induction k; introv ? hlo.
  { false. forwards: hlo; eauto. nat_math. }
  
  
  destruct (prop_inv (P x)).
    { exists x. split; eauto. }
    { eapply (IHk (x + 1)%nat). nat_math. eauto using increment_lower_bound_nat. }
Qed.

Hint Resolve bounded_has_minimal_nat : bounded_has_minimal.


Lemma admits_lower_bound_nat : forall (P : nat->Prop),
  ex (lower_bound le P).
Proof using.
  exists 0%nat. unfold lower_bound. nat_math.
Qed.

Hint Resolve admits_lower_bound_nat : admits_lower_bound.


Lemma bounded_has_maximal_nat :
  @bounded_has_minimal nat (inverse le).
Proof using.
  intros P [ y ? ] [ x h ].
  assert (y <= x).
    { forwards: h. eauto. eauto. }
  
  assert (self_inverse: forall i, i <= x -> (x - (x - i))%nat = i).
    intros. nat_math.
  forwards [ z [ ? hz ]]: (@bounded_has_minimal_nat (fun i => P (x - i)%nat)).
    { exists (x - y)%nat. rewrite self_inverse by eauto. eauto. }
    { eauto using admits_lower_bound_nat. }
  exists (x - z)%nat.
  clear dependent y.
  split; [ assumption | ].
  intros y ?.
  assert (y <= x).
    { forwards: h. eauto. eauto. }
  forwards: hz (x - y)%nat.
    { rewrite self_inverse by eauto. eauto. }
  unfold inverse. nat_math.
Qed.

Hint Resolve bounded_has_maximal_nat : bounded_has_minimal.

Lemma mmin_spec_nat:
  forall (P:nat->Prop) m,
  m = mmin le P ->
  ex P ->
  P m /\ (forall x, P x -> m <= x).
Proof using.
  introv E Q. applys (@mmin_spec _ _ _ P m E Q).
  applys admits_lower_bound_nat.
  applys bounded_has_minimal_nat.
Qed.



Definition MMin `{Inhab A} `{Le A} := mmin le.


Definition MMax `{Inhab A} `{Le A} := mmax le.