Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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

Notation PropositionalExtensionality :=
  (forall A B : Prop, (A <-> B) -> A = B).

Provable-proposition extensionality

Notation ProvablePropositionExtensionality :=
  (forall A:Prop, A -> A = True).

Refutable-proposition extensionality

Notation RefutablePropositionExtensionality :=
  (forall A:Prop, ~A -> A = False).

Predicate extensionality

Notation PredicateExtensionality :=
  (forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q).

Propositional functional extensionality

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.PredicateExtensionality -> PropositionalExtensionality
Proof.PredicateExtensionality -> PropositionalExtensionality
  intros Ext A B Equiv.Ext:PredicateExtensionality
A, B:Prop
Equiv:A <-> B
A = B 
  change A with ((fun _ => A) I).Ext:PredicateExtensionality
A, B:Prop
Equiv:A <-> B
(fun _ : True => A) I = B
  now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B).
Qed.

Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality.PredicateExtensionality ->
PropositionalFunctionalExtensionality
Proof.PredicateExtensionality ->
PropositionalFunctionalExtensionality
  intros Ext A P Q Eq.Ext:PredicateExtensionality
A:Type
P, Q:A -> Prop
Eq:forall x : A, P x = Q x
P = Q apply Ext.Ext:PredicateExtensionality
A:Type
P, Q:A -> Prop
Eq:forall x : A, P x = Q x
forall x : A, P x <-> Q x intros x.Ext:PredicateExtensionality
A:Type
P, Q:A -> Prop
Eq:forall x0 : A, P x0 = Q x0
x:A
P x <-> Q x now rewrite (Eq x).
Qed.

Lemma PropExt_and_PropFunExt_imp_PredExt :
  PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality.PropositionalExtensionality ->
PropositionalFunctionalExtensionality ->
PredicateExtensionality
Proof.PropositionalExtensionality ->
PropositionalFunctionalExtensionality ->
PredicateExtensionality
  intros Ext FunExt A P Q Equiv.Ext:PropositionalExtensionality
FunExt:PropositionalFunctionalExtensionality
A:Type
P, Q:A -> Prop
Equiv:forall x : A, P x <-> Q x
P = Q
  apply FunExt.Ext:PropositionalExtensionality
FunExt:PropositionalFunctionalExtensionality
A:Type
P, Q:A -> Prop
Equiv:forall x : A, P x <-> Q x
forall x : A, P x = Q x intros x.Ext:PropositionalExtensionality
FunExt:PropositionalFunctionalExtensionality
A:Type
P, Q:A -> Prop
Equiv:forall x0 : A, P x0 <-> Q x0
x:A
P x = Q x now apply Ext.
Qed.

Theorem PropExt_and_PropFunExt_iff_PredExt :
  PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality.PropositionalExtensionality /\
PropositionalFunctionalExtensionality <->
PredicateExtensionality
Proof.PropositionalExtensionality /\
PropositionalFunctionalExtensionality <->
PredicateExtensionality
  firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt.
Qed.

(**********************************************************************)

Propositional extensionality and provable proposition extensionality

Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality.PropositionalExtensionality ->
ProvablePropositionExtensionality
Proof.PropositionalExtensionality ->
ProvablePropositionExtensionality
  intros Ext A Ha; apply Ext; split; trivial.
Qed.

(**********************************************************************)

Propositional extensionality and refutable proposition extensionality

Lemma PropExt_imp_RefutPropExt : PropositionalExtensionality -> RefutablePropositionExtensionality.PropositionalExtensionality ->
RefutablePropositionExtensionality
Proof.PropositionalExtensionality ->
RefutablePropositionExtensionality
  intros Ext A Ha; apply Ext; split; easy.
Qed.