Verification Challenge - Dependently-typed Programming

Verification of the algorithm described in "On building trees of minimum height" by Richard S. Bird, using Coq

TODO

Prove Lemma 1 (join builds minimum height from combining lmps):

• Given that is a lmp (local minimum pair) in a sequence of trees
• Then there is a tree T of minimum height in which are siblings

Prove auxiliary facts about lmp (local minimum pair):

1. Proof that in an strictly increasing list, the leftmost pair is always an lmp.

2. Proof that in a non-strictly decreasing list, the rightmost pair is always an lmp.

3. Proof that in a list that is not non-strictly decreasing there is always a pair (a, b) for which it holds that . This is a strictly increasing sequence.

From these facts we should be able to conclude that every sequence has an lmp (Thomas: I'm not sure whether we actually need this proof)

Invariants about order on lists:

Lemma 2, 3:

2. Given list [..,x, a, b, y, ..] a >= b ^ y > a -> (a, b) lmp
3. Given list [..,x, a, b, y, ..] a < b ^ b < y ^ x >= a -> (a, b) lmp

Prove that step produces a strictly increasing list (sequence of lmps):

1. Proof that [a] is a strictly increasing list (trivial)
2. Proof that implies that [a, b] is strictly increasing (trivial)
3. From induction on the above 2 base cases, prove that the result of the function step is an strictly increasing list.
   • For this we need to prove that using join in the definition of step is safe. Needs:
     • Proof that in any sequence xs ++ [a,b]: implies that (a,b) is an lmp. (follows from 1.a)
     • Proof that in any sequence xs ++ [t, u, v] ++ ts: implies that (t, u) is an lmp. (follows from Lemma 2)
     • Proof that in any sequence xs ++ [t, u, v] ++ ts: [u,v] ++ ts is increasing & t >= v ^ t >= u => (u, v) is an lmp (follows from Lemma 3)

From the above follows that foldl1 join creates a tree of minimum height. QED.

Possible problems

• Step is not a fixpoint decreasing on one of its arguments, in combination with foldr it is however terminating. How to convince coq?
• There is no fold1, since it is an partial function. is this a problem for us?
• How to deal with 'end of list' (NIL), which can be interpreted as an item of the maximum height.
• The main problem: how to prove that using join on lmps as arguments to a recursive call on step maintains the invariant (that step creates a strictly increasing list).