comparison src/Equality.v @ 398:05efde66559d

Get it working in Coq 8.4beta1; use nice coqdoc notation for italics
author Adam Chlipala <adam@chlipala.net>
date Wed, 06 Jun 2012 11:25:13 -0400
parents bef6fb896edd
children ff0aef0f33a5
comparison
equal deleted inserted replaced
397:d62ed7381a0b 398:05efde66559d
1 (* Copyright (c) 2008-2011, Adam Chlipala 1 (* Copyright (c) 2008-2012, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
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}\textit{%#<i>#definitional equality#</i>#%}%. 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 %\emph{%#<i>#the top-level structure of the recursive argument is known#</i>#%}%. 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
165 165
166 Recall that co-recursive definitions have a dual rule: a co-recursive call only simplifies when it is the discriminee of a [match]. This condition is built into the beta rule for %\index{Gallina terms!cofix}%[cofix], the anonymous form of [CoFixpoint]. 166 Recall that co-recursive definitions have a dual rule: a co-recursive call only simplifies when it is the discriminee of a [match]. This condition is built into the beta rule for %\index{Gallina terms!cofix}%[cofix], the anonymous form of [CoFixpoint].
167 167
168 %\medskip% 168 %\medskip%
169 169
170 The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a %\index{propositional equality}\textit{%#<i>#propositional equality#</i>#%}%, 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. 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.
171 171
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.#"#%''% *) 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.#"#%''% *)
173 173
174 174
175 (** * Heterogeneous Lists Revisited *) 175 (** * Heterogeneous Lists Revisited *)
324 end) with 324 end) with
325 | refl_equal => refl_equal 0 325 | refl_equal => refl_equal 0
326 end. 326 end.
327 (* end thide *) 327 (* end thide *)
328 328
329 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *) 329 (** Surprisingly, what seems at first like a _simpler_ lemma is harder to prove. *)
330 330
331 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end. 331 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
332 (* begin thide *) 332 (* begin thide *)
333 (** %\vspace{-.25in}%[[ 333 (** %\vspace{-.25in}%[[
334 simple destruct pf. 334 simple destruct pf.
379 << 379 <<
380 The term "refl_equal x'" has type "x' = x'" while it is expected to have type 380 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
381 "x = x'" 381 "x = x'"
382 >> 382 >>
383 383
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 %\textit{%#<i>#must#</i>#%}% 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 %\textit{%#<i>#must#</i>#%}% equate two non-matching terms, which makes it impossible to equate that proof with reflexivity. 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.
385 385
386 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *) 386 Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *)
387 387
388 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x. 388 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
389 intros; apply UIP_refl. 389 intros; apply UIP_refl.
390 Qed. 390 Qed.
391 391
393 (** %\vspace{-.15in}% [[ 393 (** %\vspace{-.15in}% [[
394 UIP_refl 394 UIP_refl
395 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x 395 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
396 ]] 396 ]]
397 397
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 %\textit{%#<i>#axiom#</i>#%}%. *) 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_. *)
399 399
400 Print eq_rect_eq. 400 Print eq_rect_eq.
401 (** %\vspace{-.15in}% [[ 401 (** %\vspace{-.15in}% [[
402 eq_rect_eq = 402 eq_rect_eq =
403 fun U : Type => Eq_rect_eq.eq_rect_eq U 403 fun U : Type => Eq_rect_eq.eq_rect_eq U
414 x = match h in (_ = y) return (Q y) with 414 x = match h in (_ = y) return (Q y) with
415 | eq_refl => x 415 | eq_refl => x
416 end 416 end
417 ]] 417 ]]
418 418
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 %\textit{%#<i>#inconsistent#</i>#%}% 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. 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.
420 420
421 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *) 421 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
422 422
423 Print Streicher_K. 423 Print Streicher_K.
424 (* end thide *) 424 (* end thide *)
468 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2) 468 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
469 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)" 469 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
470 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)" 470 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
471 >> 471 >>
472 472
473 This first cut at the theorem statement does not even type-check. We know that the two [fhlist] types appearing in the error message are always equal, by associativity of normal list append, but this fact is not apparent to the type checker. This stems from the fact that Coq's equality is %\index{intensional type theory}\textit{%#<i>#intensional#</i>#%}%, in the sense that type equality theorems can never be applied after the fact to get a term to type-check. Instead, we need to make use of equality explicitly in the theorem statement. *) 473 This first cut at the theorem statement does not even type-check. We know that the two [fhlist] types appearing in the error message are always equal, by associativity of normal list append, but this fact is not apparent to the type checker. This stems from the fact that Coq's equality is %\index{intensional type theory}%_intensional_, in the sense that type equality theorems can never be applied after the fact to get a term to type-check. Instead, we need to make use of equality explicitly in the theorem statement. *)
474 474
475 Theorem fhapp_ass : forall ls1 ls2 ls3 475 Theorem fhapp_ass : forall ls1 ls2 ls3
476 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3)) 476 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
477 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3), 477 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
478 fhapp hls1 (fhapp hls2 hls3) 478 fhapp hls1 (fhapp hls2 hls3)
568 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) 568 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
569 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) 569 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
570 end 570 end
571 ]] 571 ]]
572 572
573 We have made an important bit of progress, as now only a single call to [fhapp] appears in the conclusion, repeated twice. Trying case analysis on our proofs still will not work, but there is a move we can make to enable it. Not only does just one call to [fhapp] matter to us now, but it also %\textit{%#<i>#does not matter what the result of the call is#</i>#%}%. In other words, the subgoal should remain true if we replace this [fhapp] call with a fresh variable. The %\index{tactics!generalize}%[generalize] tactic helps us do exactly that. *) 573 We have made an important bit of progress, as now only a single call to [fhapp] appears in the conclusion, repeated twice. Trying case analysis on our proofs still will not work, but there is a move we can make to enable it. Not only does just one call to [fhapp] matter to us now, but it also _does not matter what the result of the call is_. In other words, the subgoal should remain true if we replace this [fhapp] call with a fresh variable. The %\index{tactics!generalize}%[generalize] tactic helps us do exactly that. *)
574 574
575 generalize (fhapp (fhapp b hls2) hls3). 575 generalize (fhapp (fhapp b hls2) hls3).
576 (** [[ 576 (** [[
577 forall f : fhlist B ((ls1 ++ ls2) ++ ls3), 577 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
578 (a0, 578 (a0,
602 end 602 end
603 ]] 603 ]]
604 604
605 To an experienced dependent types hacker, the appearance of this goal term calls for a celebration. The formula has a critical property that indicates that our problems are over. To get our proofs into the right form to apply [UIP_refl], we need to use associativity of list append to rewrite their types. We could not do that before because other parts of the goal require the proofs to retain their original types. In particular, the call to [fhapp] that we generalized must have type [(ls1 ++ ls2) ++ ls3], for some values of the list variables. If we rewrite the type of the proof used to type-cast this value to something like [ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3], then the lefthand side of the equality would no longer match the type of the term we are trying to cast. 605 To an experienced dependent types hacker, the appearance of this goal term calls for a celebration. The formula has a critical property that indicates that our problems are over. To get our proofs into the right form to apply [UIP_refl], we need to use associativity of list append to rewrite their types. We could not do that before because other parts of the goal require the proofs to retain their original types. In particular, the call to [fhapp] that we generalized must have type [(ls1 ++ ls2) ++ ls3], for some values of the list variables. If we rewrite the type of the proof used to type-cast this value to something like [ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3], then the lefthand side of the equality would no longer match the type of the term we are trying to cast.
606 606
607 However, now that we have generalized over the [fhapp] call, the type of the term being type-cast appears explicitly in the goal and %\textit{%#<i>#may be rewritten as well#</i>#%}%. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append. *) 607 However, now that we have generalized over the [fhapp] call, the type of the term being type-cast appears explicitly in the goal and _may be rewritten as well_. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append. *)
608 608
609 rewrite app_ass. 609 rewrite app_ass.
610 (** [[ 610 (** [[
611 ============================ 611 ============================
612 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3) 612 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
636 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics. The next section explores an alternative that leads to simpler developments in some cases. *) 636 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics. The next section explores an alternative that leads to simpler developments in some cases. *)
637 637
638 638
639 (** * Heterogeneous Equality *) 639 (** * Heterogeneous Equality *)
640 640
641 (** There is another equality predicate, defined in the %\index{Gallina terms!JMeq}%[JMeq] module of the standard library, implementing %\index{heterogeneous equality}\textit{%#<i>#heterogeneous equality#</i>#%}%. *) 641 (** There is another equality predicate, defined in the %\index{Gallina terms!JMeq}%[JMeq] module of the standard library, implementing %\index{heterogeneous equality}%_heterogeneous equality_. *)
642 642
643 Print JMeq. 643 Print JMeq.
644 (** %\vspace{-.15in}% [[ 644 (** %\vspace{-.15in}% [[
645 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop := 645 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
646 JMeq_refl : JMeq x x 646 JMeq_refl : JMeq x x
647 ]] 647 ]]
648 648
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. [JMeq] starts out looking a lot like [eq]. The crucial difference is that we may use [JMeq] %\textit{%#<i>#on arguments of different types#</i>#%}%. 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. *) 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. [JMeq] starts out looking a lot like [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 650
651 Infix "==" := JMeq (at level 70, no associativity). 651 Infix "==" := JMeq (at level 70, no associativity).
652 652
653 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *) 653 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
654 (* begin thide *) 654 (* begin thide *)
786 eq_ind_r 786 eq_ind_r
787 : forall (A : Type) (x : A) (P : A -> Prop), 787 : forall (A : Type) (x : A) (P : A -> Prop),
788 P x -> forall y : A, y = x -> P y 788 P x -> forall y : A, y = x -> P y
789 ]] 789 ]]
790 790
791 The corresponding lemma used for [JMeq] in the proof of [pair_cong] is %\index{Gallina terms!JMeq\_rew\_r}%[JMeq_rew_r], which, confusingly, is defined by [rewrite] as needed, so it is not available for checking until after we apply it. *) 791 The corresponding lemma used for [JMeq] in the proof of [pair_cong] is %\index{Gallina terms!internal\_JMeq\_rew\_r}%[internal_JMeq_rew_r], which, confusingly, is defined by [rewrite] as needed, so it is not available for checking until after we apply it. *)
792 792
793 Check JMeq_rew_r. 793 Check internal_JMeq_rew_r.
794 (** %\vspace{-.15in}%[[ 794 (** %\vspace{-.15in}%[[
795 JMeq_rew_r 795 internal_JMeq_rew_r
796 : forall (A : Type) (x : A) (B : Type) (b : B) 796 : forall (A : Type) (x : A) (B : Type) (b : B)
797 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x 797 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x
798 ]] 798 ]]
799 799
800 The key difference is that, where the [eq] lemma is parametrized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop]. To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y]. In contrast, to apply [JMeq_rew_r], it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and %\emph{%#<i>#its type#</i>#%}%. In other words, the predicate must be %\emph{%#<i>#polymorphic#</i>#%}% in [y]'s type; any type must make sense, from a type-checking standpoint. There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done naively leads to a type error. 800 The key difference is that, where the [eq] lemma is parametrized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop]. To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y]. In contrast, to apply [internal_JMeq_rew_r], it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and _its type_. In other words, the predicate must be _polymorphic_ in [y]'s type; any type must make sense, from a type-checking standpoint. There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done naively leads to a type error.
801 801
802 When [rewrite] cannot figure out how to apply [JMeq_rew_r] for [x == y] where [x] and [y] have the same type, the tactic can instead use an alternate theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *) 802 When [rewrite] cannot figure out how to apply [internal_JMeq_rew_r] for [x == y] where [x] and [y] have the same type, the tactic can instead use an alternate theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *)
803 803
804 Check JMeq_ind_r. 804 Check JMeq_ind_r.
805 (** %\vspace{-.15in}%[[ 805 (** %\vspace{-.15in}%[[
806 JMeq_ind_r 806 JMeq_ind_r
807 : forall (A : Type) (x : A) (P : A -> Prop), 807 : forall (A : Type) (x : A) (P : A -> Prop),
808 P x -> forall y : A, y == x -> P y 808 P x -> forall y : A, y == x -> P y
809 ]] 809 ]]
810 810
811 Ironically, where in the proof of [fhapp_ass'] we used [rewrite app_ass] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free [JMeq_rew_r]! 811 Ironically, where in the proof of [fhapp_ass'] we used [rewrite app_ass] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free [internal_JMeq_rew_r]!
812 812
813 For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *) 813 For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *)
814 814
815 Theorem out_of_luck : forall n m : nat, 815 Theorem out_of_luck : forall n m : nat,
816 n == m 816 n == m
828 (fun n0 : nat => S n0 == S m) n 828 (fun n0 : nat => S n0 == S m) n
829 ]] 829 ]]
830 *) 830 *)
831 apply JMeq_ind_r with (x := m); auto. 831 apply JMeq_ind_r with (x := m); auto.
832 832
833 (** However, we run into trouble trying to get the goal into a form compatible with [JMeq_rew_r.] *) 833 (** However, we run into trouble trying to get the goal into a form compatible with [internal_JMeq_rew_r.] *)
834 Undo 2. 834 Undo 2.
835 (** %\vspace{-.15in}%[[ 835 (** %\vspace{-.15in}%[[
836 pattern nat, n. 836 pattern nat, n.
837 ]] 837 ]]
838 << 838 <<
848 848
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]. *) 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]. *)
850 850
851 Abort. 851 Abort.
852 852
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 %\emph{%#<i>#some#</i>#%}% 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. *) 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. *)
854 854
855 855
856 (** * Equivalence of Equality Axioms *) 856 (** * Equivalence of Equality Axioms *)
857 857
858 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *) 858 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
932 932
933 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[ 933 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
934 Theorem S_eta : S = (fun n => S n). 934 Theorem S_eta : S = (fun n => S n).
935 ]] 935 ]]
936 936
937 Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be %\index{extensionality of function equality}\textit{%#<i>#extensional#</i>#%}%. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We %\textit{%#<i>#can#</i>#%}% assert function extensionality as an axiom. *) 937 Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be %\index{extensionality of function equality}%_extensional_. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We _can_ assert function extensionality as an axiom. *)
938 938
939 (* begin thide *) 939 (* begin thide *)
940 Axiom ext_eq : forall A B (f g : A -> B), 940 Axiom ext_eq : forall A B (f g : A -> B),
941 (forall x, f x = g x) 941 (forall x, f x = g x)
942 -> f = g. 942 -> f = g.
987 987
988 destruct x; constructor. 988 destruct x; constructor.
989 Qed. 989 Qed.
990 (* end thide *) 990 (* end thide *)
991 991
992 (** Unlike in the case of [eq_rect_eq], we have no way of deriving this axiom of %\index{functional extensionality}\emph{%#<i>#functional extensionality#</i>#%}% for types with decidable equality. To allow equality reasoning without axioms, it may be worth rewriting a development to replace functions with alternate representations, such as finite map types for which extensionality is derivable in CIC. *) 992 (** Unlike in the case of [eq_rect_eq], we have no way of deriving this axiom of %\index{functional extensionality}%_functional extensionality_ for types with decidable equality. To allow equality reasoning without axioms, it may be worth rewriting a development to replace functions with alternate representations, such as finite map types for which extensionality is derivable in CIC. *)