## Mercurial > cpdt > repo

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

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Batch of changes based on proofreader feedback

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Fri, 30 Nov 2012 11:57:55 -0500 |

parents | 40a9a36844d6 |

children | 5025a401ad9e |

comparison

equal
deleted
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 |