An overview over the KIV project can be found here

The problem is formulated algebraically. The entire axiomatization can be found in the specification solitaire. The game is formalized as the function *solitaire*, which returns the list of stacks after distributing all cards over the stacks, with the helper function *push*. The latter recurses over the stacks and prepends to the first stack where this is possible.

The idea of the proves is to switch the representation, i.e., we use the function *solix*, which returns the stack of indices (into the original sequence) instead of the cards themselves.

The first theorem solix-to-solitaire states that we can obtain the result of *solitaire* by calculating *solix* of the same cards and then replacing the indices in the stacks by the actual elements. This conversion is done by the function *.tolist*.

This allows us to prove the main theorem by proving the same theorem (found here) over the stack of indices. The proof of this theorem follows the description given by the organizers of the competition, i.e., the proof is decomposed into

- showing that there is an ascending sequence with a length equal to the number of stacks (main lemma theoremx-atleast)
- showing that the existence of a longer sequence is contradictory (main lemma theoremx-atmost-h shows that a longer ascending sequence yields two indices in the same stack)

A few properties about the result of *solix* are needed throughout the proofs and are defined by the predicates *inv* (stacks are nonempty and all indices are within the bounds of the original sequence), *covers* (all indices are covered by the resulting list of stacks) and *ordered* (the indices within each stack are ordered and the corresponding elements are also ordered).

## Leave a Comment

You must be logged in to post a comment.