Library ext

Require Export FunctionalExtensionality.
Require Import ClassicalFacts.

Inductive ext_v := .

This file defines the extensionality properties we use in the formalization. They rely on two axioms of the Coq standard libraries:

Axiom propositional_extensionality : prop_extensionality.

Lemma and_extensionality : ∀ (P Q1 Q2 : Prop), (P → Q1 = Q2) → (P ∧ Q1 ) = (P ∧ Q2 ).
Proof.
intros; apply propositional_extensionality; split; intros [HP HQ].
rewrite <- (H HP); auto.
rewrite (H HP); auto.
Qed.

Lemma arrow_extensionality : ∀ (P Q1 Q2 : Prop), (P → Q1 = Q2) → (P → Q1 ) = (P → Q2 ).
Proof.
intros; apply propositional_extensionality; split; intros HQ HP.
rewrite <- (H HP); auto.
rewrite (H HP); auto.
Qed.

Lemma forall_extensionality : ∀ A (P Q : A → Prop), P = Q → (∀ x, P x ) = (∀ x, Q x ).
Proof. intros A P Q Heq; rewrite Heq; reflexivity. Qed.

Lemma exists_extensionality : ∀ A (P Q : A → Prop), P = Q → (∃ x, P x ) = (∃ x, Q x ).
Proof. intros A P Q Heq; rewrite Heq; reflexivity. Qed.