How can I prove propositional extensionality in Coq?

Question

I'm trying to prove a substitution theorem about Prop, and I'm failing miserably. Can the following theorem be proven in coq, and if not, why not.

  Theorem prop_subst:
    forall (f : Prop -> Prop) (P Q : Prop), 
      (P <-> Q) -> ((f P) <-> (f Q)).

The point is that the proof, in logic, would be by induction. Prop isn't defined inductively, as far as I can see. How would such a theorem be proven in Coq?

Answer 1

Here's the answer: The property I was looking for is called propositional extensionality, and means that forall p q : Prop, (p <-> q) -> (p = q). The converse, is trivial. This is something that is defined in Library Coq.Logic.ClassicalFacts, together with other facts from classical, i.e., non-intuitionistic logic. The above definition is called prop_extensionality, and can be used as follows: Axiom EquivThenEqual: prop_extensionality. Now you can apply the EquivThenEqual, use it for rewriting, etc. Thanks to Kristopher Micinski for pointing towards extensionality.

Answer 2

What you are looking for is called "extensionality:"

http://coq.inria.fr/V8.1/faq.html#htoc41

http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html

http://en.wikipedia.org/wiki/Extensionality

EDIT:

You can admit predicate extensionality, as noted in the Coq FAQ.

Answer 3

This is propositional extentionality.

Lemma blah: forall (P Q: Prop), (forall (f:Prop -> Prop), f Q -> f P) -> P = Q.
  intros P Q H.
  apply (H (fun x => x = Q)).
  reflexivity.
Qed.

Section S.

Hypothesis prop_subst:
  forall (f : Prop -> Prop) (P Q : Prop), 
    (P <-> Q) -> ((f P) <-> (f Q)).

Lemma prop_subst_is_ext: forall P Q, (P <-> Q) -> P = Q.
  intros.
  apply blah.
  intro f.
  destruct (prop_subst f P Q); assumption.
Qed.

End S.

Check prop_subst_is_ext.