Library Coq.Logic.PropExtensionalityFacts


Some facts and definitions about propositional and predicate extensionality
We investigate the relations between the following extensionality principles
  • Proposition extensionality
  • Predicate extensionality
  • Propositional functional extensionality
  • Provable-proposition extensionality
  • Refutable-proposition extensionality
  • Extensional proposition representatives
  • Extensional predicate representatives
  • Extensional propositional function representatives
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

Set Implicit Arguments.

Definitions

Propositional extensionality


Provable-proposition extensionality


Refutable-proposition extensionality


Predicate extensionality


Propositional functional extensionality


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.

Propositional extensionality and provable proposition extensionality


Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality.

Propositional extensionality and refutable proposition extensionality


Lemma PropExt_imp_RefutPropExt : PropositionalExtensionality -> RefutablePropositionExtensionality.