(** * AXIOM BASE After discussions by Andrew Appel, Zhong Shao, Xavier Leroy, 2007. Rationale: Support classical axioms where possible, but preserve the ability to do efficient program extraction on Set functions. That is, if (A B : Set) and (f: A -> B), it must be possible to extract an ML program from f that does *not* manipulate representations of propositions. That is, Set is predicative, but we do not merge Set into Type. Also for this reason we limit the axiom of choice: we use unique_choice that produces propositions, instead of an axiom that produces types or Hilbert's epsilon operator. *) Require ClassicalFacts. (* no axioms in this line *) Require Export Coq.Logic.ClassicalChoice. (* Axioms dependent_unique_choice, relational_choice *) Axiom dep_extensionality: forall (A: Type) (B: A -> Type) (f g : forall x: A, B x), (forall x, f x = g x) -> f = g. Implicit Arguments dep_extensionality. Axiom prop_ext: ClassicalFacts.prop_extensionality. Implicit Arguments prop_ext. (**** LEMMAS ****) Lemma extensionality: forall (A B: Type) (f g : A -> B), (forall x, f x = g x) -> f = g. Proof. intros; apply dep_extensionality; auto. Qed. Implicit Arguments extensionality. Lemma prop_degen: ClassicalFacts.prop_degeneracy. Proof. exact (ClassicalFacts.prop_ext_em_degen prop_ext classic). Qed. Implicit Arguments prop_degen. Lemma proof_irr: ClassicalFacts.proof_irrelevance. Proof. exact (ClassicalFacts.ext_prop_dep_proof_irrel_cic prop_ext). Qed. Implicit Arguments proof_irr.