The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Yevgeniy,

> I am interested in using Coq for program extraction from classical
> proofs. Coq seems suitable for this because it produces nice proof
> terms, which are almost programs. So I hope to prove theorems in Coq,
> take proof terms and use them by my own programs to replace the
> classical rule NNPP by call/cc, eliminate computationally irrelevant
> information, normalize, and so on (currently I have a normalizer
> written in Scheme).

  Actually, you can use Coq built-in extraction mechanism for
classical program extraction. What you need to do is to axiomatize
((A->False)->A)->A in Set and to extract it manually using the
"Extract Constant" command.

Parameter Peirce: forall A:Set, ((A->forall C:Set, C)->A)->A.
Extract Constant Peirce => "call/cc"

  Notice the "forall C:Set, C" instead of simply "False" or
"Empty_set". This is because otherwise the extraction tool is too
clever and believes that the inner code of a call to Peirce is dead
code that it can remove.

  Extraction to Scheme uses non-standard macros such as "match-case"
(reminiscent of bigloo?) and many others strange things. I couldn't
find a scheme dialect that can interpret the extracted files as such.

  However, extraction to ocaml works but you need support for callcc
(you may ask the ocaml developers for further informations). I attach
a working example.

  Peirce's axiom in Set interacts badly with impredicativity so that
it was inconsistent in Coq version 7 (unless restricting B to be an
inhabited type which actually is usually the case in
programming-oriented applications of call/cc).

  Based on the generally considered sound set-theoretic interpretation
of the Set-predicative variant of the Calculus of Inductive
Constructions, Peirce's axiom is consistent with Coq version 8 (without
the -set-impredicative option) but programs, well-typed in Coq, that
uses it may fail to preserve typing when extracted (typically when
building types by case analysis on classical programs).

  Hugo Herbelin


Require Import Max.

Parameter Peirce:forall A:Set, ((A->forall C:Set, C)->A)->A.

Theorem infinity : 
  forall f:nat->bool, {b:bool & forall n:nat, {p:nat|n<=p/\f p=b}}.
Proof.
intro f.
apply Peirce;intros H.
apply H.
exists true.
intro n1.
apply Peirce;intros H0.
apply H0.
apply H.
exists false.
intro n2.
cut (f (max n1 n2)=f (max n1 n2)).
pattern (f (max n1 n2)) at 2.
case (f (max n1 n2));intros.
apply H0.
exists (max n1 n2); split; auto with arith.
exists (max n1 n2); split; auto with arith.
trivial.
Defined.

Theorem two_of_infinity :
  forall f:nat->bool, {n1:nat & {n2:nat | n1 < n2 /\ f n1 = f n2}}.
Proof.
intro f.
destruct (infinity f) as (b, Hb).
destruct (Hb 0) as (n1, (_, Hfn1)).
destruct (Hb (S n1)) as (n2, (Hn1n2, Hfn2)).
exists n1.
exists n2.
split; [assumption | transitivity b; [assumption | symmetry;assumption]].
Defined.

Require Import Bool. 

Definition f1 (n:nat) := true.
Definition f2 (n:nat) := false.
Fixpoint f3 (n:nat) : bool := match n with 0 => true | S n => negb (f3 n) end.
Fixpoint f4 (n:nat) : bool := match n with 0 => false | S n => negb (f4 n) 
end.

Parameter print : 
 forall f:nat->bool, {n1:nat & {n2:nat | n1 < n2 /\ f n1 = f n2}} -> 
Empty_set.

Definition test1 := print f1 (two_of_infinity f1).
Definition test2 := print f2 (two_of_infinity f2).
Definition test3 := print f3 (two_of_infinity f3).
Definition test4 := print f4 (two_of_infinity f4).

Extract Constant Peirce =>
 "fun h -> Callcc.callcc (fun k -> h (fun x _ -> Callcc.throw k x))".

Extract Constant print => 
 "fun (_:nat->bool) (ExistS (n1,n2)) ->
  let rec int_of_nat = function O -> 0 | S n -> int_of_nat n + 1 in
  Printf.printf ""n1=%d n2=%d\n"" (int_of_nat n1) (int_of_nat n2)".

Extraction "infinity" test1 test2 test3 test4.

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type bool =
  | True
  | False

type nat =
  | O
  | S of nat

type empty_set = unit (* empty inductive *)

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)

type ('a, 'p) sigS =
  | ExistS of 'a * 'p

(** val max : nat -> nat -> nat **)

let rec max n m =
  match n with
    | O -> m
    | S n' -> (match m with
                 | O -> n
                 | S m' -> S (max n' m'))

(** val negb : bool -> bool **)

let negb = function
  | True -> False
  | False -> True

(** val peirce : (('a1 -> __ -> __) -> 'a1) -> 'a1 **)

let peirce = fun h -> Callcc.callcc (fun k -> h (fun x _ -> Callcc.throw k x))

(** val infinity : (nat -> bool) -> (bool, nat -> nat) sigS **)

let infinity f =
  peirce (fun h ->
    Obj.magic h (ExistS (True, (fun n1 ->
      peirce (fun h0 ->
        Obj.magic h0
          (Obj.magic h (ExistS (False, (fun n2 ->
            match f (max n1 n2) with
              | True -> h0 (max n1 n2) __
              | False -> Obj.magic (max n1 n2)))) __) __)))) __)

(** val two_of_infinity : (nat -> bool) -> (nat, nat) sigS **)

let two_of_infinity f =
  let ExistS (b, hb) = infinity f in let s = hb O in ExistS (s, (hb (S s)))

(** val f3 : nat -> bool **)

let rec f3 = function
  | O -> True
  | S n0 -> negb (f3 n0)

(** val f4 : nat -> bool **)

let rec f4 = function
  | O -> False
  | S n0 -> negb (f4 n0)

(** val print : (nat -> bool) -> (nat, nat) sigS -> empty_set **)

let print = fun (_:nat->bool) (ExistS (n1,n2)) ->
  let rec int_of_nat = function O -> 0 | S n -> int_of_nat n + 1 in
  Printf.printf "n1=%d n2=%d\n" (int_of_nat n1) (int_of_nat n2)

(** val test1 : empty_set **)

let test1 =
  print (fun x -> True) (two_of_infinity (fun x -> True))

(** val test2 : empty_set **)

let test2 =
  print (fun x -> False) (two_of_infinity (fun x -> False))

(** val test3 : empty_set **)

let test3 =
  print (fun x -> f3 x) (two_of_infinity (fun x -> f3 x))

(** val test4 : empty_set **)

let test4 =
  print (fun x -> f4 x) (two_of_infinity (fun x -> f4 x))

type __ = Obj.t

type bool =
  | True
  | False

type nat =
  | O
  | S of nat

type empty_set = unit (* empty inductive *)

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)

type ('a, 'p) sigS =
  | ExistS of 'a * 'p

val max : nat -> nat -> nat

val negb : bool -> bool

val peirce : (('a1 -> __ -> __) -> 'a1) -> 'a1

val infinity : (nat -> bool) -> (bool, nat -> nat) sigS

val two_of_infinity : (nat -> bool) -> (nat, nat) sigS

val f3 : nat -> bool

val f4 : nat -> bool

val print : (nat -> bool) -> (nat, nat) sigS -> empty_set

val test1 : empty_set

val test2 : empty_set

val test3 : empty_set

val test4 : empty_set