Coq bits

----- Original Coq source -----
Require Extraction.
Extraction Language Haskell.
Set Extraction Optimize.

Module Bits.

Inductive bit: Type :=
| B0
| B1.

Inductive nibble: Type :=
| bits (b0 b1 b2 b3: bit).

Definition nibble_zero (n : nibble): bool :=
  match n with
    | (bits B0 B0 B0 B0) => true
    | (bits _ _ _ _) => false
  end.

Definition nibble_odd (n: nibble): bool :=
  match n with
    | (bits _ _ _ B1) => true
    | (bits _ _ _ _) => false
  end.

Definition nibble_even (n: nibble): bool :=
  negb (nibble_odd n).

Definition nibble_chess (n: nibble): bool :=
  match n with
    | (bits B0 B1 B0 B1) => true
    | (bits B1 B0 B1 B0) => true
    | _ => false
  end.

Theorem test_nibble_zeroity: (nibble_zero (bits B0 B0 B0 B0)) = true.
  reflexivity.
Qed.

Theorem test_nibble_oddity: (nibble_odd (bits B1 B1 B0 B1)) = true.
  reflexivity.
Qed.

Theorem test_nibble_evenity: (nibble_even (bits B1 B0 B1 B0)) = true.
  reflexivity.
Qed.

Theorem test_nibble_chessity: (nibble_chess (bits B1 B0 B1 B0)) = true.
  reflexivity.
Qed.

End Bits.

Recursive Extraction Bits.

----- Converted to Haskell -----

module Main where

import qualified Prelude

data Bool =
   True
 | False

negb :: Bool -> Bool
negb b =
  case b of {
   True -> False;
   False -> True}

data Bit =
   B0
 | B1

bit_rect :: a1 -> a1 -> Bit -> a1
bit_rect f f0 b =
  case b of {
   B0 -> f;
   B1 -> f0}

bit_rec :: a1 -> a1 -> Bit -> a1
bit_rec =
  bit_rect

data Nibble =
   Bits Bit Bit Bit Bit

nibble_rect :: (Bit -> Bit -> Bit -> Bit -> a1) -> Nibble -> a1
nibble_rect f n =
  case n of {
   Bits x x0 x1 x2 -> f x x0 x1 x2}

nibble_rec :: (Bit -> Bit -> Bit -> Bit -> a1) -> Nibble -> a1
nibble_rec =
  nibble_rect

nibble_zero :: Nibble -> Bool
nibble_zero n =
  case n of {
   Bits b0 b1 b2 b3 ->
    case b0 of {
     B0 ->
      case b1 of {
       B0 ->
        case b2 of {
         B0 -> case b3 of {
                B0 -> True;
                B1 -> False};
         B1 -> False};
       B1 -> False};
     B1 -> False}}

nibble_odd :: Nibble -> Bool
nibble_odd n =
  case n of {
   Bits _ _ _ b3 -> case b3 of {
                     B0 -> False;
                     B1 -> True}}

nibble_even :: Nibble -> Bool
nibble_even n =
  negb (nibble_odd n)

nibble_chess :: Nibble -> Bool
nibble_chess n =
  case n of {
   Bits b0 b1 b2 b3 ->
    case b0 of {
     B0 ->
      case b1 of {
       B0 -> False;
       B1 ->
        case b2 of {
         B0 -> case b3 of {
                B0 -> False;
                B1 -> True};
         B1 -> False}};
     B1 ->
      case b1 of {
       B0 ->
        case b2 of {
         B0 -> False;
         B1 -> case b3 of {
                B0 -> True;
                B1 -> False}};
       B1 -> False}}}