comparison src/Equality.v @ 427:5e6b76ca14de

Pass through Equality, to incorporate new coqdoc features
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 11:09:48 -0400
parents 5f25705a10ea
children a54a4a2ea6e4
comparison
equal deleted inserted replaced
426:5f25705a10ea 427:5e6b76ca14de
21 (** In traditional mathematics, the concept of equality is usually taken as a given. On the other hand, in type theory, equality is a very contentious subject. There are at least three different notions of equality that are important, and researchers are actively investigating new definitions of what it means for two terms to be equal. Even once we fix a notion of equality, there are inevitably tricky issues that arise in proving properties of programs that manipulate equality proofs explicitly. In this chapter, I will focus on design patterns for circumventing these tricky issues, and I will introduce the different notions of equality as they are germane. *) 21 (** In traditional mathematics, the concept of equality is usually taken as a given. On the other hand, in type theory, equality is a very contentious subject. There are at least three different notions of equality that are important, and researchers are actively investigating new definitions of what it means for two terms to be equal. Even once we fix a notion of equality, there are inevitably tricky issues that arise in proving properties of programs that manipulate equality proofs explicitly. In this chapter, I will focus on design patterns for circumventing these tricky issues, and I will introduce the different notions of equality as they are germane. *)
22 22
23 23
24 (** * The Definitional Equality *) 24 (** * The Definitional Equality *)
25 25
26 (** We have seen many examples so far where proof goals follow %``%#"#by computation.#"#%''% That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's%\index{definitional equality}% _definitional equality_. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal. 26 (** We have seen many examples so far where proof goals follow "by computation." That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's%\index{definitional equality}% _definitional equality_. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal.
27 27
28 The %\index{tactics!cbv}%[cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [0] when applied to [1]. *) 28 The %\index{tactics!cbv}%[cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [0] when applied to [1]. *)
29 29
30 Definition pred' (x : nat) := 30 Definition pred' (x : nat) :=
31 match x with 31 match x with
104 Eval compute in fun x => id' x. 104 Eval compute in fun x => id' x.
105 (** %\vspace{-.15in}%[[ 105 (** %\vspace{-.15in}%[[
106 = fun x : nat => (fix id' (n : nat) : nat := n) x 106 = fun x : nat => (fix id' (n : nat) : nat := n) x
107 ]] 107 ]]
108 108
109 By running [compute], we ask Coq to run reduction steps until no more apply, so why do we see an application of a known function, where clearly no beta reduction has been performed? The answer has to do with ensuring termination of all Gallina programs. One candidate rule would say that we apply recursive definitions wherever possible. However, this would clearly lead to nonterminating reduction sequences, since the function may appear fully applied within its own definition, and we would naively %``%#"#simplify#"#%''% such applications immediately. Instead, Coq only applies the beta rule for a recursive function when _the top-level structure of the recursive argument is known_. For [id'] above, we have only one argument [n], so clearly it is the recursive argument, and the top-level structure of [n] is known when the function is applied to [O] or to some [S e] term. The variable [x] is neither, so reduction is blocked. 109 By running [compute], we ask Coq to run reduction steps until no more apply, so why do we see an application of a known function, where clearly no beta reduction has been performed? The answer has to do with ensuring termination of all Gallina programs. One candidate rule would say that we apply recursive definitions wherever possible. However, this would clearly lead to nonterminating reduction sequences, since the function may appear fully applied within its own definition, and we would naively "simplify" such applications immediately. Instead, Coq only applies the beta rule for a recursive function when _the top-level structure of the recursive argument is known_. For [id'] above, we have only one argument [n], so clearly it is the recursive argument, and the top-level structure of [n] is known when the function is applied to [O] or to some [S e] term. The variable [x] is neither, so reduction is blocked.
110 110
111 What are recursive arguments in general? Every recursive function is compiled by Coq to a %\index{Gallina terms!fix}%[fix] expression, for anonymous definition of recursive functions. Further, every [fix] with multiple arguments has one designated as the recursive argument via a [struct] annotation. The recursive argument is the one that must decrease across recursive calls, to appease Coq's termination checker. Coq will generally infer which argument is recursive, though we may also specify it manually, if we want to tweak reduction behavior. For instance, consider this definition of a function to add two lists of [nat]s elementwise: *) 111 What are recursive arguments in general? Every recursive function is compiled by Coq to a %\index{Gallina terms!fix}%[fix] expression, for anonymous definition of recursive functions. Further, every [fix] with multiple arguments has one designated as the recursive argument via a [struct] annotation. The recursive argument is the one that must decrease across recursive calls, to appease Coq's termination checker. Coq will generally infer which argument is recursive, though we may also specify it manually, if we want to tweak reduction behavior. For instance, consider this definition of a function to add two lists of [nat]s elementwise: *)
112 112
113 Fixpoint addLists (ls1 ls2 : list nat) : list nat := 113 Fixpoint addLists (ls1 ls2 : list nat) : list nat :=
114 match ls1, ls2 with 114 match ls1, ls2 with
141 end) n1 n2 :: addLists ls1' ls2' 141 end) n1 n2 :: addLists ls1' ls2'
142 end 142 end
143 end) ls nil 143 end) ls nil
144 ]] 144 ]]
145 145
146 The outer application of the [fix] expression for [addList] was only simplified in the first case, because in the second case the recursive argument is [ls], whose top-level structure is not known. 146 The outer application of the [fix] expression for [addLists] was only simplified in the first case, because in the second case the recursive argument is [ls], whose top-level structure is not known.
147 147
148 The opposite behavior pertains to a version of [addList] with [ls2] marked as recursive. *) 148 The opposite behavior pertains to a version of [addLists] with [ls2] marked as recursive. *)
149 149
150 Fixpoint addLists' (ls1 ls2 : list nat) {struct ls2} : list nat := 150 Fixpoint addLists' (ls1 ls2 : list nat) {struct ls2} : list nat :=
151 match ls1, ls2 with 151 match ls1, ls2 with
152 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists' ls1' ls2' 152 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists' ls1' ls2'
153 | _, _ => nil 153 | _, _ => nil
154 end. 154 end.
155
156 (* begin hide *)
157 Definition foo := @eq.
158 (* end hide *)
155 159
156 Eval compute in fun ls => addLists' ls nil. 160 Eval compute in fun ls => addLists' ls nil.
157 (** %\vspace{-.15in}%[[ 161 (** %\vspace{-.15in}%[[
158 = fun ls : list nat => match ls with 162 = fun ls : list nat => match ls with
159 | nil => nil 163 | nil => nil
167 171
168 %\medskip% 172 %\medskip%
169 173
170 The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a%\index{propositional equality}% _propositional equality_, because it reifies definitional equality as a proposition that may or may not hold. Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity. In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina. We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use. 174 The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a%\index{propositional equality}% _propositional equality_, because it reifies definitional equality as a proposition that may or may not hold. Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity. In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina. We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use.
171 175
172 This all may make it sound like the choice of [eq]'s definition is unimportant. To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs. Before that point, I will introduce proof methods for goals that use proofs of the standard propositional equality %``%#"#as data.#"#%''% *) 176 This all may make it sound like the choice of [eq]'s definition is unimportant. To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs. Before that point, I will introduce proof methods for goals that use proofs of the standard propositional equality "as data." *)
173 177
174 178
175 (** * Heterogeneous Lists Revisited *) 179 (** * Heterogeneous Lists Revisited *)
176 180
177 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated %``%#"#cursor#"#%''% type. The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [member] types. *) 181 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [fmember] types. *)
178 182
179 Section fhlist. 183 Section fhlist.
180 Variable A : Type. 184 Variable A : Type.
181 Variable B : A -> Type. 185 Variable B : A -> Type.
182 186
207 end. 211 end.
208 End fhlist. 212 End fhlist.
209 213
210 Implicit Arguments fhget [A B elm ls]. 214 Implicit Arguments fhget [A B elm ls].
211 215
216 (* begin hide *)
217 Definition map := O.
218 (* end hide *)
219
212 (** We can define a [map]-like function for [fhlist]s. *) 220 (** We can define a [map]-like function for [fhlist]s. *)
213 221
214 Section fhlist_map. 222 Section fhlist_map.
215 Variables A : Type. 223 Variables A : Type.
216 Variables B C : A -> Type. 224 Variables B C : A -> Type.
221 | nil => fun _ => tt 229 | nil => fun _ => tt
222 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls)) 230 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
223 end. 231 end.
224 232
225 Implicit Arguments fhmap [ls]. 233 Implicit Arguments fhmap [ls].
234
235 (* begin hide *)
236 Definition ilist := O.
237 Definition get := O.
238 Definition imap := O.
239 (* end hide *)
226 240
227 (** For the inductive versions of the [ilist] definitions, we proved a lemma about the interaction of [get] and [imap]. It was a strategic choice not to attempt such a proof for the definitions that we just gave, because that sets us on a collision course with the problems that are the subject of this chapter. *) 241 (** For the inductive versions of the [ilist] definitions, we proved a lemma about the interaction of [get] and [imap]. It was a strategic choice not to attempt such a proof for the definitions that we just gave, because that sets us on a collision course with the problems that are the subject of this chapter. *)
228 242
229 Variable elm : A. 243 Variable elm : A.
230 244
269 while it is expected to have type "a = elm" 283 while it is expected to have type "a = elm"
270 >> 284 >>
271 285
272 In retrospect, the problem is not so hard to see. Reflexivity proofs only show [x = x] for particular values of [x], whereas here we are thinking in terms of a proof of [a = elm], where the two sides of the equality are not equal syntactically. Thus, the essential lemma we need does not even type-check! 286 In retrospect, the problem is not so hard to see. Reflexivity proofs only show [x = x] for particular values of [x], whereas here we are thinking in terms of a proof of [a = elm], where the two sides of the equality are not equal syntactically. Thus, the essential lemma we need does not even type-check!
273 287
274 Is it time to throw in the towel? Luckily, the answer is %``%#"#no.#"#%''% In this chapter, we will see several useful patterns for proving obligations like this. 288 Is it time to throw in the towel? Luckily, the answer is "no." In this chapter, we will see several useful patterns for proving obligations like this.
275 289
276 For this particular example, the solution is surprisingly straightforward. The [destruct] tactic has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments. 290 For this particular example, the solution is surprisingly straightforward. The [destruct] tactic has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments.
277 [[ 291 [[
278 case a0. 292 case a0.
279 293
352 end. 366 end.
353 (* end thide *) 367 (* end thide *)
354 368
355 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *) 369 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
356 370
371 (* begin hide *)
372 Definition lemma3' := O.
373 (* end hide *)
374
357 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x. 375 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
358 (* begin thide *) 376 (* begin thide *)
359 (** %\vspace{-.25in}%[[ 377 (** %\vspace{-.25in}%[[
360 simple destruct pf. 378 simple destruct pf.
361 ]] 379 ]]
379 << 397 <<
380 The term "eq_refl x'" has type "x' = x'" while it is expected to have type 398 The term "eq_refl x'" has type "x' = x'" while it is expected to have type
381 "x = x'" 399 "x = x'"
382 >> 400 >>
383 401
384 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], referring to the [in]-bound variable [x']. To do a dependent [match], we _must_ choose a fresh name for the second argument of [eq]. We are just as constrained to use the %``%#"#real#"#%''% value [x] for the first argument. Thus, within the [return] clause, the proof we are matching on _must_ equate two non-matching terms, which makes it impossible to equate that proof with reflexivity. 402 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], referring to the [in]-bound variable [x']. To do a dependent [match], we _must_ choose a fresh name for the second argument of [eq]. We are just as constrained to use the "real" value [x] for the first argument. Thus, within the [return] clause, the proof we are matching on _must_ equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
385 403
386 Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *) 404 Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *)
387 405
388 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x. 406 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
389 intros; apply UIP_refl. 407 intros; apply UIP_refl.
393 (** %\vspace{-.15in}% [[ 411 (** %\vspace{-.15in}% [[
394 UIP_refl 412 UIP_refl
395 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x 413 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
396 ]] 414 ]]
397 415
398 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an _axiom_. *) 416 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an _axiom_, the term [Eq_rect_eq.eq_rect_eq] below. *)
417
418 (* begin hide *)
419 Definition ere := eq_rect_eq.
420 (* end hide *)
399 421
400 Print eq_rect_eq. 422 Print eq_rect_eq.
401 (** %\vspace{-.15in}% [[ 423 (** %\vspace{-.15in}% [[
402 eq_rect_eq = 424 eq_rect_eq =
403 fun U : Type => Eq_rect_eq.eq_rect_eq U 425 fun U : Type => Eq_rect_eq.eq_rect_eq U
404 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), 426 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
405 x = eq_rect p Q x p h 427 x = eq_rect p Q x p h
406 ]] 428 ]]
407 429
408 The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a %``%#"#fact#"#%''% that seems like common sense, once the notation is deciphered. The term [eq_rect] is the automatically generated recursion principle for [eq]. Calling [eq_rect] is another way of [match]ing on an equality proof. The proof we match on is the argument [h], and [x] is the body of the [match]. The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed. We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *) 430 The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. The term [eq_rect] is the automatically generated recursion principle for [eq]. Calling [eq_rect] is another way of [match]ing on an equality proof. The proof we match on is the argument [h], and [x] is the body of the [match]. The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed. We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *)
431
432 (* begin hide *)
433 Definition False' := False.
434 (* end hide *)
409 435
410 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), 436 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
411 x = eq_rect p Q x p h). 437 x = eq_rect p Q x p h).
412 (** %\vspace{-.15in}%[[ 438 (** %\vspace{-.15in}%[[
413 = forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), 439 = forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
414 x = match h in (_ = y) return (Q y) with 440 x = match h in (_ = y) return (Q y) with
415 | eq_refl => x 441 | eq_refl => x
416 end 442 end
417 ]] 443 ]]
418 444
419 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an %\index{axioms}%axiom; that is, a proposition asserted as true without proof. We cannot assert just any statement without proof. Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant. In general, we need to be sure that we never assert _inconsistent_ sets of axioms. A set of axioms is inconsistent if its conjunction implies [False]. For the case of [eq_rect_eq], consistency has been verified outside of Coq via %``%#"#informal#"#%''% metatheory%~\cite{AxiomK}%, in a study that also established unprovability of the axiom in CIC. 445 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an %\index{axioms}%axiom; that is, a proposition asserted as true without proof. We cannot assert just any statement without proof. Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant. In general, we need to be sure that we never assert _inconsistent_ sets of axioms. A set of axioms is inconsistent if its conjunction implies [False]. For the case of [eq_rect_eq], consistency has been verified outside of Coq via "informal" metatheory%~\cite{AxiomK}%, in a study that also established unprovability of the axiom in CIC.
420 446
421 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *) 447 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
448
449 (* begin hide *)
450 Definition Streicher_K' := (Streicher_K, UIP_refl__Streicher_K).
451 (* end hide *)
422 452
423 Print Streicher_K. 453 Print Streicher_K.
424 (* end thide *) 454 (* end thide *)
425 (** %\vspace{-.15in}% [[ 455 (** %\vspace{-.15in}% [[
426 Streicher_K = 456 Streicher_K =
427 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U) 457 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
428 : forall (U : Type) (x : U) (P : x = x -> Prop), 458 : forall (U : Type) (x : U) (P : x = x -> Prop),
429 P (eq_refl x) -> forall p : x = x, P p 459 P (eq_refl x) -> forall p : x = x, P p
430 ]] 460 ]]
431 461
432 This is the unfortunately named %\index{axiom K}``%#"#Streicher's axiom K,#"#%''% which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *) 462 This is the unfortunately named %\index{axiom K}%"Streicher's axiom K," which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
433 463
434 End fhlist_map. 464 End fhlist_map.
435 465
436 (** It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality. The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases. To simplify presentation, we will stick with the axiom version in the rest of this chapter. *) 466 (** It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality. The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases. To simplify presentation, we will stick with the axiom version in the rest of this chapter. *)
437 467
644 (** %\vspace{-.15in}% [[ 674 (** %\vspace{-.15in}% [[
645 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop := 675 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
646 JMeq_refl : JMeq x x 676 JMeq_refl : JMeq x x
647 ]] 677 ]]
648 678
649 The identity [JMeq] stands for %\index{John Major equality}``%#"#John Major equality,#"#%''% a name coined by Conor McBride%~\cite{JMeq}% as a sort of pun about British politics. The definition [JMeq] starts out looking a lot like the definition of [eq]. The crucial difference is that we may use [JMeq] _on arguments of different types_. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *) 679 The identity [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as a sort of pun about British politics. The definition [JMeq] starts out looking a lot like the definition of [eq]. The crucial difference is that we may use [JMeq] _on arguments of different types_. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *)
650 680
651 Infix "==" := JMeq (at level 70, no associativity). 681 Infix "==" := JMeq (at level 70, no associativity).
652 682
653 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *) 683 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
654 (* begin thide *) 684 (* begin thide *)
829 ]] 859 ]]
830 *) 860 *)
831 apply JMeq_ind_r with (x := m); auto. 861 apply JMeq_ind_r with (x := m); auto.
832 862
833 (** However, we run into trouble trying to get the goal into a form compatible with [internal_JMeq_rew_r.] *) 863 (** However, we run into trouble trying to get the goal into a form compatible with [internal_JMeq_rew_r.] *)
864
834 Undo 2. 865 Undo 2.
835 (** %\vspace{-.15in}%[[ 866 (** %\vspace{-.15in}%[[
836 pattern nat, n. 867 pattern nat, n.
837 ]] 868 ]]
838 << 869 <<
848 879
849 In other words, the successor function [S] is insufficiently polymorphic. If we try to generalize over the type of [n], we find that [S] is no longer legal to apply to [n]. *) 880 In other words, the successor function [S] is insufficiently polymorphic. If we try to generalize over the type of [n], we find that [S] is no longer legal to apply to [n]. *)
850 881
851 Abort. 882 Abort.
852 883
853 (** Why did we not run into this problem in our proof of [fhapp_ass'']? The reason is that the pair constructor is polymorphic in the types of the pair components, while functions like [S] are not polymorphic at all. Use of such non-polymorphic functions with [JMeq] tends to push toward use of axioms. The example with [nat] here is a bit unrealistic; more likely cases would involve functions that have _some_ polymorphism, but not enough to allow abstractions of the sort we attempted above with [pattern]. For instance, we might have an equality between two lists, where the goal only type-checks when the terms involved really are lists, though everything is polymorphic in the types of list data elements. The #<a href="http://www.mpi-sws.org/~gil/Heq/">#Heq%\footnote{\url{http://www.mpi-sws.org/~gil/Heq/}}%#</a># library builds up a slightly different foundation to help avoid such problems. *) 884 (** Why did we not run into this problem in our proof of [fhapp_ass'']? The reason is that the pair constructor is polymorphic in the types of the pair components, while functions like [S] are not polymorphic at all. Use of such non-polymorphic functions with [JMeq] tends to push toward use of axioms. The example with [nat] here is a bit unrealistic; more likely cases would involve functions that have _some_ polymorphism, but not enough to allow abstractions of the sort we attempted above with [pattern]. For instance, we might have an equality between two lists, where the goal only type-checks when the terms involved really are lists, though everything is polymorphic in the types of list data elements. The {{http://www.mpi-sws.org/~gil/Heq/}Heq} library builds up a slightly different foundation to help avoid such problems. *)
854 885
855 886
856 (** * Equivalence of Equality Axioms *) 887 (** * Equivalence of Equality Axioms *)
857 888
858 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *) 889 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
871 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop := 902 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
872 exists pf : B = A, x = match pf with eq_refl => y end. 903 exists pf : B = A, x = match pf with eq_refl => y end.
873 904
874 Infix "===" := JMeq' (at level 70, no associativity). 905 Infix "===" := JMeq' (at level 70, no associativity).
875 906
907 (** remove printing exists *)
908
876 (** We say that, by definition, [x] and [y] are equal if and only if there exists a proof [pf] that their types are equal, such that [x] equals the result of casting [y] with [pf]. This statement can look strange from the standpoint of classical math, where we almost never mention proofs explicitly with quantifiers in formulas, but it is perfectly legal Coq code. 909 (** We say that, by definition, [x] and [y] are equal if and only if there exists a proof [pf] that their types are equal, such that [x] equals the result of casting [y] with [pf]. This statement can look strange from the standpoint of classical math, where we almost never mention proofs explicitly with quantifiers in formulas, but it is perfectly legal Coq code.
877 910
878 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *) 911 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
879 912
880 (** remove printing exists *)
881 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x. 913 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
882 intros; unfold JMeq'; exists (eq_refl A); reflexivity. 914 intros; unfold JMeq'; exists (eq_refl A); reflexivity.
883 Qed. 915 Qed.
884 916
885 (** printing exists $\exists$ *) 917 (** printing exists $\exists$ *)
921 *) 953 *)
922 954
923 rewrite (UIP_refl _ _ x0); reflexivity. 955 rewrite (UIP_refl _ _ x0); reflexivity.
924 Qed. 956 Qed.
925 957
926 (** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs. One style may be more convenient than the other for some proofs, but we can always interconvert between our results. The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those %``%#"#simple#"#%''% proofs. On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements. *) 958 (** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs. One style may be more convenient than the other for some proofs, but we can always interconvert between our results. The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those "simple" proofs. On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements. *)
927 959
928 (* end thide *) 960 (* end thide *)
929 961
930 962
931 (** * Equality of Functions *) 963 (** * Equality of Functions *)
950 (* begin thide *) 982 (* begin thide *)
951 apply functional_extensionality; crush. 983 apply functional_extensionality; crush.
952 Qed. 984 Qed.
953 (* end thide *) 985 (* end thide *)
954 986
955 (** The same axiom can help us prove equality of types, where we need to %``%#"#reason under quantifiers.#"#%''% *) 987 (** The same axiom can help us prove equality of types, where we need to "reason under quantifiers." *)
956 988
957 Theorem forall_eq : (forall x : nat, match x with 989 Theorem forall_eq : (forall x : nat, match x with
958 | O => True 990 | O => True
959 | S _ => True 991 | S _ => True
960 end) 992 end)