**September 8, 2014** - Tagged as: coq, en.

- Provide some guidance for starters who are interested in proving algorithms correct.
- Demonstrate how to prove properties of functions with accumulators and functions that work on list indexes, instead of elements of the list.
- Demonstrate how to use "timeout" arguments to convince Coq that a function is really terminating on all inputs.

Require Import List.

Import ListNotations.

Open Scope list_scope.

Require Import Arith.

Require Import Omega.

Require Import Permutation.

- Result should be a permutation of it's parameter.
- Result should be in sorted order.

Inductive sorted : list nat → Prop :=

| Sorted_nil : sorted []

| Sorted_singleton : ∀ e, sorted [e]

| Sorted_cons : ∀ e h t, sorted (h :: t) → e ≤ h → sorted (e :: h :: t).

Inductive Sorting_correct (algo : list nat → list nat) :=

| sorting_correct_intro :

(∀ l, sorted (algo l) ∧ Permutation l (algo l)) → Sorting_correct algo.

Fixpoint insert (i : nat) (l : list nat) :=

match l with

| [] ⇒ [i]

| h :: t ⇒ if leb i h then i :: h :: t else h :: insert i t

end.

Definition insertion_sort := fold_right insert [].

***** Exercise: 2 stars. Use insert_perm and transitivity, symmetry and reflexivity of Permutation.

***** Exercise: 2 star. Use insert_sorted_preserve.

Theorem insertion_sort_correct : Sorting_correct insertion_sort.

Proof.

constructor. split. apply insertion_sort_sorted. apply Permutation_insertion_sort.

Qed.

Fixpoint find_min_idx_aux (l : list nat) (min min_idx cur_idx : nat) : nat :=

match l with

| [] ⇒ min_idx

| h :: t ⇒ if leb h min then find_min_idx_aux t h cur_idx (S cur_idx)

else find_min_idx_aux t min min_idx (S cur_idx)

end.

Definition find_min_idx (l : list nat) : nat :=

match l with

| [] ⇒ 0

| h :: t ⇒ find_min_idx_aux t h 0 1

end.

Lemma find_min_idx_len_inv : ∀ l m mi ci r,

find_min_idx_aux l m mi ci = r →

mi < ci →

r < ci + length l.

find_min_idx_aux l m mi ci = r →

mi < ci →

r < ci + length l.

Inductive member {A} : A → list A → Prop :=

| Member_head : ∀ e l, member e (e :: l)

| Member_tail : ∀ e h t, member e t → member e (h :: t).

Lemma member_preserved_by_perm : ∀ A (l : list A) l' e,

Permutation l l' →

member e l →

member e l'.

Permutation l l' →

member e l →

member e l'.

***** Exercise: 5 stars. find_min_idx really returns index of smallest element.

Fixpoint replace {A} (l : list A) (idx : nat) (e : A) : list A :=

match l with

| [] ⇒ []

| h :: t ⇒

match idx with

| 0 ⇒ e :: t

| S idx' ⇒ h :: replace t idx' e

end

end.

***** Exercise: 1 star. First part of correctness proof of replace.

***** Exercise: 1 star. Second part of correctness proof of replace. replace preserves length of the list.

Fixpoint selection_sort_aux (l : list nat) (step : nat) : list nat :=

match step with

| 0 ⇒ l

| S step' ⇒

match l with

| [] ⇒ []

| h :: t ⇒

match find_min_idx_aux t h 0 1 with

| 0 ⇒ h :: selection_sort_aux t step'

| S min ⇒ nth min t 0 :: selection_sort_aux (replace t min h) step'

end

end

end.

Definition selection_sort (l : list nat) : list nat := selection_sort_aux l (length l).

***** Exercise: 2 stars.

Lemma replace_perm_head : ∀ n h t,

n < length t →

Permutation (h :: t) (nth n t 0 :: replace t n h).

n < length t →

Permutation (h :: t) (nth n t 0 :: replace t n h).

***** Exercise: 3 stars. Use replace_perm_head.

***** Exercise: 2 stars. Use member_replace and find_min_idx_correct.

Lemma swap_min_replace : ∀ h t min_idx,

find_min_idx (h :: t) = S min_idx →

(∀ e, member e (replace t min_idx h) → nth min_idx t 0 ≤ e).

find_min_idx (h :: t) = S min_idx →

(∀ e, member e (replace t min_idx h) → nth min_idx t 0 ≤ e).

***** Exercise: 1 star.

***** Exercise: 2 stars. Use member_preserved_by_perm.

Lemma min_preserved_by_perm : ∀ m l l',

Permutation l l' →

(∀ e, member e l → m ≤ e) →

(∀ e, member e l' → m ≤ e).

Permutation l l' →

(∀ e, member e l → m ≤ e) →

(∀ e, member e l' → m ≤ e).

***** Exercise: 4 stars. Selection sort returns sorted.

***** Exercise: 1 star. Show that selection sort is correct.

Fixpoint rev_at {A} idx (l : list A) : list A :=

match idx with

| 0 ⇒ rev l

| S idx' ⇒

match l with

| [] ⇒ []

| h :: t ⇒ h :: rev_at idx' t

end

end.

Fixpoint map_rest_aux {A} (l : list A) (f : list A → list A) (timeout : nat) : list A :=

match timeout with

| 0 ⇒ l

| S timeout' ⇒

match f l with

| [] ⇒ []

| h :: t ⇒ h :: map_rest_aux t f timeout'

end

end.

Definition map_rest {A} (l : list A) (f : list A → list A) : list A :=

map_rest_aux l f (length l).

Lemma Permutation_map_rest :

∀ A (f : list A → list A),

(∀ (l : list A), Permutation l (f l)) →

(∀ (l : list A), Permutation l (map_rest l f)).

∀ A (f : list A → list A),

(∀ (l : list A), Permutation l (f l)) →

(∀ (l : list A), Permutation l (map_rest l f)).

Definition flip_pancakes (l : list nat) : list nat :=

let min_idx := find_min_idx l in

rev_at 0 (rev_at min_idx l).

Definition pancake_sort (l : list nat) : list nat := map_rest l flip_pancakes.

***** Exercise: 2 stars. Use transitivity of permutation and Permutation_rev_at.

***** Exercise: 1 star. Use Permutation_flip_pancakes.

Lemma min_permutation : ∀ e l,

(∀ e', member e' l → e ≤ e') →

(∀ l', Permutation l l' →

(∀ e', member e' l' → e ≤ e')).

(∀ e', member e' l → e ≤ e') →

(∀ l', Permutation l l' →

(∀ e', member e' l' → e ≤ e')).

***** Exercise: 1 star. flip_pancakes preserves the length.

***** Exercise: 4 stars. We can use rev_at to move smallest element to the end of the list, and then to the beginning of the list. Very tricky. Feel free to cheat.

***** Exercise: 3 stars. flip_pancakes moves smallest element to the head of the list.

***** Exercise: 4 stars. You need a lot of lemmas we defined before, and it's a very long proof. Still not as hard as find_min_idx_correct.

Theorem pancake_sort_correct : Sorting_correct pancake_sort.

Proof.

constructor. intro. split. apply pancake_sorted. apply Permutation_pancake_sort.

Qed.