Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Equivalence for propositional functions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equivalence for propositional functions


Chronological Thread 
    < Chronological >      < Thread >
  • From: Théo Winterhalter <theo.winterhalter AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Equivalence for propositional functions
  • Date: Wed, 25 Dec 2024 01:01:45 +0100
  • Authentication-results: mail2-relais-roc.national.inria.fr; dkim=none (message not signed) header.i=none; spf=SoftFail smtp.mailfrom=theo.winterhalter AT inria.fr; dmarc=fail (p=none dis=none) d=inria.fr
Yes, with exactly the  same proof. You can substitute y for x in the goal and thus you only need to prove f x <-> f x which holds by reflexivity.

On 25 Dec 2024, at 00:09, richard <richard.dapoigny AT univ-smb.fr> wrote:

Dear coq users,

In Coq it is possible to prove image equality for functions :

Theorem eq_img: forall {X:Type} (f: X->X) (x y :X), x = y -> f x = f y.

However, is it possible to prove similarly an equivalence for propositional functions (assuming classical logic)? :

Theorem eq_fprop: forall {X:Type} (f: X->Prop) (x y :X), x = y -> f x <-> f y.

Thanks for your help.
Richard



Archive powered by MHonArc 2.6.19+.

Top of Page