Mercurial > cpdt > repo

annotate src/Equality.v @ 118:ee676bf3d681

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Up to Streicher
author Adam Chlipala <adamc@hcoop.net>
date Sat, 18 Oct 2008 12:04:28 -0400
parents
children 8df59f0b3dc0
rev   line source
adamc@118 1 (* Copyright (c) 2008, Adam Chlipala
adamc@118 2 *
adamc@118 3 * This work is licensed under a
adamc@118 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@118 5 * Unported License.
adamc@118 6 * The license text is available at:
adamc@118 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@118 8 *)
adamc@118 9
adamc@118 10 (* begin hide *)
adamc@118 11 Require Import Eqdep List.
adamc@118 12
adamc@118 13 Require Import Tactics.
adamc@118 14
adamc@118 15 Set Implicit Arguments.
adamc@118 16 (* end hide *)
adamc@118 17
adamc@118 18
adamc@118 19 (** %\chapter{Reasoning About Equality Proofs}% *)
adamc@118 20
adamc@118 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. *)
adamc@118 22
adamc@118 23
adamc@118 24 (** * Heterogeneous Lists Revisited *)
adamc@118 25
adamc@118 26 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. *)
adamc@118 27
adamc@118 28 Section fhlist.
adamc@118 29 Variable A : Type.
adamc@118 30 Variable B : A -> Type.
adamc@118 31
adamc@118 32 Fixpoint fhlist (ls : list A) : Type :=
adamc@118 33 match ls with
adamc@118 34 | nil => unit
adamc@118 35 | x :: ls' => B x * fhlist ls'
adamc@118 36 end%type.
adamc@118 37
adamc@118 38 Variable elm : A.
adamc@118 39
adamc@118 40 Fixpoint fmember (ls : list A) : Type :=
adamc@118 41 match ls with
adamc@118 42 | nil => Empty_set
adamc@118 43 | x :: ls' => (x = elm) + fmember ls'
adamc@118 44 end%type.
adamc@118 45
adamc@118 46 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@118 47 match ls return fhlist ls -> fmember ls -> B elm with
adamc@118 48 | nil => fun _ idx => match idx with end
adamc@118 49 | _ :: ls' => fun mls idx =>
adamc@118 50 match idx with
adamc@118 51 | inl pf => match pf with
adamc@118 52 | refl_equal => fst mls
adamc@118 53 end
adamc@118 54 | inr idx' => fhget ls' (snd mls) idx'
adamc@118 55 end
adamc@118 56 end.
adamc@118 57 End fhlist.
adamc@118 58
adamc@118 59 Implicit Arguments fhget [A B elm ls].
adamc@118 60
adamc@118 61 (** We can define a [map]-like function for [fhlist]s. *)
adamc@118 62
adamc@118 63 Section fhlist_map.
adamc@118 64 Variables A : Type.
adamc@118 65 Variables B C : A -> Type.
adamc@118 66 Variable f : forall x, B x -> C x.
adamc@118 67
adamc@118 68 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
adamc@118 69 match ls return fhlist B ls -> fhlist C ls with
adamc@118 70 | nil => fun _ => tt
adamc@118 71 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
adamc@118 72 end.
adamc@118 73
adamc@118 74 Implicit Arguments fhmap [ls].
adamc@118 75
adamc@118 76 (** 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. *)
adamc@118 77
adamc@118 78 Variable elm : A.
adamc@118 79
adamc@118 80 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
adamc@118 81 fhget (fhmap hls) mem = f (fhget hls mem).
adamc@118 82 induction ls; crush.
adamc@118 83
adamc@118 84 (** Part of our single remaining subgoal is:
adamc@118 85
adamc@118 86 [[
adamc@118 87
adamc@118 88 a0 : a = elm
adamc@118 89 ============================
adamc@118 90 match a0 in (_ = a2) return (C a2) with
adamc@118 91 | refl_equal => f a1
adamc@118 92 end = f match a0 in (_ = a2) return (B a2) with
adamc@118 93 | refl_equal => a1
adamc@118 94 end
adamc@118 95 ]]
adamc@118 96
adamc@118 97 This seems like a trivial enough obligation. The equality proof [a0] must be [refl_equal], since that is the only constructor of [eq]. Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
adamc@118 98
adamc@118 99 [[
adamc@118 100
adamc@118 101 destruct a0.
adamc@118 102
adamc@118 103 [[
adamc@118 104 User error: Cannot solve a second-order unification problem
adamc@118 105 ]]
adamc@118 106
adamc@118 107 This is one of Coq's standard error messages for informing us that its heuristics for attempting an instance of an undecidable problem about dependent typing have failed. We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
adamc@118 108
adamc@118 109 [[
adamc@118 110
adamc@118 111 assert (a0 = refl_equal _).
adamc@118 112
adamc@118 113 [[
adamc@118 114 The term "refl_equal ?98" has type "?98 = ?98"
adamc@118 115 while it is expected to have type "a = elm"
adamc@118 116 ]]
adamc@118 117
adamc@118 118 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!
adamc@118 119
adamc@118 120 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.
adamc@118 121
adamc@118 122 For this particular example, the solution is surprisingly straightforward. [destruct] has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments. *)
adamc@118 123
adamc@118 124 case a0.
adamc@118 125 (** [[
adamc@118 126
adamc@118 127 ============================
adamc@118 128 f a1 = f a1
adamc@118 129 ]]
adamc@118 130
adamc@118 131 It seems that [destruct] was trying to be too smart for its own good. *)
adamc@118 132
adamc@118 133 reflexivity.
adamc@118 134 Qed.
adamc@118 135
adamc@118 136 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *)
adamc@118 137
adamc@118 138 Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
adamc@118 139 simple destruct pf; reflexivity.
adamc@118 140 Qed.
adamc@118 141
adamc@118 142 (** [simple destruct pf] is a convenient form for applying [case]. It runs [intro] to bring into scope all quantified variables up to its argument. *)
adamc@118 143
adamc@118 144 Print lemma1.
adamc@118 145
adamc@118 146 (** [[
adamc@118 147
adamc@118 148 lemma1 =
adamc@118 149 fun (x : A) (pf : x = elm) =>
adamc@118 150 match pf as e in (_ = y) return (0 = match e with
adamc@118 151 | refl_equal => 0
adamc@118 152 end) with
adamc@118 153 | refl_equal => refl_equal 0
adamc@118 154 end
adamc@118 155 : forall (x : A) (pf : x = elm), 0 = match pf with
adamc@118 156 | refl_equal => 0
adamc@118 157 end
adamc@118 158 ]]
adamc@118 159
adamc@118 160 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
adamc@118 161
adamc@118 162 Definition lemma1' :=
adamc@118 163 fun (x : A) (pf : x = elm) =>
adamc@118 164 match pf return (0 = match pf with
adamc@118 165 | refl_equal => 0
adamc@118 166 end) with
adamc@118 167 | refl_equal => refl_equal 0
adamc@118 168 end.
adamc@118 169
adamc@118 170 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)
adamc@118 171
adamc@118 172 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
adamc@118 173 (** [[
adamc@118 174
adamc@118 175 simple destruct pf.
adamc@118 176
adamc@118 177 [[
adamc@118 178
adamc@118 179 User error: Cannot solve a second-order unification problem
adamc@118 180 ]] *)
adamc@118 181 Abort.
adamc@118 182
adamc@118 183 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
adamc@118 184
adamc@118 185 Definition lemma2' :=
adamc@118 186 fun (x : A) (pf : x = x) =>
adamc@118 187 match pf return (0 = match pf with
adamc@118 188 | refl_equal => 0
adamc@118 189 end) with
adamc@118 190 | refl_equal => refl_equal 0
adamc@118 191 end.
adamc@118 192
adamc@118 193 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
adamc@118 194
adamc@118 195 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@118 196 (** [[
adamc@118 197
adamc@118 198 simple destruct pf.
adamc@118 199
adamc@118 200 [[
adamc@118 201
adamc@118 202 User error: Cannot solve a second-order unification problem
adamc@118 203 ]] *)
adamc@118 204 Abort.
adamc@118 205
adamc@118 206 (** This time, even our manual attempt fails.
adamc@118 207
adamc@118 208 [[
adamc@118 209
adamc@118 210 Definition lemma3' :=
adamc@118 211 fun (x : A) (pf : x = x) =>
adamc@118 212 match pf as pf' in (_ = x') return (pf' = refl_equal x') with
adamc@118 213 | refl_equal => refl_equal _
adamc@118 214 end.
adamc@118 215
adamc@118 216 [[
adamc@118 217
adamc@118 218 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
adamc@118 219 "x = x'"
adamc@118 220 ]]
adamc@118 221
adamc@118 222 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], refering 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.
adamc@118 223
adamc@118 224 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)
adamc@118 225
adamc@118 226 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@118 227 intros; apply UIP_refl.
adamc@118 228 Qed.
adamc@118 229
adamc@118 230 Check UIP_refl.
adamc@118 231 (** [[
adamc@118 232
adamc@118 233 UIP_refl
adamc@118 234 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
adamc@118 235 ]]
adamc@118 236
adamc@118 237 [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>#%}%. *)
adamc@118 238
adamc@118 239 Print eq_rect_eq.
adamc@118 240 (** [[
adamc@118 241
adamc@118 242 eq_rect_eq =
adamc@118 243 fun U : Type => Eq_rect_eq.eq_rect_eq U
adamc@118 244 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@118 245 x = eq_rect p Q x p h
adamc@118 246 ]]
adamc@118 247
adamc@118 248 [eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. [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]. [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed.
adamc@118 249
adamc@118 250 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an 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.
adamc@118 251
adamc@118 252 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
adamc@118 253
adamc@118 254 Print Streicher_K.
adamc@118 255 (** [[
adamc@118 256
adamc@118 257 Streicher_K =
adamc@118 258 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
adamc@118 259 : forall (U : Type) (x : U) (P : x = x -> Prop),
adamc@118 260 P (refl_equal x) -> forall p : x = x, P p
adamc@118 261 ]]
adamc@118 262
adamc@118 263 This is the unfortunately-named "Streicher's axiom K," which says that a predicate on properly-typed equality proofs holds of all such proofs if it holds of reflexivity. *)
adamc@118 264
adamc@118 265 End fhlist_map.
adamc@118 266