coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Vincent Aravantinos <vincent.aravantinos AT gmail.com>
To: gang chen <gangchen_sh AT yahoo.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?
Date: Thu, 14 Feb 2008 10:54:17 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:subject:date:to:x-mailer:from; b=a9baeqkMhoExXOco/D9kP++hA7pOQeIEE9j8oa43SLhO5oXxEz0wt/1kcKdumpLGP6xADS73iNqNmT5fsidQ9QNshiEPStR+PYBTv9Zp0aO0rWi947tesb15O/xJv88ycf06rHkAxETwBdYCYNYLGmYB7ZncOvynhe/Wzk0o2+Y=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Le 14 f�vr. 08 � 00:17, gang chen a �crit :

More precisely, is the assertion

Goal equiv : forall (F : Prop->Prop) (A B : Prop),
(A<->B)->((F A)<->(F B)).

provable ?

I believe this conjecture is false without further restriction on F.

(I'm not a specialist so I'm not sure the following reasonning is ok. Many people on this list are more qualified than I am, so if I'm wrong we will know it quickly :)

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.

Vincent

[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