(** * Selection:  Selection Sort, With Specification and Proof of Correctness*)
(**
  This sorting algorithm works by choosing (and deleting) the smallest
  element, then doing it again, and so on.  It takes O(N^2) time.

  You should never* use a selection sort.  If you want a simple
  quadratic-time sorting algorithm (for small input sizes) you should
  use insertion sort.  Insertion sort is simpler to implement, runs
  faster, and is simpler to prove correct.   We use selection sort here
  only to illustrate the proof techniques.

     *Well, hardly ever.  If the cost of "moving" an element is _much_
  larger than the cost of comparing two keys, then selection sort is
  better than insertion sort.  But this consideration does not apply in our
  setting, where the elements are  represented as pointers into the
  heap, and only the pointers need to be moved.

  What you should really never use is bubble sort.  Bubble sort
  would be the wrong way to go.  Everybody knows that!
  https://www.youtube.com/watch?v=k4RRi_ntQc8
*)

(* ################################################################# *)
(** * The Selection-Sort Program  *)

From VFA Require Import Perm.
From Coq Require Export Lists.List.  (* for exercise involving [List.length] *)

(** Find (and delete) the smallest element in a list. *)

Fixpoint select (x: nat) (l: list nat) : nat * list nat :=
match l with
|  nil => (x, nil)
|  h::t => if x <=? h
               then let (j, l') := select x t in (j, h::l')
               else let (j, l') := select h t in (j, x::l')
end.

(** Now, selection-sort works by repeatedly extracting the smallest element,
   and making a list of the results. But the following attempted definition
   fails: *)

Fail Fixpoint selsort l :=
match l with
| i::r => let (j,r') := select i r
        in j :: selsort r'
| nil => nil
end.

(** _Error: Recursive call to [selsort] has principal argument equal
  to [r'] instead of [r]_.  That is, the recursion is not _structural_, since
  the list [r'] is not a structural sublist of [i::r].  One way to fix the
  problem is to use Coq's [Function] feature, and prove that
  [length r' < length (i::r)].  Later in this chapter, we'll show that approach.

  Instead, here we solve this problem is by providing "fuel", an additional
  argument that has no use in the algorithm except to bound the
  amount of recursion.  The [n] argument, below, is the fuel. *)

Fixpoint selsort l n {struct n} :=
match l, n with
| x::r, S n' => let (y,r') := select x r
              in y :: selsort r' n'
| nil, _ => nil
| _::_, O => nil  (* Oops!  Ran out of fuel! *)
end.

(** What happens if we run out of fuel before we reach the end
   of the list?  Then WE GET THE WRONG ANSWER. *)

Example out_of_gas: selsort [3;1;4;1;5] 3 <> [1;1;3;4;5].
Proof.
simpl.
intro.
discriminate.
Qed.

(** What happens if we have have too much fuel?  No problem. *)

Example too_much_gas: selsort [3;1;4;1;5] 10 = [1;1;3;4;5].
Proof.
simpl.
reflexivity.
Qed.

(** The [selection_sort] algorithm provides just enough fuel. *)

Definition selection_sort l := selsort l (length l).

Example sort_pi: selection_sort [3;1;4;1;5;9;2;6;5;3;5] = [1;1;2;3;3;4;5;5;5;6;9].
Proof.
unfold selection_sort.
simpl.
reflexivity.
Qed.

(** Now we repeat (from [Sort]) the specification of a correct
    sorting algorithm: it rearranges the elements into a list that is
    totally ordered. *)

Inductive sorted: list nat -> Prop :=
 | sorted_nil: sorted nil
 | sorted_1: forall i, sorted (i::nil)
 | sorted_cons: forall i j l, i <= j -> sorted (j::l) -> sorted (i::j::l).

Definition is_a_sorting_algorithm (f: list nat -> list nat) :=
  forall al, Permutation al (f al) /\ sorted (f al).

(* ################################################################# *)
(** * Proof of Correctness of Selection sort *)

(** Here's what we want to prove. *)

Definition selection_sort_correct : Prop :=
    is_a_sorting_algorithm selection_sort.

(** For the exercises below, you may uncomment the next line and use
    the techniques and definitions from the [Multiset] chapter to
    prove the results. If you do that, make sure to leave the theorem
    statements unchanged. Note that there is no need to use multisets:
    they are completely optional. *)

(* Require Import Multiset. *)

(** We'll start by working on part 1, permutations. *)

(** First, let's prove that [select] gives us back a permutation
    of its input. *)

Local Hint Constructors Permutation.

Lemma select_perm': forall x l y r,
  (y, r) = select x l -> Permutation (x :: l) (y :: r).
Proof. (* WORKED IN CLASS *)
  intros x l. generalize dependent x.
  induction l as [ | h t]; intros x y r Hsel; simpl in Hsel.
  - inversion Hsel. subst. auto.
  - bdestruct (x <=? h).
    + destruct (select x t) as (j, l') eqn:Hd. inversion Hsel. subst. eauto.
    + destruct (select h t) as (j, l') eqn:Hd. inversion Hsel. subst. eauto.
Qed.

(** **** Exercise: 2 stars, standard (select_perm)  *)

(** Hints:  After destructing [select x l], you should be
    able to quickly finish with the lemma above. If you're
    using multisets, [contents_perm] could be helpful. *)

Lemma select_perm: forall x l,
  let (y,r) := select x l in Permutation (x::l) (y::r).
Proof. (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, standard (selection_sort_perm)  *)

(** Hints: Induct on [n]. The lemma just proved above will be helpful;
    but, the [let] expression might get in the way of immediately
    applying it. You can [assert] an instantiated form of the lemma,
    including the [let], for a particular [x] and [l], then use
    rewriting to make use of the lemma. The standard library theorem
    [Permutation_length] could also be helpful. If you're using
    multisets, [same_contents_iff_perm] could be helpful. *)

Lemma selsort_perm:
  forall n,
  forall l, length l = n -> Permutation l (selsort l n).
Proof. (* FILL IN HERE *) Admitted.

Theorem selection_sort_perm:
  forall l, Permutation l (selection_sort l).
Proof. (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, standard (select_smallest)  *)

(** Hints: You do not need [induction]. Helpful lemmas include
    [select_perm] and [Forall_perm]. *)

Lemma select_smallest_aux:
  forall x al y bl,
    Forall (fun z => y <= z) bl ->
    select x al = (y,bl) ->
    y <= x.
Proof. (* FILL IN HERE *) Admitted.

(** Hint: Induct on [al], but leave [x] universally quantified
    in the inductive hypothesis. *)

Theorem select_smallest:
  forall x al y bl, select x al = (y,bl) ->
     Forall (fun z => y <= z) bl.
Proof. (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, standard (selection_sort_sorted)  *)

(** Hint: You do not need [induction]. Helpful lemmas include
    [selsort_perm] and [Forall_perm].*)

Lemma selection_sort_sorted_aux:
  forall y bl,
   sorted (selsort bl (length bl)) ->
   Forall (fun z : nat => y <= z) bl ->
   sorted (y :: selsort bl (length bl)).
Proof.
 (* FILL IN HERE *) Admitted.

(** Hints: Induct on the length of [al], leaving [al] universally
    quantified in the inductive hypothesis.  Useful lemmas include
    [selection_sort_sorted_aux] and [select_perm].  You might also
    find use for [select_smallest] or [Permutation_length]. *)

Theorem selection_sort_sorted: forall al, sorted (selection_sort al).
Proof. (* FILL IN HERE *) Admitted.
(** [] *)

(** Now we wrap it all up.  *)

Theorem selection_sort_is_correct: selection_sort_correct.
Proof.
split. apply selection_sort_perm. apply selection_sort_sorted.
Qed.

(* ################################################################# *)
(** * Recursive Functions That are Not Structurally Recursive *)

(** [Fixpoint] in Coq allows for recursive functions where some
  parameter is structurally recursive: in every call, the argument
  passed at that parameter position is an immediate substructure
  of the corresponding formal parameter.  For recursive functions
  where that is not the case -- but for which you can still prove
  that they terminate -- you can use a more advanced feature of
  Coq, called [Function]. *)

Require Import Recdef.  (* needed for [measure] feature *)

Function selsort' l {measure length l} :=
match l with
| x::r => let (y,r') := select x r
        in y :: selsort' r'
| nil => nil
end.

(** When you use [Function] with [measure], it's your obligation to
    prove that the measure actually decreases. *)

Proof.
intros.
pose proof (select_perm x r).
rewrite teq0 in H.
apply Permutation_length in H.
simpl in *.
omega.
Defined.

(** The proof must end with [Defined] instead of [Qed], otherwise you
    can't compute with the function in Coq. *)

Compute selsort' [3;1;4;1;5;9;2;6;5].

(** You won't want to unfold [selsort'] (or anything defined with
    [Function]) in proofs. Instead, rewrite with [selsort'_equation],
    which was automatically defined by the [Function] command. *)

Check selsort'_equation.

(** **** Exercise: 3 stars, standard (selsort'_perm)  *)

(** Hint: Follow the same strategy as [selsort_perm]. *)

Lemma selsort'_perm:
  forall n,
  forall l, length l = n -> Permutation l (selsort' l).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)



(* Tue Jan 28 13:58:40 EST 2020 *)