The Coq mailing list

[Daniel Schepler <dschepler AT scalable-networks.com>]

I was playing around with a "call_cc" axiom and found a few surprises 
regarding my understanding of what eliminations from Prop to Type are 
forbidden by Coq...

Axiom call_cc: forall {A B:Type},
  ( (A->B) -> A ) -> A.

My expected execution semantics for call_cc would be that call_cc saves a 
copy 
of the current execution state, and calls the given function with cont:A->B.  
If cont is ever called, it rewinds to the saved execution state and causes 
call_cc to return the argument given to cont.

Definition classic : forall P:Prop, P \/ ~P :=
  fun P:Prop => call_cc (fun cont =>
  or_intror _ (fun p:P => cont (or_introl _ p))).

So far so good... in terms of execution, this first returns a synthetic 
"proof" 
of ~P.  If that "proof" is ever called, its argument is a proof of P, so it 
rewinds execution to the call to classic and instead returns that proof of P.

Definition NNPP : forall P:Prop, ~~P -> P :=
  fun (P:Prop) (nnp:~~P) =>
  call_cc (fun cont => False_rect P (nnp cont)).

Again, no surprises here.  This calls nnp with a synthetic proof of ~P; in 
order for nnp to try to produce an instance of False, it's eventually going 
to 
have to call the proof of ~P, and then we rewind to the call of NNPP and 
return the argument to ~P as a proof of P.

Definition not_all_not_ex: forall (A:Type) (P:A->Prop),
  (~ forall a:A, ~ P a) -> exists a:A, P a :=
  fun (A:Type) (P:A->Prop) (nan:~ forall a:A, ~ P a) =>
call_cc (fun cont => False_rect (exists a:A, P a)
  (nan (fun (a:A) (pa:P a) => cont
    (ex_intro (fun a:A => P a) a pa)))).

Same idea... it calls nan with a synthetic proof of "forall a:A, ~ P a", and 
nan is eventually going to have to call it with some a in A and a proof of P 
a, which we use to rewind to not_all_not_ex and return a proof of the 
existence statement.

Definition not_and_or_not: forall P Q:Prop,
  ~(P/\Q) -> (~P \/ ~Q) :=
  fun (P Q:Prop) (nand:~(P/\Q)) =>
  call_cc (fun cont => or_introl _ (fun p:P =>
    cont (or_intror _ (fun q:Q => nand (conj p q))))).

Fill in a similar interpretation here...

But to my surprise, I was also able to define type-valued versions of 
classic, 
not_all_not_ex, and not_and_or_not:

Definition classic_dec : forall P:Prop, {P} + {~P} :=
  fun P:Prop => call_cc (fun cont =>
  right _ (fun p:P => cont (left _ p))).

Definition not_all_not_example: forall (A:Type) (P:A->Prop),
  (~ forall a:A, ~ P a) -> { a:A | P a } :=
  fun (A:Type) (P:A->Prop) (nan:~ forall a:A, ~ P a) =>
call_cc (fun cont => False_rect { a:A | P a }
  (nan (fun (a:A) (pa:P a) => cont
    (exist (fun a:A => P a) a pa)))).

Definition not_and_or_not_dec: forall P Q:Prop,
  ~(P/\Q) -> {~P} + {~Q} :=
  fun (P Q:Prop) (nand:~(P/\Q)) =>
  call_cc (fun cont => left _ (fun p:P =>
    cont (right _ (fun q:Q => nand (conj p q))))).

Based on these examples, I was able to prove that (assuming something you'd 
expect to be true regarding the semantics of call/cc) proof_irrelevance is no 
longer valid:

Axiom partial_call_cc_semantics:
  forall (A B:Type) (a:A) (f:B->A),
  call_cc (fun cont => f (cont a)) = a.

Lemma not_proof_irrelevance:
  ~ (forall (P:Prop) (p1 p2:P), p1 = p2).
Proof.
intro proof_irrelevance.
pose (p1 := fun (p: forall n:nat, ~True) => p 0 I).
pose (p2 := fun (p: forall n:nat, ~True) => p 1 I).
assert (p1 = p2).
apply proof_irrelevance.
assert (not_all_not_example _ _ p1 =
        not_all_not_example _ _ p2).
rewrite H; trivial.
unfold not_all_not_example in H0.
unfold p1 in H0; unfold p2 in H0.
rewrite 2 partial_call_cc_semantics in H0.
discriminate H0.
Qed.

So my question is: why is Coq allowing those eliminations?  And would there 
be 
some alternative way to formulate the call_cc axiom such that 
proof_irrelevance would still be valid, but call_cc could still be used with 
general Types?

Also, it's not at all clear to me whether a version of Coq implementing 
call_cc could guarantee termination of programs.  For example, I think 
not_all_not_ex, if called on a statement involving an inductive type like 
nat, 
could essentially end up iterating through the nats searching for one which 
satisfies the desired statement.  And it seems that e.g. classic isn't 
guaranteed to return a correct value; even if there is some proof of P, 
classic could incorrectly return its synthetic proof of ~P and never be 
called 
on it (heh).  On the other hand, of course there isn't an algorithm which 
could correctly return a truth value of P in general.  So I guess the main 
use 
of call_cc would be as a thought experiment: even if it were implemented, 
there would still be no way for an execution to produce an instance of False; 
so call_cc and therefore classic etc. are (intuitively) consistent.
-- 
Daniel Schepler