The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Am Dienstag, den 14.12.2010, 18:37 -0800 schrieb Daniel Schepler:
> 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.
> 

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

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

> 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)))).


> 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?

I may be stating the obvious, but the axioms you give are inconsistent
as can be shown by: 

Require Import ClassicalFacts.

Lemma inconsistent : False.
assert(H : forall (B:Prop) (b1 b2:B), b1 = b2).
apply proof_irrelevance_cci. apply classic.
apply not_proof_irrelevance ; trivial.
Qed.

Print Assumptions inconsistent.

The reason is that call_cc, with the proposed reduction rule, would
probably allow for non-terminating Programs which provide inhabitants
for any type. 


-- 
Regards
Christian