The axioms for correctness of synthesis.

The correctness of the synthesis cannot be defined from first principles (i.e. directly in Coq) as the underlying type clash.function.t as well as functions map fold and zipWith are stub axioms which is extracted to clash explicitly via the Haskell extraction process in extraction process. However, the automata simulation algorithm is built out of the above mentioned basic functions and therefore it should be possible to prove the correctness provided we have a basic set of compatibility axioms between the concrete version and the synthesized version of the above functions. Here we define these natural compatibility axioms which form the basis of our correctness of synthesis. The axiom fold_spec asserts that folding a function f over the concrete version give function vector u and its synthesized version yield the same result. The map_spec zipWith_spec and constant_spec on the other hand asserts that applying the combinator and then synthesizing is the same as synthesizing and the applying the corresponding clash version of the combinator.