Library Coq.Logic.PropExtensionalityFacts
Some facts and definitions about propositional and predicate extensionality
We investigate the relations between the following extensionality principles
Table of contents
1. Definitions
2.1 Predicate extensionality <-> Proposition extensionality + Propositional functional extensionality
2.2 Propositional extensionality -> Provable propositional extensionality
2.3 Propositional extensionality -> Refutable propositional extensionality
- Proposition extensionality
- Predicate extensionality
- Propositional functional extensionality
- Provable-proposition extensionality
- Refutable-proposition extensionality
- Extensional proposition representatives
- Extensional predicate representatives
- Extensional propositional function representatives
Set Implicit Arguments.
Provable-proposition extensionality
Refutable-proposition extensionality
Predicate extensionality
Local Notation PredicateExtensionality :=
(forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q).
Propositional functional extensionality
Local Notation PropositionalFunctionalExtensionality :=
(forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q).
Propositional and predicate extensionality
Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality
Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality.
Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality.
Lemma PropExt_and_PropFunExt_imp_PredExt :
PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality.
Theorem PropExt_and_PropFunExt_iff_PredExt :
PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality.