The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

You can never inspect a proof of a proposition when you are trying to 
build a element whose type is in Set or in Type (except a few 
exceptions, to be fully honest, but I don't want to loom into these 
details).

There are a few reasons for that, the main one is that this is what 
Proof has been designed for (you can sweep it away at extraction because 
it does not interract with "real" computations).

A more proof-theoretical reason is that if you combine impredicativity 
(like in Prop) and strong elimination (like in Set), you get something 
were you can proof : ~ forall A. A \/ ~A, in other words, if you could 
build a programm using the details of a proof in Coq, then Coq would be 
inconsistent with classical logic. Which is counter intuitive enough to 
be widely regarded as to be avoided. Though this oddity is quite 
interesting: it is rather easy to build a reasonable logic which is 
inconsistent with classical logic.

Yet another reason would have to do with being compatible with proof 
irrelevance. In which two proofs are considered equal. It has very 
interesting implications on what the type theory can express.

To sum up and answer to your question more directly: there is no way 
that you can complete the proof you're showing in your example (however, 
if you had a proof of { A } + { B }, that would be another deal).


Arnaud Spiwack

Areski Nait Abdallah a écrit :
> > (1) Any tactic works just as well for a goal of type Prop or of type Set
> >     
>
> 	>> exept eventually the elimination of the existential quantifier 
> 	>> (for technical reasons).
>
> These exception and technical reasons is precisely what my question is about.
>
> As an example : Assume
>    1. I have a proof of A \/ B.
>    2. I have a proof of A -> { x : E | P }
>    3. I have a proof of B -> { x : E | P }
> When and under which conditions do I combine these into a proof of 
>    4. A \/ B -> { x : E | P } , 
> and why are these conditions necessary ?
>
>
> Thanks.
> A.
>
>
>   
> > Cody
> >
> > On Wed, 2007-12-19 at 15:17 +0100, Areski Nait Abdallah wrote:
> >     
> > > Hello,
> > >
> > > I am looking for a reference which discusses 
> > >
> > > 	(1) which tactis can be used for solving a goal of type Set, and 
> > >
> > >         (2) covers the rationale for such tactics.
> > >
> > > Thank you for your help,
> > >
> > > Areski
> > >
> > >       
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>