So, I have a homework - sort 8 values using minimum number of comparisons and prove that it’s optimal solution. The number is 16 using merge-insertion sort and no less comparisons are possible (informally, because log_2(8!) > 15).

Using Coq isn’t part of the homework, but I want to do it anyway. The actual homework won’t contain any Coq proofs.

The source code looks like this - nested "if"s (third levels in one part of the code) and lots of assignments using auxiliary variable t (to swap values around in the array).

```
If (x(1) > x(4)) Then
If (x(0) > x(4)) Then
t = x(0)
x(0) = x(4)
x(4) = x(3)
x(3) = x(2)
x(2) = x(1)
x(1) = t
Else
t = x(1)
x(1) = x(4)
x(4) = x(3)
x(3) = x(2)
x(2) = t
End If
Else
If (x(3) > x(4)) Then
t = x(2)
x(2) = x(4)
x(4) = x(3)
x(3) = t
Else
t = x(2)
x(2) = x(3)
x(3) = t
End If
End If
```

For now I’m trying to define inductive datatype for describing the sort algorithm. Any hints, please?

**[Edit1]** This is what I got. It seems to be correct.

```
Require Import Permutation List Omega.
Inductive value := x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7.
Inductive variable := aux | num: value -> variable.
Definition variable_eq_dec (x y: variable): {x=y} + {x<>y}.
Proof.
destruct x, y.
+ left; auto.
+ right; congruence.
+ right; congruence.
+ destruct v, v0; try (left; congruence); (right; congruence).
Defined.
Inductive assignment := assign: variable -> variable -> assignment.
Inductive comparison := GT: forall (more less: value), comparison.
Inductive step :=
| assignments: forall (L: list assignment), step
| conditional: forall (c: comparison) (positive negative: step), step.
Definition algorithm := list step.
Definition instantation := variable -> nat.
Definition is_increasing (i: instantation) :=
i (num x0) <= i (num x1) /\
i (num x1) <= i (num x2) /\
i (num x2) <= i (num x3) /\
i (num x3) <= i (num x4) /\
i (num x4) <= i (num x5) /\
i (num x5) <= i (num x6) /\
i (num x6) <= i (num x7).
Definition list_of_values (i: instantation) :=
i (num x0) :: i (num x1) :: i (num x2) :: i (num x3) :: i (num x4) :: i (num x5) :: i (num x6) :: i (num x7) :: nil.
Definition is_permutation (i1 i2: instantation) := Permutation (list_of_values i1) (list_of_values i2).
Definition is_sorted (start result: instantation) := is_increasing result /\ is_permutation start result.
Definition run_assignment (values: instantation) (a: assignment): instantation.
Proof.
destruct a as [v1 v2].
exact (fun i => if variable_eq_dec i v1 then values v2 else values i).
Defined.
Definition run_step (values: instantation) (s: step): instantation.
Proof.
induction s.
+ induction L.
- exact values.
- exact (run_assignment IHL a).
+ destruct c.
exact (if Compare_dec.gt_dec (values (num more)) (values (num less)) then IHs1 else IHs2).
Defined.
Definition run_algorithm (values: instantation) (algo: algorithm): instantation.
Proof.
induction algo.
+ exact values.
+ exact (run_step IHalgo a).
Defined.
Definition count_comparisons_in_step (s: step): nat.
Proof.
induction s.
+ exact 0.
+ exact (PeanoNat.Nat.max IHs1 IHs2).
Qed.
Definition do_nothing := assignments nil.
Definition swap (x y: value) :=
assign (num y) aux ::
assign (num x) (num y) ::
assign aux (num x) ::
nil.
Definition step1 := conditional (GT x0 x1) (assignments (swap x0 x1)) do_nothing.
Definition step2 := conditional (GT x2 x3) (assignments (swap x2 x3)) do_nothing.
(* etc *)
```

**[Edit2]** It was fun while it lasted. Because, for example, running ‘simpl’ on goals like this (only 9 steps instead of all 16) takes forever.

```
run_algorithm before (step9 :: step8 :: step7 :: step6 :: step5 :: step4 :: step3 :: step2 :: step1 :: nil) (num x1) <=
run_algorithm before (step9 :: step8 :: step7 :: step6 :: step5 :: step4 :: step3 :: step2 :: step1 :: nil) (num x3)
```

**[Edit3]** Worked around it, using (i believe) smth called preconditions and postconditions.