Mercurial > cpdt > repo

comparison src/Universes.v @ 426:5f25705a10ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 18:10:26 -0400
parents 686cf945dd02
children 5744842c36a8
comparison
equal deleted inserted replaced
425:6ed5ee4845e4 426:5f25705a10ea
753 x = eq_rect p Q x p h ] 753 x = eq_rect p Q x p h ]
754 ]] 754 ]]
755 755
756 This axiom says that it is permissible to simplify pattern matches over proofs of equalities like [e = e]. The axiom is logically equivalent to some simpler corollaries. In the theorem names, %``%#"#UIP#"#%''% stands for %\index{unicity of identity proofs}``%#"#unicity of identity proofs#"#%''%, where %``%#"#identity#"#%''% is a synonym for %``%#"#equality.#"#%''% *) 756 This axiom says that it is permissible to simplify pattern matches over proofs of equalities like [e = e]. The axiom is logically equivalent to some simpler corollaries. In the theorem names, %``%#"#UIP#"#%''% stands for %\index{unicity of identity proofs}``%#"#unicity of identity proofs#"#%''%, where %``%#"#identity#"#%''% is a synonym for %``%#"#equality.#"#%''% *)
757 757
758 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x. 758 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = eq_refl x.
759 intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [ 759 intros; replace pf with (eq_rect x (eq x) (eq_refl x) x pf); [
760 symmetry; apply eq_rect_eq 760 symmetry; apply eq_rect_eq
761 | exact (match pf as pf' return match pf' in _ = y return x = y with 761 | exact (match pf as pf' return match pf' in _ = y return x = y with
762 | refl_equal => refl_equal x 762 | eq_refl => eq_refl x
763 end = pf' with 763 end = pf' with
764 | refl_equal => refl_equal _ 764 | eq_refl => eq_refl _
765 end) ]. 765 end) ].
766 Qed. 766 Qed.
767 767
768 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2. 768 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
769 intros; generalize pf1 pf2; subst; intros; 769 intros; generalize pf1 pf2; subst; intros;
873 873
874 (** One additional axiom-related wrinkle arises from an aspect of Gallina that is very different from set theory: a notion of _computational equivalence_ is central to the definition of the formal system. Axioms tend not to play well with computation. Consider this example. We start by implementing a function that uses a type equality proof to perform a safe type-cast. *) 874 (** One additional axiom-related wrinkle arises from an aspect of Gallina that is very different from set theory: a notion of _computational equivalence_ is central to the definition of the formal system. Axioms tend not to play well with computation. Consider this example. We start by implementing a function that uses a type equality proof to perform a safe type-cast. *)
875 875
876 Definition cast (x y : Set) (pf : x = y) (v : x) : y := 876 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
877 match pf with 877 match pf with
878 | refl_equal => v 878 | eq_refl => v
879 end. 879 end.
880 880
881 (** Computation over programs that use [cast] can proceed smoothly. *) 881 (** Computation over programs that use [cast] can proceed smoothly. *)
882 882
883 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12. 883 Eval compute in (cast (eq_refl (nat -> nat)) (fun n => S n)) 12.
884 (** %\vspace{-.15in}%[[ 884 (** %\vspace{-.15in}%[[
885 = 13 885 = 13
886 : nat 886 : nat
887 ]] 887 ]]
888 *) 888 *)
895 Qed. 895 Qed.
896 896
897 Eval compute in (cast t3 (fun _ => First)) 12. 897 Eval compute in (cast t3 (fun _ => First)) 12.
898 (** [[ 898 (** [[
899 = match t3 in (_ = P) return P with 899 = match t3 in (_ = P) return P with
900 | refl_equal => fun n : nat => First 900 | eq_refl => fun n : nat => First
901 end 12 901 end 12
902 : fin (12 + 1) 902 : fin (12 + 1)
903 ]] 903 ]]
904 904
905 Computation gets stuck in a pattern-match on the proof [t3]. The structure of [t3] is not known, so the match cannot proceed. It turns out a more basic problem leads to this particular situation. We ended the proof of [t3] with [Qed], so the definition of [t3] is not available to computation. That is easily fixed. *) 905 Computation gets stuck in a pattern-match on the proof [t3]. The structure of [t3] is not known, so the match cannot proceed. It turns out a more basic problem leads to this particular situation. We ended the proof of [t3] with [Qed], so the definition of [t3] is not available to computation. That is easily fixed. *)
936 (** %\vspace{-.15in}% [[ 936 (** %\vspace{-.15in}% [[
937 = First 937 = First
938 : fin (13 + 1) 938 : fin (13 + 1)
939 ]] 939 ]]
940 940
941 This simple computational reduction hides the use of a recursive function to produce a suitable [refl_equal] proof term. The recursion originates in our use of [induction] in [t4]'s proof. *) 941 This simple computational reduction hides the use of a recursive function to produce a suitable [eq_refl] proof term. The recursion originates in our use of [induction] in [t4]'s proof. *)
942 942
943 943
944 (** ** Methods for Avoiding Axioms *) 944 (** ** Methods for Avoiding Axioms *)
945 945
946 (** The last section demonstrated one reason to avoid axioms: they interfere with computational behavior of terms. A further reason is to reduce the philosophical commitment of a theorem. The more axioms one assumes, the harder it becomes to convince oneself that the formal system corresponds appropriately to one's intuitions. A refinement of this last point, in applications like %\index{proof-carrying code}%proof-carrying code%~\cite{PCC}% in computer security, has to do with minimizing the size of a%\index{trusted code base}% _trusted code base_. To convince ourselves that a theorem is true, we must convince ourselves of the correctness of the program that checks the theorem. Axioms effectively become new source code for the checking program, increasing the effort required to perform a correctness audit. 946 (** The last section demonstrated one reason to avoid axioms: they interfere with computational behavior of terms. A further reason is to reduce the philosophical commitment of a theorem. The more axioms one assumes, the harder it becomes to convince oneself that the formal system corresponds appropriately to one's intuitions. A refinement of this last point, in applications like %\index{proof-carrying code}%proof-carrying code%~\cite{PCC}% in computer security, has to do with minimizing the size of a%\index{trusted code base}% _trusted code base_. To convince ourselves that a theorem is true, we must convince ourselves of the correctness of the program that checks the theorem. Axioms effectively become new source code for the checking program, increasing the effort required to perform a correctness audit.
993 Definition finOut n (f : fin n) : match n return fin n -> Type with 993 Definition finOut n (f : fin n) : match n return fin n -> Type with
994 | O => fun _ => Empty_set 994 | O => fun _ => Empty_set
995 | _ => fun f => {f' : _ | f = Next f'} + {f = First} 995 | _ => fun f => {f' : _ | f = Next f'} + {f = First}
996 end f := 996 end f :=
997 match f with 997 match f with
998 | First _ => inright _ (refl_equal _) 998 | First _ => inright _ (eq_refl _)
999 | Next _ f' => inleft _ (exist _ f' (refl_equal _)) 999 | Next _ f' => inleft _ (exist _ f' (eq_refl _))
1000 end. 1000 end.
1001 (* end thide *) 1001 (* end thide *)
1002 1002
1003 (** As another example, consider the following type of formulas in first-order logic. The intent of the type definition will not be important in what follows, but we give a quick intuition for the curious reader. Our formulas may include [forall] quantification over arbitrary [Type]s, and we index formulas by environments telling which variables are in scope and what their types are; such an environment is a [list Type]. A constructor [Inject] lets us include any Coq [Prop] as a formula, and [VarEq] and [Lift] can be used for variable references, in what is essentially the de Bruijn index convention. (Again, the detail in this paragraph is not important to understand the discussion that follows!) *) 1003 (** As another example, consider the following type of formulas in first-order logic. The intent of the type definition will not be important in what follows, but we give a quick intuition for the curious reader. Our formulas may include [forall] quantification over arbitrary [Type]s, and we index formulas by environments telling which variables are in scope and what their types are; such an environment is a [list Type]. A constructor [Inject] lets us include any Coq [Prop] as a formula, and [VarEq] and [Lift] can be used for variable references, in what is essentially the de Bruijn index convention. (Again, the detail in this paragraph is not important to understand the discussion that follows!) *)
1004 1004
1159 | HNil => fun pf => match nth_error_nil pf with end 1159 | HNil => fun pf => match nth_error_nil pf with end
1160 | HCons t ts x values'' => 1160 | HCons t ts x values'' =>
1161 match natIndex return nth_error (t :: ts) natIndex = Some nat -> nat with 1161 match natIndex return nth_error (t :: ts) natIndex = Some nat -> nat with
1162 | O => fun pf => 1162 | O => fun pf =>
1163 match Some_inj pf in _ = T return T with 1163 match Some_inj pf in _ = T return T with
1164 | refl_equal => x 1164 | eq_refl => x
1165 end 1165 end
1166 | S natIndex' => getNat values'' natIndex' 1166 | S natIndex' => getNat values'' natIndex'
1167 end 1167 end
1168 end. 1168 end.
1169 End withTypes. 1169 End withTypes.