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.

score 8 · Accepted Answer · answered Apr 26 '19 at 15:25

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.

chi · Answer 2 · 2019-04-26T13:12:24.920

6

You are working with types in different sorts.

> Check (Nat.Even 8).
Nat.Even 8
     : Prop

> Check {p:nat | 8=p+p}.
{p : nat | 8 = p + p}
     : Set

A feature of the Coq type system is that you can not eliminate a value whose type is in Prop to obtain something whose type is not in Prop (roughly -- some exception is done by Coq for Prop types which carry no information, like True and False, but we are not in that case). Roughly put you can not use a proof of a proposition for anything but to prove another proposition.

This limitation is unfortunately required to allow Prop to be impredicative (we want forall P: Prop, P->P to be a type in sort Prop) and to be consistent with the law of excluded middle. We can not have everything or we meet Berardi's paradox.

edited Apr 26 '19 at 13:12

answered Apr 26 '19 at 12:55

chi

111,837
3
133
218

1

Can you really not, for example, use `Prop` information to show that a case you've reached is impossible when constructing a `Type`? – luqui Apr 26 '19 at 12:57
@luqui I can't recall, but I think Coq indeed does an exception for inductive types having zero or one trivial constructors, since they carry no "data". A quick experiment seems to confirm this. – chi Apr 26 '19 at 13:09
I'm still a bit confused, does it mean that `div_2_even_number` can **not** be proved? is there any way to define (and extract) `div_2_any_number`? – OrenIshShalom Apr 26 '19 at 13:45
@OrenIshShalom how is `Nat.Even` defined? – luqui Apr 26 '19 at 14:42
`div_2_even_number` can be proved, but not directly from the `Nat.Even` assumption. Think of what it would extract to: if you erase the proofs (`Nat.Even` and `n = p + p`) you are left with a function `nat -> nat`, which should map even numbers to their halves, and which will never be applied to odd numbers (because they do not have proofs of `Nat.Even` in the source language). Therefore `div_2_even_number` has to do at least as much computation as a division by two to construct the result `p : nat`, plus potentially additional work to construct the proof term for `n = p + p`. – Li-yao Xia Apr 26 '19 at 14:43
2

@chi is correct, if the expected type is of sort `Type`, you can only destruct proof terms which are noninformative, and that allows you to destruct proofs of `False` in "impossible cases". – Li-yao Xia Apr 26 '19 at 14:45
1

@luqui here it is: `Nat.Even = fun n : nat => exists m : nat, n = 2 * m : nat -> Prop` – OrenIshShalom Apr 26 '19 at 14:58

Proofs' role in Coq extractions

2 Answers2

Linked