coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?

From: Robin Green <greenrd AT greenrd.org>
To: Vincent Aravantinos <vincent.aravantinos AT gmail.com>
Cc: gang chen <gangchen_sh AT yahoo.com>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?
Date: Thu, 14 Feb 2008 10:26:47 +0000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: Systems Research Group, UCD Dublin

On Thu, 14 Feb 2008 10:54:17 +0100
Vincent Aravantinos
<vincent.aravantinos AT gmail.com>
wrote:

> Assume you are given two functions (f:Prop -> nat) and (g:nat ->
> Prop), and then define a F like this:
>
> Definition F (P:Prop) : Prop -> Prop := g (1 + f P).
>
> I don't see any reason why such a function would respect your
> conjecture.

But how can you define a function f : Prop -> nat which yields
different numbers for different propositions, in Coq? You can't do case
analysis on Props.
--
Robin

[Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, gang chen
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Vincent Aravantinos
  - Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Robin Green
    - Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Vincent Aravantinos
      - Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Gyesik Lee
        
        Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Andreas Abel
      - Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Bruno Barras
        
        Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Conor McBride
        
        Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, gang chen