coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matej Kosik <kosik AT fiit.stuba.sk>
- To: Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] How can I make this reasoning step in Coq ?
- Date: Thu, 23 Apr 2009 19:19:13 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Openpgp: id=F248FE18; url=http://altair.sk/uploads/kosik.asc
Edsko de Vries wrote:
>> I have chosen unfortunate notation. I thought, it is obvious. E was
>> meant as a "environment" (set of hypotheses) from which we want to prove
>> succedent. E is not a proposition.
>
> What is the difference? :)
>
> Edsko
>
Aha, there is probably nothing wrong with E.
However, I haven't expressed myself clearly enough in what direction I
wanted to progress.
Lemma foo : (E -> p) -> (E /\ ~p -> False).
helps in the direction I was not interested in.
However, the following:
Lemma bar : forall P : Prop, (~ P -> False) -> P
would help me to prove NNPP. Thus, `bar' must be unprovable too without
loading additional axioms from the classical logic (if NNPP is unprovable).
- [Coq-Club] How can I make this reasoning step in Coq ?, Matej Kosik
- Re: [Coq-Club] How can I make this reasoning step in Coq ?,
Edsko de Vries
- Re: [Coq-Club] How can I make this reasoning step in Coq ?, Yves Bertot
- Re: [Coq-Club] How can I make this reasoning step in Coq ?,
Matej Kosik
- Re: [Coq-Club] How can I make this reasoning step in Coq ?,
Edsko de Vries
- Re: [Coq-Club] How can I make this reasoning step in Coq ?, Matej Kosik
- Re: [Coq-Club] How can I make this reasoning step in Coq ?, Tillmann Rendel
- Re: [Coq-Club] How can I make this reasoning step in Coq ?, Matej Kosik
- Re: [Coq-Club] How can I make this reasoning step in Coq ?,
Edsko de Vries
- Re: [Coq-Club] How can I make this reasoning step in Coq ?, Ezra Cooper
- Re: [Coq-Club] How can I make this reasoning step in Coq ?,
Edsko de Vries
Archive powered by MhonArc 2.6.16.