PR.axioms

(* 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.