Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Equivalence for propositional functions


Chronological Thread 
    < Chronological >      < Thread >
  • From: richard <richard.dapoigny AT univ-smb.fr>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Equivalence for propositional functions
  • Date: Wed, 25 Dec 2024 00:09:00 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richard.dapoigny AT univ-smb.fr; spf=Pass smtp.mailfrom=richard.dapoigny AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout01-ext2.partage.renater.fr
  • Dkim-filter: OpenDKIM Filter v2.10.3 zmtaauth05.partage.renater.fr E2FDA201FE
  • Ironport-sdr: 676b4a1a_JV95cufz/DobSYv3e0ZkFO3sxL+oUvqOB2JsVvMJORt5tF4 6vgpkr8CpI1vOsVZel5cl9r0VvVsbwLoanoRq6g==

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