Proof Driven Development sample

1.Proof.v

Require Import List.
Import ListNotations.

Fixpoint reversed { A: Type } (xs: list A) :=
  match xs with
  | nil => nil
  | x :: xs' => reversed xs' ++ [x]
end.

Lemma reversed_sub: 
  forall (A: Type) (xs ys: list A), reversed (xs ++ ys) = reversed(ys) ++ reversed(xs).
Proof.
  intros A xs ys. induction xs.
  -
    simpl.
    rewrite app_nil_r. reflexivity.
  -
    simpl. rewrite IHxs.
    rewrite app_assoc_reverse. reflexivity.
Qed.

Theorem matches_double_reversed : forall (A: Type) (xs: list A), reversed (reversed xs) = xs.
Proof.
  intros A xs. induction xs.
  - simpl. reflexivity.
  - simpl.
    rewrite reversed_sub. rewrite IHxs.
    simpl. reflexivity.
Qed.

Require Extraction.
Extraction Language Haskell.
Extraction "out.hs" reversed.

main.hs

import Data.List
import Out

toHList :: (List a) -> [a]
toHList lis =
  case lis of {
  Nil -> [];
  Cons x lis' -> [x] ++ (toHList lis')}

toList :: [a] -> List a
toList lis =
  case lis of {
  [] -> Nil;
  (x:xs') -> app (Cons x Nil) (toList xs')}

main :: IO()
main = do
  mapM_ putStrLn $ map show $ toHList $ reversed $ toList [1,2,3,4,5]

out.hs

module Out where

import qualified Prelude

data List a =
   Nil
 | Cons a (List a)

app :: (List a1) -> (List a1) -> List a1
app l m =
  case l of {
   Nil -> m;
   Cons a l1 -> Cons a (app l1 m)}

reversed :: (List a1) -> List a1
reversed xs =
  case xs of {
   Nil -> Nil;
   Cons x xs' -> app (reversed xs') (Cons x Nil)}