Mercurial > cpdt > repo

comparison src/Universes.v @ 436:5d5e44f905c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changes during more coqdoc hacking
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 15:41:06 -0400
parents a54a4a2ea6e4
children 8077352044b2
comparison
equal deleted inserted replaced
435:a54a4a2ea6e4 436:5d5e44f905c7
774 match goal with 774 match goal with
775 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity 775 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity
776 end. 776 end.
777 Qed. 777 Qed.
778 778
779 (* begin hide *)
780 Require Eqdep_dec.
781 (* end hide *)
782
779 (** These corollaries are special cases of proof irrelevance. In developments that only need proof irrelevance for equality, there is no need to assert full irrelevance. 783 (** These corollaries are special cases of proof irrelevance. In developments that only need proof irrelevance for equality, there is no need to assert full irrelevance.
780 784
781 Another facet of proof irrelevance is that, like excluded middle, it is often provable for specific propositions. For instance, [UIP] is provable whenever the type [A] has a decidable equality operation. The module [Eqdep_dec] of the standard library contains a proof. A similar phenomenon applies to other notable cases, including less-than proofs. Thus, it is often possible to use proof irrelevance without asserting axioms. 785 Another facet of proof irrelevance is that, like excluded middle, it is often provable for specific propositions. For instance, [UIP] is provable whenever the type [A] has a decidable equality operation. The module [Eqdep_dec] of the standard library contains a proof. A similar phenomenon applies to other notable cases, including less-than proofs. Thus, it is often possible to use proof irrelevance without asserting axioms.
782 786
783 %\bigskip% 787 %\bigskip%
841 exists f : forall x : A, B x, 845 exists f : forall x : A, B x,
842 forall x : A, R x (f x) 846 forall x : A, R x (f x)
843 ]] 847 ]]
844 848
845 This axiom lets us convert a relational specification [R] into a function implementing that specification. We need only prove that [R] is truly a function. An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs. We also simplify the statement of the theorem by considering only non-dependent function types. *) 849 This axiom lets us convert a relational specification [R] into a function implementing that specification. We need only prove that [R] is truly a function. An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs. We also simplify the statement of the theorem by considering only non-dependent function types. *)
850
851 (* begin hide *)
852 Require RelationalChoice.
853 (* end hide *)
846 854
847 Require Import ClassicalChoice. 855 Require Import ClassicalChoice.
848 Check choice. 856 Check choice.
849 (** %\vspace{-.15in}% [[ 857 (** %\vspace{-.15in}% [[
850 choice 858 choice