Mercurial > cpdt > repo
comparison src/Equality.v @ 294:1b6c81e51799
Fixes added while proofreading JFR camera-ready
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Thu, 09 Dec 2010 13:44:57 -0500 |
| parents | 2c88fc1dbe33 |
| children | 559ec7328410 |
comparison
equal
deleted
inserted
replaced
| 293:e2dbc0f1c1e8 | 294:1b6c81e51799 |
|---|---|
| 16 (* end hide *) | 16 (* end hide *) |
| 17 | 17 |
| 18 | 18 |
| 19 (** %\chapter{Reasoning About Equality Proofs}% *) | 19 (** %\chapter{Reasoning About Equality Proofs}% *) |
| 20 | 20 |
| 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, we will focus on design patterns for circumventing these tricky issues, and we 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 %\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 %\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. |
| 93 Qed. | 93 Qed. |
| 94 (* end thide *) | 94 (* end thide *) |
| 95 | 95 |
| 96 (** The standard [eq] relation is critically dependent on the definitional equality. [eq] is often called a %\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. | 96 (** The standard [eq] relation is critically dependent on the definitional equality. [eq] is often called a %\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. |
| 97 | 97 |
| 98 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, we will introduce effective proof methods for goals that use proofs of the standard propositional equality %``%#"#as data.#"#%''% *) | 98 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.#"#%''% *) |
| 99 | 99 |
| 100 | 100 |
| 101 (** * Heterogeneous Lists Revisited *) | 101 (** * Heterogeneous Lists Revisited *) |
| 102 | 102 |
| 103 (** 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. *) | 103 (** 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. *) |
| 480 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) | 480 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3) |
| 481 end | 481 end |
| 482 | 482 |
| 483 ]] | 483 ]] |
| 484 | 484 |
| 485 We have made an important bit of progress, as now only a single call to [fhapp] appears in the conclusion. 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 [generalize] tactic helps us do exactly that. *) | 485 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 [generalize] tactic helps us do exactly that. *) |
| 486 | 486 |
| 487 generalize (fhapp (fhapp b hls2) hls3). | 487 generalize (fhapp (fhapp b hls2) hls3). |
| 488 (** [[ | 488 (** [[ |
| 489 forall f : fhlist B ((ls1 ++ ls2) ++ ls3), | 489 forall f : fhlist B ((ls1 ++ ls2) ++ ls3), |
| 490 (a0, | 490 (a0, |