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.
What’s the best way of proving goals like this (even with more mixed second list)?
Permutation
(x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: nil)
(x1 :: x0 :: x3 :: x2 :: x4 :: x5 :: x6 :: x7 :: nil)
Last Qed takes forever (when it shouldn’t) and it seems like a bug: https://gist.github.com/LessnessRandomness/eb1bf0ef8abd9d96766be3b0418f6d5f
Can someone reproduce this behaviour? Using the latest Coq 8.12.0.
The following seems to work on simple explicit valid instances (to be checked further…):
From Coq Require Import List Permutation.
Lemma Permutation_Add_cons A :
forall (a : A) l1 l2 l2', Add a l2 l2' -> Permutation l1 l2 -> Permutation (a :: l1) l2'.
Proof.
intros a l1 l2 l2' Hadd HP.
now etransitivity; [ apply Permutation_cons | apply Permutation_Add, Hadd ].
Qed.
Ltac permutation_solve :=
intros; now repeat (eapply Permutation_Add_cons; [ repeat econstructor | ]).
Goal forall (A : Type) (x0 x1 x2 x3 x4 x5 x6 x7 : A),
Permutation
(x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: nil)
(x1 :: x0 :: x3 :: x2 :: x4 :: x5 :: x6 :: x7 :: nil).
Proof. permutation_solve. Qed.
Goal forall (A : Type) (x0 x1 x2 x3 x4 x5 x6 x7 : A),
Permutation
(x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: nil)
(x1 :: x5 :: x4 :: x2 :: x7 :: x3 :: x6 :: x0 :: nil).
Proof. permutation_solve. Qed.
Now I’m trying to “export” the algorithm to graphviz as flowchart, using the DOT language.
For that I need to set a number for each block (comparison and assignments) to make them distinct. I made such an inductive type:
Require Import List.
Inductive value := x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7.
Inductive variable := aux | num: value -> variable.
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.
Inductive step' :=
| assignments': forall (i: nat) (L: list assignment), step'
| conditional': forall (i: nat) (c: comparison) (positive negative: step'), step'.
Any hints how to better transform a step instance to step' instance such that all indexes of assignments are distinct and all indexes of comparisons are distinct too? I hope I explained my idea good enough.
[Edit:] I gave up on this idea (at least for now). It seems more time-efficient to write all the DOT source manually, just by being careful.
[Edit2:] I added the indexes manually and then managed to transform it into DOT source code, except I didn’t clear out the empty assignments. But I fixed this defect by hand.
Is there any development that proves this lower bound (log_2(n!)) for sorting algorithms? Or maybe there is some good literature about such proof (for humans)?
I want to “cheat” by reusing already done work, if possible, because I don’t understand the proof good enough to formalise it in Coq for now.
Thanks in advance.
“Cheating” is welcome and in fact is not cheating, but a required part of actual research. Homework is different, but it’s also carefully selected to be doable without looking it up.
As you might know, a proof “for humans” appears in the Cormen et al. algorithm textbook, but I assume that’s not enough material for a formalized proof. I have absolutely no clue how hard formalizing that is, and my googling did not find an answer. But it found a paper on a related but different problem, quicksort’s average complexity: for that, the following paper from 2008 claims the first mechanized proof.
Official version (paywalled):
Preprint:
Algorithm textbook by Cormen et al abstracts everything away and uses decision tree model for the proof. Correspondence between sorting algorithm and decision tree isn’t obvious even for me as a human. 
It’s probably some kind of weirdness caused by tinkering in Coq - if something can’t be formalized in Coq (ideally by me so I understand the formalization better), I don’t understand it. 
Now I understand the idea. First expand/transform algorithm into some kind of binary tree (type algorithm') then collect all assignments into leafs of the tree (type algorithm'')…
Inductive algorithm': nat -> Type :=
| leaf': algorithm' 0
| conditional': forall n (c: comparison) (pos_assignments neg_assignments: list assignment) (pos neg: algorithm' n), algorithm' (S n).
Inductive algorithm'': nat -> Type :=
| leaf'': list assignment -> algorithm'' 0
| conditional'': forall n (c: comparison) (pos neg: algorithm'' n), algorithm'' (S n).
The question now is - what I’m doing wrong here? I can’t quite prove the equivalence between two types. Any help is appreciated. 
(Edit: As Yves showed me on stackoverflow by finding a counterexample, the theorem is wrong. Oh well, back to thinking. )
Require Import List Lia.
Set Implicit Arguments.
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; abstract congruence.
+ right; abstract congruence.
+ destruct v, v0; try (left; abstract congruence); (right; abstract congruence).
Defined.
Inductive assignment := assign: variable -> variable -> assignment.
Inductive comparison := GT: forall (more less: value), comparison.
Definition instantation := variable -> nat.
Definition run_assignment (a: assignment) (i: instantation): instantation :=
match a with
| assign v1 v2 => fun x => if variable_eq_dec x v1 then i v2 else i x end.
Fixpoint run_assignment_list (L: list assignment): instantation -> instantation :=
match L with
| nil => fun i => i
| a :: l => fun i => run_assignment_list l (run_assignment a i)
end.
Inductive algorithm': nat -> Type :=
| leaf': algorithm' 0
| conditional': forall n (c: comparison) (pos_assignments neg_assignments: list assignment) (pos neg: algorithm' n), algorithm' (S n).
Inductive algorithm'': nat -> Type :=
| leaf'': list assignment -> algorithm'' 0
| conditional'': forall n (c: comparison) (pos neg: algorithm'' n), algorithm'' (S n).
Definition run_algorithm' n (a: algorithm' n): instantation -> instantation.
Proof.
induction a.
+ exact (fun x => x).
+ intro i. destruct c. exact (if Compare_dec.gt_dec (i (num more)) (i (num less))
then IHa1 (run_assignment_list pos_assignments i)
else IHa2 (run_assignment_list neg_assignments i)).
Defined.
Definition run_algorithm'' n (a: algorithm'' n) (i: instantation): instantation.
Proof.
induction a.
+ exact (run_assignment_list l i).
+ destruct c.
exact (if Compare_dec.gt_dec (i (num more)) (i (num less)) then IHa1 else IHa2).
Defined.
Fixpoint append_assignments n (a: algorithm'' n) (L: list assignment): algorithm'' n :=
match a with
| leaf'' L0 => leaf'' (L ++ L0)
| conditional'' c pos neg => conditional'' c (append_assignments pos L) (append_assignments neg L)
end.
Fixpoint algorithm'_to_algorithm'' n (a: algorithm' n): algorithm'' n :=
match a with
| leaf' => leaf'' nil
| conditional' c Lpos Lneg pos neg =>
conditional'' c (append_assignments (algorithm'_to_algorithm'' pos) Lpos)
(append_assignments (algorithm'_to_algorithm'' neg) Lneg)
end.
Theorem algorithm'_algorithm''_equiv n (a: algorithm' n):
forall (i: instantation) (x: variable), run_algorithm' a i x = run_algorithm'' (algorithm'_to_algorithm'' a) i x.
Proof.
Admitted.
Also I encountered problems when I tried using Program. I can’t prove the following thing (at the end with Admitted).
Edit: I was told to use Function in Zulip and it worked.
Require Import Permutation List Lia Program.
Set Implicit Arguments.
Inductive value := x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7.
Inductive variable := aux | num: value -> variable.
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.
Fixpoint add_assignments (L: list assignment) (s: step): step :=
match s with
| assignments L0 => assignments (L ++ L0)
| conditional c pos neg => conditional c (add_assignments L pos) (add_assignments L neg)
end.
Definition add_assignments_to_algorithm (L: list assignment) (a: algorithm): algorithm :=
match a with
| nil => conditional (GT x0 x1) (assignments L) (assignments L) :: nil
| x :: t => add_assignments L x :: t
end.
Program Fixpoint compactify_algorithm (a: algorithm) {measure (length a)}: algorithm :=
match a with
| nil => nil
| assignments L :: nil => conditional (GT x0 x1) (assignments L) (assignments L) :: nil
| assignments L :: (x :: t) as tail => compactify_algorithm (add_assignments_to_algorithm L tail)
| conditional c pos neg :: t => conditional c pos neg :: compactify_algorithm t
end.
Theorem compactify_algorithm_aux (a: algorithm) (L: list assignment) (x: step):
compactify_algorithm (assignments L :: x :: a) = compactify_algorithm (add_assignments_to_algorithm L (x :: a)).
Proof.
Admitted.
Incidently, in a survey paper recently announced on the Coq Club, there is a link to a formalisation in Isabelle/HOL of the bound of comparisons.
What strategy should be used to prove this result (at the end, with Admitted)? Thanks in advance for any hints.
Hopefully it is true theorem. I already got burned when I had wrong intuition and there was counterexample found.
Edit: Based on counterexample found by Yves on stackoverflow, I added few more conditions to remove all counterexamples of that type.
Edit 2:
Even then there are counterexamples, for example:
assignments (assign aux (num x1) :: assign (num x1) (num x0) :: nil) ::
conditional (GT x0 x1)
(assignments nil)
(assignments (assign (num x0) aux :: nil)) :: nil.
Require Import Permutation List Lia FunInd Recdef.
Set Implicit Arguments.
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; abstract congruence.
+ right; abstract congruence.
+ destruct v, v0; try (left; abstract congruence); (right; abstract 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 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 run_assignment (a: assignment) (i: instantation): instantation :=
match a with
| assign v1 v2 => fun x => if variable_eq_dec x v1 then i v2 else i x end.
Fixpoint run_assignment_list (L: list assignment): instantation -> instantation :=
match L with
| nil => fun i => i
| a :: l => fun i => run_assignment_list l (run_assignment a i)
end.
Fixpoint run_step (s: step) (i: instantation): instantation :=
match s with
| assignments L => run_assignment_list L i
| conditional (GT more less) pos neg =>
if Compare_dec.gt_dec (i (num more)) (i (num less)) then run_step pos i else run_step neg i
end.
Fixpoint run_algorithm (a: algorithm): instantation -> instantation :=
match a with
| nil => fun i => i
| s :: t => fun i => run_algorithm t (run_step s i)
end.
Definition permuting_step (s: step) := forall (i: instantation), is_permutation i (run_step s i).
Definition permuting_algorithm (a: algorithm) := forall (i: instantation), is_permutation i (run_algorithm a i).
(* Additions *)
Fixpoint compact_assignments (a: algorithm): Prop :=
match a with
| nil => True
| assignments L :: assignments L0 :: t => False
| x :: t => compact_assignments t
end.
Fixpoint no_useless_comparisons_in_step (s: step): Prop :=
match s with
| assignments L => True
| conditional (GT a b) pos neg => a <> b /\ no_useless_comparisons_in_step pos /\ no_useless_comparisons_in_step neg
end.
Definition no_useless_comparisons (a: algorithm) := forall x, In x a -> no_useless_comparisons_in_step x.
Definition compact_algorithm (a: algorithm) := compact_assignments a /\ no_useless_comparisons a.
Theorem permuting_algorithm_aux00 (a: algorithm) (s: step):
compact_algorithm (s :: a) -> permuting_algorithm (s :: a) -> permuting_algorithm a /\ permuting_step s.
Proof.
Admitted.