(* Version: 17.09. *)

# Axiomatic Assumptions

For our development, we have to extend Coq with two well known axiomatic assumptions, namely functional extensionality and propositional extensionality. The latter entails proof irrelevance.

## Functional Extensionality

We import the axiom from the Coq Standard Library and derive a utility tactic to make the assumption practically usable.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Program.Tactics.

Tactic Notation "nointr" tactic(t) :=
let m := fresh "marker" in
pose (m := tt);
t; revert_until m; clear m.

Ltac fext := nointr repeat (
match goal with
[ |- ?x = ?y ] =>
(refine (@functional_extensionality_dep _ _ _ _ _) ||
refine (@forall_extensionality _ _ _ _) ||
refine (@forall_extensionalityP _ _ _ _) ||
refine (@forall_extensionalityS _ _ _ _)); intro
end).

## Propositional Extensionality

We state the axiom of propositional extensionality directly and use it to prove proof irrelevance.
Axiom pext : forall P Q : Prop, (P <-> Q) -> (P = Q).

Lemma pi {P : Prop} (p q : P) : p = q.
Proof.
assert (P = True) by (apply pext; tauto). subst. now destruct p,q.
Qed.