Minimization

Minimization.v

From Coq Require Import Lia.

Section TERMINATION.

  Inductive terminate (P : nat -> Prop) : nat -> Prop :=
  | found : forall n, P n -> terminate P n
  | step : forall n, terminate P (S n) -> terminate P n
  .

  Fixpoint terminate_ind_dep
    (P : nat -> Prop)
    (Q : forall n, terminate P n -> Prop)
    (case_found : forall n (H : P n), Q n (found P n H))
    (case_step : forall n (T : terminate P (S n)), Q (S n) T -> Q n (step P n T))
    n (T : terminate P n) {struct T} : Q n T :=
    match T with
    | found _ n H => case_found n H
    | step _ n T => case_step n T (terminate_ind_dep P Q case_found case_step (S n) T)
    end.

  Lemma terminate_downward_closed P : forall m n, terminate P n -> m <= n -> terminate P m.
  Proof.
    intros m n T LE.
    induction LE.
    - assumption.
    - eapply IHLE. eapply step. eapply T.
  Qed.

  Lemma terminate_zero P : (exists n, P n) -> terminate P 0.
  Proof.
    intros E. destruct E as [m H]. eapply terminate_downward_closed.
    - eapply found. eapply H.
    - lia.
  Qed.

End TERMINATION.

Section MINIMIZATION.

  Context (P : nat -> Prop).
  Context (dec : forall n, {P n} + {~ P n}).

  Lemma step_when_false : forall n, ~ P n -> terminate P n -> terminate P (S n).
  Proof.
    intros n H T.
    destruct T.
    - exfalso; tauto.
    - assumption.
  Defined.

  Fixpoint minimize_from (n : nat) (T : terminate P n) {struct T} : nat :=
    match dec n with
    | left _ => n
    | right H => minimize_from (S n) (step_when_false n H T)
    end.

  Definition minimize (E : exists n, P n) : nat := minimize_from 0 (terminate_zero P E).

  Lemma minimize_from_true n T : P (minimize_from n T).
  Proof.
    induction T using terminate_ind_dep.
    - simpl. destruct (dec n).
      + eauto.
      + exfalso; tauto.
    - simpl. destruct (dec n).
      + eauto.
      + eapply IHT.
  Qed.

  Lemma minimize_from_false n T : forall m, n <= m < minimize_from n T -> ~ P m.
  Proof.
    induction T using terminate_ind_dep.
    - intros m RANGE.
      simpl in RANGE. destruct (dec n).
      + exfalso; lia.
      + exfalso; eauto.
    - intros m RANGE.
      simpl in RANGE. destruct (dec n).
      + exfalso; lia.
      + assert (CASE : n = m \/ S n <= m < minimize_from (S n) T) by lia.
        destruct CASE.
        * subst. eauto.
        * eapply IHT. eauto.
  Qed.

  Lemma minimize_true E : P (minimize E).
  Proof.
    unfold minimize. eapply minimize_from_true.
  Qed.

  Lemma minimize_minimal E : forall n, P n -> minimize E <= n.
  Proof.
    enough (NOT_FOUND : forall n, n < minimize E -> ~ P n).
    { intros n H.
      assert (CASE : n < minimize E \/ minimize E <= n) by lia.
      destruct CASE.
      - exfalso. eapply NOT_FOUND; eauto.
      - eauto.
    }
    unfold minimize.
    intros n LT.
    assert (RANGE : 0 <= n < minimize_from 0 (terminate_zero P E)) by lia.
    eapply minimize_from_false. eauto.
  Qed.

End MINIMIZATION.