coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Satrajit Roy <satrajit.roy AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Not sure if this is the right forum for beginners' questions, however .....
Date: Fri, 6 Sep 2013 19:27:34 -0400

Why can't I prove:

forall p:Type->Prop, ~(forall q:Type, (p q))->(exists q:Type, ~(p q))

When I can easily prove:

forall p:Type->Prop, exists q, ~p q->~forall q, p q

or prove:

forall p:Type->Prop, ~exists q, p q->forall q, ~p q

or even prove:

forall p:Type->Prop, forall q, p q->~exists q, ~p q

--

Satrajit

[Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Satrajit Roy, 09/07/2013
- Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., t x, 09/07/2013
- Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Adam Chlipala, 09/07/2013
  - Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Andrew Hirsch, 09/08/2013
    - RE: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Shigeo Nishi, 09/08/2013
      - Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Adam Chlipala, 09/08/2013
        
        RE: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Shigeo Nishi, 09/08/2013
        
        Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., t x, 09/08/2013