How can I prove propositionalism in Coq?

Question

I am trying to prove a replacement theorem about Prop, and I fail. Is it possible to prove the following theorem in coq, and if not, then why not.

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

The fact is that a proof in logic would be an induction. As far as I can see, Prop is not defined inductively. How can one prove such a theorem in Coq?

Answer 1

Here's the answer: the property I was looking for is called propositional extensibility and means that forall pq : Prop, (p <-> q) -> (p = q) . The converse is trivial. This is what is defined in Library Coq.Logic.ClassicalFacts , along with other facts from the classic, 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 EquivThenEqual , use it for rewriting, etc. Thanks to Christopher Mirinsky for pointing out the extension.

Answer 2

What you are looking for is called "extality:"

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 recognize the prevalence of predicates as indicated in the Coq FAQ.

Answer 3

This is propositional extensiveness.

 Lemma blah: forall (PQ: Prop), (forall (f:Prop -> Prop), f Q -> f P) -> P = Q. intros PQ H. apply (H (fun x => x = Q)). reflexivity. Qed. Section S. Hypothesis prop_subst: forall (f : Prop -> Prop) (PQ : Prop), (P <-> Q) -> ((f P) <-> (f Q)). Lemma prop_subst_is_ext: forall PQ, (P <-> Q) -> P = Q. intros. apply blah. intro f. destruct (prop_subst f PQ); assumption. Qed. End S. Check prop_subst_is_ext.