### comparison src/Equality.v @ 480:f38a3af9dd17

Batch of changes based on proofreader feedback
comparison
equal inserted replaced
479:40a9a36844d6 480:f38a3af9dd17
178 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." *) 178 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." *)
179 179
180 180
181 (** * Heterogeneous Lists Revisited *) 181 (** * Heterogeneous Lists Revisited *)
182 182
183 (** One of our example dependent data structures from the last chapter was the heterogeneous list and its 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. *) 183 (** One of our example dependent data structures from the last chapter (code repeated below) was the heterogeneous list and its 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. *)
184 184
185 Section fhlist. 185 Section fhlist.
186 Variable A : Type. 186 Variable A : Type.
187 Variable B : A -> Type. 187 Variable B : A -> Type.
188 188
418 (** %\vspace{-.15in}% [[ 418 (** %\vspace{-.15in}% [[
419 UIP_refl 419 UIP_refl
420 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x 420 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
421 ]] 421 ]]
422 422
423 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] below. *) 423 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. (Its name uses the acronym "UIP" for "unicity of identity proofs.") 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] below. *)
424 424
425 (* begin hide *) 425 (* begin hide *)
426 Import Eq_rect_eq. 426 Import Eq_rect_eq.
427 (* end hide *) 427 (* end hide *)
428 Print eq_rect_eq. 428 Print eq_rect_eq.
457 (* begin thide *) 457 (* begin thide *)
458 Definition Streicher_K' := UIP_refl__Streicher_K. 458 Definition Streicher_K' := UIP_refl__Streicher_K.
459 (* end thide *) 459 (* end thide *)
460 (* end hide *) 460 (* end hide *)
461 461
462 Print Streicher_K. 462 Check Streicher_K.
463 (* end thide *) 463 (* end thide *)
464 (** %\vspace{-.15in}% [[ 464 (** %\vspace{-.15in}% [[
465 Streicher_K = 465 Streicher_K
466 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
467 : forall (U : Type) (x : U) (P : x = x -> Prop), 466 : forall (U : Type) (x : U) (P : x = x -> Prop),
468 P (eq_refl x) -> forall p : x = x, P p 467 P eq_refl -> forall p : x = x, P p
469 ]] 468 ]]
470 469
471 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. *) 470 This is the opaquely 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. *)
472 471
473 End fhlist_map. 472 End fhlist_map.
474 473
475 (* begin hide *) 474 (* begin hide *)
476 (* begin thide *) 475 (* begin thide *)
689 (** %\vspace{-.15in}% [[ 688 (** %\vspace{-.15in}% [[
690 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop := 689 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
691 JMeq_refl : JMeq x x 690 JMeq_refl : JMeq x x
692 ]] 691 ]]
693 692
694 The identifier [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. *) 693 The identifier [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as an inside joke 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. *)
695 694
696 Infix "==" := JMeq (at level 70, no associativity). 695 Infix "==" := JMeq (at level 70, no associativity).
697 696
698 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *) 697 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
699 (* begin thide *) 698 (* begin thide *)
720 (** %\vspace{-.15in}% [[ 719 (** %\vspace{-.15in}% [[
721 JMeq_eq 720 JMeq_eq
722 : forall (A : Type) (x y : A), x == y -> x = y 721 : forall (A : Type) (x y : A), x == y -> x = y
723 ]] 722 ]]
724 723
725 It may be surprising that we cannot prove that heterogeneous equality implies normal equality. The difficulties are the same kind we have seen so far, based on limitations of [match] annotations. 724 It may be surprising that we cannot prove that heterogeneous equality implies normal equality. The difficulties are the same kind we have seen so far, based on limitations of [match] annotations. The [JMeq_eq] axiom has been proved on paper to be consistent, but asserting it may still be considered to complicate the logic we work in, so there is some motivation for avoiding it.
726 725
727 We can redo our [fhapp] associativity proof based around [JMeq]. *) 726 We can redo our [fhapp] associativity proof based around [JMeq]. *)
728 727
729 Section fhapp'. 728 Section fhapp'.
730 Variable A : Type. 729 Variable A : Type.
860 Theorem out_of_luck : forall n m : nat, 859 Theorem out_of_luck : forall n m : nat,
861 n == m 860 n == m
862 -> S n == S m. 861 -> S n == S m.
863 intros n m H. 862 intros n m H.
864 863
865 (** Applying [JMeq_ind_r] is easy, as the %\index{tactics!pattern}%[pattern] tactic will transform the goal into an application of an appropriate [fun] to a term that we want to abstract. *) 864 (** Applying [JMeq_ind_r] is easy, as the %\index{tactics!pattern}%[pattern] tactic will transform the goal into an application of an appropriate [fun] to a term that we want to abstract. (In general, [pattern] abstracts over a term by introducing a new anonymous function taking that term as argument.) *)
866 865
867 pattern n. 866 pattern n.
868 (** %\vspace{-.15in}%[[ 867 (** %\vspace{-.15in}%[[
869 n : nat 868 n : nat
870 m : nat 869 m : nat