haskell - Proofs' role in Coq extractions

Question

I'm trying to understand what is the role of proofs in Coq extractions. I have the following example of floor integer division by two taken from here. For my first try I used the Admitted keyword:

(*********************)
(* div_2_even_number *)
(*********************)
Definition div_2_even_number: forall n,
  (Nat.Even n) -> {p:nat | n=p+p}.
Proof.
Admitted.

(*************)
(* test_even *)
(*************)
Definition test_even: forall n,
  {Nat.Even n}+{Nat.Even (pred n)}.
Proof.
Admitted.

(********************)
(* div_2_any_number *)
(********************)
Definition div_2_any_number (n:nat):
  {p:nat | n = p+p}+{p:nat | (pred n) = p+p} :=
  match (test_even n) with
  | left h => inl _ (div_2_even_number n h)
  | right h' => inr _ (div_2_even_number (pred n) h')
  end.

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/some_file.hs" div_2_any_number.

When I examine the resulting Haskell file I see that it is indeed missing:

div_2_even_number :: Prelude.Integer -> Prelude.Integer
div_2_even_number =
  Prelude.error "AXIOM TO BE REALIZED"

test_even :: Prelude.Integer -> Prelude.Bool
test_even =
  Prelude.error "AXIOM TO BE REALIZED"

div_2_any_number :: Prelude.Integer -> Prelude.Either Prelude.Integer
                    Prelude.Integer
div_2_any_number n =
  case test_even n of {
   Prelude.True -> Prelude.Left (div_2_even_number n);
   Prelude.False -> Prelude.Right (div_2_even_number (pred n))}

So I figured OK, let's prove div_2_even_number:

(*********************)
(* div_2_even_number *)
(*********************)
Definition div_2_even_number: forall n,
  (Nat.Even n) -> {p:nat | n=p+p}.
Proof.
  intros n0 H.
  unfold Nat.Even in H.
  destruct H as [m0].
  exists m0.
Qed.

But I get the following error:

Error: Case analysis on sort Set is not allowed for inductive definition ex.

What's going on here? I'm obviously missing something here.

Answer 1

Though what chi said is correct, in this case you can actually extract the witness p from the existence proof. When you have a boolean predicate P : nat -> bool, if exists p, P p = true, you can compute some p that satisfies the predicate by running the following function from 0:

find p := if P p then p else find (S p)

You cannot write this function directly in Coq, but it is possible to do so by crafting a special inductive proposition. This pattern is implemented in the choice module of the mathematical components library:

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.

(* == is the boolean equality test *)
Definition even n := exists p, (n == 2 * p) = true.

Definition div_2_even_number n (nP : even n) : {p | (n == 2 * p) = true} :=
  Sub (xchoose nP) (xchooseP nP).

The xchoose : (exists n, P n = true) -> nat function performs the above search, and xchooseP shows that the its result satisfies the boolean predicate. (The actual types are more general than this, but when instantiated to nat they yield this signature.) I have used the boolean equality operator to simplify the code, but it would have been possible to use = instead.

That being said, if you care about running your code, programming in this fashion is terribly inefficient: you need to perform n / 2 nat comparisons to test divide n. It is much better to write a simply typed version of the division function:

Fixpoint div2 n :=
  match n with
  | 0 | 1 => 0
  | S (S n) => S (div2 n)
  end.