bubble.v

Require Import ZArith.
Require Import List.
Require Import Program.Wf.
Import ListNotations.

(** Copied from https://github.com/tchajed/strong-induction *)

(** Here we prove the principle of strong induction, induction on the natural
numbers where the inductive hypothesis includes all smaller natural numbers. *)

Require Import PeanoNat.

Section StrongInduction.

  Variable P:nat -> Prop.

  (** The stronger inductive hypothesis given in strong induction. The standard
  [nat ] induction principle provides only n = pred m, with [P 0] required
  separately. *)
  Hypothesis IH : forall m, (forall n, n < m -> P n) -> P m.

  Lemma P0 : P 0.
  Proof.
    apply IH; intros.
    exfalso; inversion H.
  Qed.

  Hint Resolve P0.

  Lemma pred_increasing : forall n m,
      n <= m ->
      Nat.pred n <= Nat.pred m.
  Proof.
    induction n; cbn; intros.
    apply le_0_n.
    induction H; subst; cbn; eauto.
    destruct m; eauto.
  Qed.

  Hint Resolve le_S_n.

  (** * Strengthen the induction hypothesis. *)

  Local Lemma strong_induction_all : forall n,
      (forall m, m <= n -> P m).
  Proof.
    induction n; intros;
      match goal with
      | [ H: _ <= _ |- _ ] =>
        inversion H
      end; eauto.
  Qed.

  Theorem strong_induction : forall n, P n.
  Proof.
    eauto using strong_induction_all.
  Qed.

End StrongInduction.

Tactic Notation "strong" "induction" ident(n) := induction n using strong_induction.

(** end of copy *)

Definition lexopair (p1 p2 : nat * nat) : Prop :=
  match p1, p2 with
  | (x1, y1), (x2, y2) => x1 < x2 \/ x1 = x2 /\ y1 < y2
  end.

Theorem lexopair_wf : well_founded lexopair.
Proof.
  unfold well_founded.
  intros [x y]. generalize dependent y.
  strong induction x.
  intros y. constructor. intros [x' y'] [H1 | [H1 H2]].
  - now apply H.
  - subst.
    strong induction y'. constructor.
    intros [x'' y'']. unfold lexopair.
    intros [H3 | [H3 H4]].
    + now apply H.
    + subst. apply H0; trivial. omega.  Qed.

Program Fixpoint bubble' acc min xs
        {measure (length acc + length xs, length xs) (lexopair)} :=
  match xs with
  | [] =>
    match acc with
    | [] => [min]
    | x :: xs => min :: bubble' [] x xs
    end
  | x :: xs =>
    if Z_le_gt_dec min x
    then bubble' (x :: acc) min xs
    else bubble' (min :: acc) x xs
  end.
Obligation 1.
Proof.
  left. simpl. omega.
Qed.

Obligation 2.
Proof.
  right. simpl. split; omega.
Qed.

Obligation 3.
Proof.
  right. simpl. split; omega.
Qed.

Obligation 4.
Proof.
  apply measure_wf. apply lexopair_wf.
Qed.

Definition bubble (xs : list Z) : list Z :=
  match xs with
  | [] => []
  | x :: xs' => bubble' [] x xs'
  end.