Mercurial > cpdt > repo

annotate src/Equality.v @ 121:61e5622b1195

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Interconvertibility
author Adam Chlipala <adamc@hcoop.net>
date Sat, 18 Oct 2008 14:55:52 -0400
parents 39c7894b3f7f
children 7cbf0376702f
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@120 11 Require Import Eqdep JMeq 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
adamc@119 267
adamc@119 268 (** * Type-Casts in Theorem Statements *)
adamc@119 269
adamc@119 270 (** Sometimes we need to use tricks with equality just to state the theorems that we care about. To illustrate, we start by defining a concatenation function for [fhlist]s. *)
adamc@119 271
adamc@119 272 Section fhapp.
adamc@119 273 Variable A : Type.
adamc@119 274 Variable B : A -> Type.
adamc@119 275
adamc@119 276 Fixpoint fhapp (ls1 ls2 : list A) {struct ls1}
adamc@119 277 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
adamc@119 278 match ls1 return fhlist _ ls1 -> _ -> fhlist _ (ls1 ++ ls2) with
adamc@119 279 | nil => fun _ hls2 => hls2
adamc@119 280 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
adamc@119 281 end.
adamc@119 282
adamc@119 283 Implicit Arguments fhapp [ls1 ls2].
adamc@119 284
adamc@119 285 (** We might like to prove that [fhapp] is associative.
adamc@119 286
adamc@119 287 [[
adamc@119 288
adamc@119 289 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 290 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 291 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
adamc@119 292
adamc@119 293 [[
adamc@119 294
adamc@119 295 The term
adamc@119 296 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
adamc@119 297 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
adamc@119 298 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
adamc@119 299 ]]
adamc@119 300
adamc@119 301 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 %\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. *)
adamc@119 302
adamc@119 303 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 304 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
adamc@119 305 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 306 fhapp hls1 (fhapp hls2 hls3)
adamc@119 307 = match pf in (_ = ls) return fhlist _ ls with
adamc@119 308 | refl_equal => fhapp (fhapp hls1 hls2) hls3
adamc@119 309 end.
adamc@119 310 induction ls1; crush.
adamc@119 311
adamc@119 312 (** The first remaining subgoal looks trivial enough:
adamc@119 313
adamc@119 314 [[
adamc@119 315
adamc@119 316 ============================
adamc@119 317 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 318 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 319 | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 320 end
adamc@119 321 ]]
adamc@119 322
adamc@119 323 We can try what worked in previous examples.
adamc@119 324
adamc@119 325 [[
adamc@119 326 case pf.
adamc@119 327
adamc@119 328 [[
adamc@119 329
adamc@119 330 User error: Cannot solve a second-order unification problem
adamc@119 331 ]]
adamc@119 332
adamc@119 333 It seems we have reached another case where it is unclear how to use a dependent [match] to implement case analysis on our proof. The [UIP_refl] theorem can come to our rescue again. *)
adamc@119 334
adamc@119 335 rewrite (UIP_refl _ _ pf).
adamc@119 336 (** [[
adamc@119 337
adamc@119 338 ============================
adamc@119 339 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 340 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 341 ]] *)
adamc@119 342
adamc@119 343 reflexivity.
adamc@119 344
adamc@119 345 (** Our second subgoal is trickier.
adamc@119 346
adamc@119 347 [[
adamc@119 348
adamc@119 349 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 350 ============================
adamc@119 351 (a0,
adamc@119 352 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 353 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 354 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 355 | refl_equal =>
adamc@119 356 (a0,
adamc@119 357 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 358 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 359 end
adamc@119 360 ]]
adamc@119 361
adamc@119 362
adamc@119 363 [[
adamc@119 364
adamc@119 365 rewrite (UIP_refl _ _ pf).
adamc@119 366
adamc@119 367 [[
adamc@119 368 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
adamc@119 369 while it is expected to have type "?556 = ?556"
adamc@119 370 ]]
adamc@119 371
adamc@119 372 We can only apply [UIP_refl] on proofs of equality with syntactically equal operands, which is not the case of [pf] here. We will need to manipulate the form of this subgoal to get us to a point where we may use [UIP_refl]. A first step is obtaining a proof suitable to use in applying the induction hypothesis. Inversion on the structure of [pf] is sufficient for that. *)
adamc@119 373
adamc@119 374 injection pf; intro pf'.
adamc@119 375 (** [[
adamc@119 376
adamc@119 377 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 378 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
adamc@119 379 ============================
adamc@119 380 (a0,
adamc@119 381 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 382 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 383 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 384 | refl_equal =>
adamc@119 385 (a0,
adamc@119 386 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 387 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 388 end
adamc@119 389 ]]
adamc@119 390
adamc@119 391 Now we can rewrite using the inductive hypothesis. *)
adamc@119 392
adamc@119 393 rewrite (IHls1 _ _ pf').
adamc@119 394 (** [[
adamc@119 395
adamc@119 396 ============================
adamc@119 397 (a0,
adamc@119 398 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 399 | refl_equal =>
adamc@119 400 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 401 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
adamc@119 402 end) =
adamc@119 403 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 404 | refl_equal =>
adamc@119 405 (a0,
adamc@119 406 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 407 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 408 end
adamc@119 409 ]]
adamc@119 410
adamc@119 411 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. *)
adamc@119 412
adamc@119 413 generalize (fhapp (fhapp b hls2) hls3).
adamc@119 414 (** [[
adamc@119 415
adamc@119 416 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
adamc@119 417 (a0,
adamc@119 418 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 419 | refl_equal => f
adamc@119 420 end) =
adamc@119 421 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 422 | refl_equal => (a0, f)
adamc@119 423 end
adamc@119 424 ]]
adamc@119 425
adamc@119 426 The conclusion has gotten markedly simpler. It seems counterintuitive that we can have an easier time of proving a more general theorem, but that is exactly the case here and for many other proofs that use dependent types heavily. Speaking informally, the reason why this kind of activity helps is that [match] annotations only support variables in certain positions. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood.
adamc@119 427
adamc@119 428 In this case, it is helpful to generalize over our two proofs as well. *)
adamc@119 429
adamc@119 430 generalize pf pf'.
adamc@119 431 (** [[
adamc@119 432
adamc@119 433 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 434 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 435 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
adamc@119 436 (a0,
adamc@119 437 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 438 | refl_equal => f
adamc@119 439 end) =
adamc@119 440 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 441 | refl_equal => (a0, f)
adamc@119 442 end
adamc@119 443 ]]
adamc@119 444
adamc@119 445 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.
adamc@119 446
adamc@119 447 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. *)
adamc@119 448
adamc@119 449 rewrite app_ass.
adamc@119 450 (** [[
adamc@119 451
adamc@119 452 ============================
adamc@119 453 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 454 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 455 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
adamc@119 456 (a0,
adamc@119 457 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 458 | refl_equal => f
adamc@119 459 end) =
adamc@119 460 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 461 | refl_equal => (a0, f)
adamc@119 462 end
adamc@119 463 ]]
adamc@119 464
adamc@119 465 We can see that we have achieved the crucial property: the type of each generalized equality proof has syntactically equal operands. This makes it easy to finish the proof with [UIP_refl]. *)
adamc@119 466
adamc@119 467 intros.
adamc@119 468 rewrite (UIP_refl _ _ pf0).
adamc@119 469 rewrite (UIP_refl _ _ pf'0).
adamc@119 470 reflexivity.
adamc@119 471 Qed.
adamc@119 472 End fhapp.
adamc@120 473
adamc@120 474 Implicit Arguments fhapp [A B ls1 ls2].
adamc@120 475
adamc@120 476
adamc@120 477 (** * Heterogeneous Equality *)
adamc@120 478
adamc@120 479 (** There is another equality predicate, defined in the [JMeq] module of the standard library, implementing %\textit{%#<i>#heterogeneous equality#</i>#%}%. *)
adamc@120 480
adamc@120 481 Print JMeq.
adamc@120 482 (** [[
adamc@120 483
adamc@120 484 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
adamc@120 485 JMeq_refl : JMeq x x
adamc@120 486 ]]
adamc@120 487
adamc@120 488 [JMeq] stands for "John Major equality," a name coined by Conor McBride 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. *)
adamc@120 489
adamc@120 490 Infix "==" := JMeq (at level 70, no associativity).
adamc@120 491
adamc@121 492 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
adamc@120 493 match pf return (pf == refl_equal _) with
adamc@120 494 | refl_equal => JMeq_refl _
adamc@120 495 end.
adamc@120 496
adamc@120 497 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
adamc@120 498
adamc@121 499 Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *)
adamc@120 500
adamc@120 501 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
adamc@120 502 O = match pf with refl_equal => O end.
adamc@121 503 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@120 504 Qed.
adamc@120 505
adamc@120 506 (** All in all, refreshingly straightforward, but there really is no such thing as a free lunch. The use of [rewrite] is implemented in terms of an axiom: *)
adamc@120 507
adamc@120 508 Check JMeq_eq.
adamc@120 509 (** [[
adamc@120 510
adamc@120 511 JMeq_eq
adamc@120 512 : forall (A : Type) (x y : A), x == y -> x = y
adamc@120 513 ]] *)
adamc@120 514
adamc@120 515 (** 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.
adamc@120 516
adamc@120 517 We can redo our [fhapp] associativity proof based around [JMeq]. *)
adamc@120 518
adamc@120 519 Section fhapp'.
adamc@120 520 Variable A : Type.
adamc@120 521 Variable B : A -> Type.
adamc@120 522
adamc@120 523 (** This time, the naive theorem statement type-checks. *)
adamc@120 524
adamc@120 525 Theorem fhapp_ass' : forall ls1 ls2 ls3
adamc@120 526 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@120 527 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adamc@120 528 induction ls1; crush.
adamc@120 529
adamc@120 530 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
adamc@120 531
adamc@120 532 [[
adamc@120 533
adamc@120 534 ============================
adamc@120 535 (a0,
adamc@120 536 fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@120 537 (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) ==
adamc@120 538 (a0,
adamc@120 539 fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@120 540 (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@120 541 ]]
adamc@120 542
adamc@120 543 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial.
adamc@120 544
adamc@120 545 [[
adamc@120 546
adamc@120 547 rewrite IHls1.
adamc@120 548
adamc@120 549 [[
adamc@120 550
adamc@120 551 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
adamc@120 552 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
adamc@120 553 ]]
adamc@120 554
adamc@120 555 We see that [JMeq] is not a silver bullet. We can use it to simplify the statements of equality facts, but the Coq type-checker uses non-trivial heterogeneous equality facts no more readily than it uses standard equality facts. Here, the problem is that the form [(e1, e2)] is syntactic sugar for an explicit application of a constructor of an inductive type. That application mentions the type of each tuple element explicitly, and our [rewrite] tries to change one of those elements without updating the corresponding type argument.
adamc@120 556
adamc@120 557 We can get around this problem by another multiple use of [generalize]. We want to bring into the goal the proper instance of the inductive hypothesis, and we also want to generalize the two relevant uses of [fhapp]. *)
adamc@120 558
adamc@120 559 generalize (fhapp b (fhapp hls2 hls3))
adamc@120 560 (fhapp (fhapp b hls2) hls3)
adamc@120 561 (IHls1 _ _ b hls2 hls3).
adamc@120 562 (** [[
adamc@120 563
adamc@120 564 ============================
adamc@120 565 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
adamc@120 566 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
adamc@120 567 ]]
adamc@120 568
adamc@120 569 Now we can rewrite with append associativity, as before. *)
adamc@120 570
adamc@120 571 rewrite app_ass.
adamc@120 572 (** [[
adamc@120 573
adamc@120 574 ============================
adamc@120 575 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
adamc@120 576 ]]
adamc@120 577
adamc@120 578 From this point, the goal is trivial. *)
adamc@120 579
adamc@120 580 intros f f0 H; rewrite H; reflexivity.
adamc@120 581 Qed.
adamc@120 582 End fhapp'.
adamc@121 583
adamc@121 584
adamc@121 585 (** * Equivalence of Equality Axioms *)
adamc@121 586
adamc@121 587 (** Assuming axioms (like axiom K and [JMeq_eq]) is a hazardous business. The due diligence associated with it is necessarily global in scope, since two axioms may be consistent alone but inconsistent together. It turns out that all of the major axioms proposed for reasoning about equality in Coq are logically equivalent, so that we only need to pick one to assert without proof. In this section, we demonstrate this by showing how each the previous two sections' approaches reduces to the other logically.
adamc@121 588
adamc@121 589 To show that [JMeq] and its axiom let us prove [UIP_refl], we start from the lemma [UIP_refl'] from the previous section. The rest of the proof is trivial. *)
adamc@121 590
adamc@121 591 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
adamc@121 592 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@121 593 Qed.
adamc@121 594
adamc@121 595 (** The other direction is perhaps more interesting. Assume that we only have the axiom of the [Eqdep] module available. We can define [JMeq] in a way that satisfies the same interface as the combination of the [JMeq] module's inductive definition and axiom. *)
adamc@121 596
adamc@121 597 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
adamc@121 598 exists pf : B = A, x = match pf with refl_equal => y end.
adamc@121 599
adamc@121 600 Infix "===" := JMeq' (at level 70, no associativity).
adamc@121 601
adamc@121 602 (** We say that, by definition, [x] and [y] are equal if and only if there exists a proof [pf] that their types are equal, such that [x] equals the result of casting [y] with [pf]. This statement can look strange from the standpoint of classical math, where we almost never mention proofs explicitly with quantifiers in formulas, but it is perfectly legal Coq code.
adamc@121 603
adamc@121 604 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
adamc@121 605
adamc@121 606 (** remove printing exists *)
adamc@121 607 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
adamc@121 608 intros; unfold JMeq'; exists (refl_equal A); reflexivity.
adamc@121 609 Qed.
adamc@121 610
adamc@121 611 (** printing exists $\exists$ *)
adamc@121 612
adamc@121 613 (** The proof of an analogue to [JMeq_eq] is a little more interesting, but most of the action is in appealing to [UIP_refl]. *)
adamc@121 614
adamc@121 615 Theorem JMeq_eq' : forall (A : Type) (x y : A),
adamc@121 616 x === y -> x = y.
adamc@121 617 unfold JMeq'; intros.
adamc@121 618 (** [[
adamc@121 619
adamc@121 620 H : exists pf : A = A,
adamc@121 621 x = match pf in (_ = T) return T with
adamc@121 622 | refl_equal => y
adamc@121 623 end
adamc@121 624 ============================
adamc@121 625 x = y
adamc@121 626 ]] *)
adamc@121 627
adamc@121 628 destruct H.
adamc@121 629 (** [[
adamc@121 630
adamc@121 631 x0 : A = A
adamc@121 632 H : x = match x0 in (_ = T) return T with
adamc@121 633 | refl_equal => y
adamc@121 634 end
adamc@121 635 ============================
adamc@121 636 x = y
adamc@121 637 ]] *)
adamc@121 638
adamc@121 639 rewrite H.
adamc@121 640 (** [[
adamc@121 641
adamc@121 642 x0 : A = A
adamc@121 643 ============================
adamc@121 644 match x0 in (_ = T) return T with
adamc@121 645 | refl_equal => y
adamc@121 646 end = y
adamc@121 647 ]] *)
adamc@121 648
adamc@121 649 rewrite (UIP_refl _ _ x0); reflexivity.
adamc@121 650 Qed.
adamc@121 651
adamc@121 652 (** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs. One style may be more convenient than the other for some proofs, but we can always intercovert between our results. The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those "simple" proofs. On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements. *)