Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How can I make this reasoning step in Coq ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How can I make this reasoning step in Coq ?


chronological Thread 
  • 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).





Archive powered by MhonArc 2.6.16.

Top of Page