The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Richard,

You don’t need classical logic for eq_fprop, but if you are willing to assume propositional extensionality [1] rewriting will be easier. 

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

Proof.

  intros * Ha. split; intro Hb; subst;

    exact Hb.

Qed.

Axiom prop_ext : forall (P Q : Prop), (P <-> Q) -> P = Q.

(* assuming prop_ext *)

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

Proof.

  intros * Ha.

  eapply prop_ext.

  exact Ha.

Qed.

Best, 

Mukesh 

[1] https://github.com/coq/coq/wiki/CoqAndAxioms

On 24 Dec 2024, at 23: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