sort_stdpp_itauto.v

From Cdcl Require Import Itauto.
From stdpp Require Import prelude.

Inductive Sorted : list nat -> Prop :=
| sorted_nil : Sorted []
| sorted_singleton : forall n, Sorted [n]
| sorted_cons : forall n m p, n <= m -> Sorted (m :: p) -> Sorted (n :: m :: p).

#[local] Hint Constructors Sorted : core.

Fixpoint insert n l :=
  match l with
  | [] => [n]
  | (x :: y) => if decide (n <= x) then n :: x :: y else x :: insert n y
  end.

Lemma sorted_insert : forall x l, Sorted l -> Sorted (insert x l).
Proof.
  induction l; simpl.
  - itauto.
  - destruct l; simpl; case_decide; intros H0.
    * itauto.
    * constructor; itauto (lia||auto).
    * inversion H0; subst; itauto.
    * simpl in IHl; case_decide.
      + inversion H0; subst; constructor; itauto lia.
      + inversion H0; subst; constructor; itauto lia.
Qed.

#[local] Hint Resolve sorted_insert : core.

Fixpoint sort l :=
  match l with
  | [] => []
  | x :: l => insert x (sort l)
  end.

Lemma sort_sorts : forall l, Sorted (sort l).
Proof.
  induction l; simpl; itauto.
Qed.

#[local] Hint Resolve sort_sorts : core.

Inductive permutation {A} : list A -> list A -> Prop :=
| perm_nil : permutation [] []
| perm_cons : forall l l' x, permutation l l' -> permutation (x :: l) (x :: l')
| perm_swap : forall l x y, permutation (x :: y :: l) (y :: x :: l)
| perm_trans : forall a b c, permutation a b -> permutation b c -> permutation a c.

#[local] Hint Constructors permutation : core.

Example permutation_ex1 : permutation [1;2] [2;1].
Proof. itauto. Qed.

Lemma permutation_sym {A} : forall (a b : list A), permutation a b -> permutation b a.
Proof.
  intros a b Ha; induction Ha; itauto eauto.
Qed.

#[local] Hint Resolve permutation_sym : core.

Lemma permutation_app_head {A} : forall (l tl tl' : list A),
    permutation tl tl' -> permutation (l ++ tl) (l ++ tl').
Proof.
  induction l; intros; simpl; itauto.
Qed.

#[local] Hint Resolve permutation_app_head : core.

Lemma insert_perm : forall x l, permutation (x :: l) (insert x l).
Proof.
  induction l; intros; simpl.
  - itauto.
  - case_decide; itauto eauto.
Qed.

#[local] Hint Resolve insert_perm : core.

Lemma sort_perm : forall l, permutation l (sort l).
Proof.
  induction l; simpl; itauto eauto.
Qed.

#[local] Hint Resolve sort_perm : core.

Definition is_sorting_algorithm f := forall l, permutation l (f l) /\ Sorted (f l).

Theorem insert_sort_is_sorting_algorithm : is_sorting_algorithm sort.
Proof.
  unfold is_sorting_algorithm; itauto.
Qed.