Mercurial > cpdt > repo

annotate src/Equality.v @ 122:7cbf0376702f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Definitional equality
author Adam Chlipala <adamc@hcoop.net>
date Sat, 18 Oct 2008 15:32:59 -0400
parents 61e5622b1195
children 9ccd215e5112
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@122 24 (** * The Definitional Equality *)
adamc@122 25
adamc@122 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.
adamc@122 27
adamc@122 28 The [cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [1] when applied to [0]. *)
adamc@122 29
adamc@122 30 Definition pred' (x : nat) :=
adamc@122 31 match x with
adamc@122 32 | O => O
adamc@122 33 | S n' => let y := n' in y
adamc@122 34 end.
adamc@122 35
adamc@122 36 Theorem reduce_me : pred' 1 = 0.
adamc@122 37 (** CIC follows the traditions of lambda calculus in associating reduction rules with Greek letters. Coq can certainly be said to support the familiar alpha reduction rule, which allows capture-avoiding renaming of bound variables, but we never need to apply alpha explicitly, since Coq uses a de Bruijn representation that encodes terms canonically.
adamc@122 38
adamc@122 39 The delta rule is for unfolding global definitions. We can use it here to unfold the definition of [pred']. We do this with the [cbv] tactic, which takes a list of reduction rules and makes as many call-by-value reduction steps as possible, using only those rules. There is an analogous tactic [lazy] for call-by-name reduction. *)
adamc@122 40
adamc@122 41 cbv delta.
adamc@122 42 (** [[
adamc@122 43
adamc@122 44 ============================
adamc@122 45 (fun x : nat => match x with
adamc@122 46 | 0 => 0
adamc@122 47 | S n' => let y := n' in y
adamc@122 48 end) 1 = 0
adamc@122 49 ]]
adamc@122 50
adamc@122 51 At this point, we want to apply the famous beta reduction of lambda calculus, to simplify the application of a known function abstraction. *)
adamc@122 52
adamc@122 53 cbv beta.
adamc@122 54 (** [[
adamc@122 55
adamc@122 56 ============================
adamc@122 57 match 1 with
adamc@122 58 | 0 => 0
adamc@122 59 | S n' => let y := n' in y
adamc@122 60 end = 0
adamc@122 61 ]]
adamc@122 62
adamc@122 63 Next on the list is the iota reduction, which simplifies a single [match] term by determining which pattern matches. *)
adamc@122 64
adamc@122 65 cbv iota.
adamc@122 66 (** [[
adamc@122 67
adamc@122 68 ============================
adamc@122 69 (fun n' : nat => let y := n' in y) 0 = 0
adamc@122 70 ]]
adamc@122 71
adamc@122 72 Now we need another beta reduction. *)
adamc@122 73
adamc@122 74 cbv beta.
adamc@122 75 (** [[
adamc@122 76
adamc@122 77 ============================
adamc@122 78 (let y := 0 in y) = 0
adamc@122 79 ]]
adamc@122 80
adamc@122 81 The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term subsituted. *)
adamc@122 82
adamc@122 83 cbv zeta.
adamc@122 84 (** [[
adamc@122 85
adamc@122 86 ============================
adamc@122 87 0 = 0
adamc@122 88 ]] *)
adamc@122 89
adamc@122 90 reflexivity.
adamc@122 91 Qed.
adamc@122 92
adamc@122 93 (** 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.
adamc@122 94
adamc@122 95 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." *)
adamc@122 96
adamc@122 97
adamc@118 98 (** * Heterogeneous Lists Revisited *)
adamc@118 99
adamc@118 100 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. *)
adamc@118 101
adamc@118 102 Section fhlist.
adamc@118 103 Variable A : Type.
adamc@118 104 Variable B : A -> Type.
adamc@118 105
adamc@118 106 Fixpoint fhlist (ls : list A) : Type :=
adamc@118 107 match ls with
adamc@118 108 | nil => unit
adamc@118 109 | x :: ls' => B x * fhlist ls'
adamc@118 110 end%type.
adamc@118 111
adamc@118 112 Variable elm : A.
adamc@118 113
adamc@118 114 Fixpoint fmember (ls : list A) : Type :=
adamc@118 115 match ls with
adamc@118 116 | nil => Empty_set
adamc@118 117 | x :: ls' => (x = elm) + fmember ls'
adamc@118 118 end%type.
adamc@118 119
adamc@118 120 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@118 121 match ls return fhlist ls -> fmember ls -> B elm with
adamc@118 122 | nil => fun _ idx => match idx with end
adamc@118 123 | _ :: ls' => fun mls idx =>
adamc@118 124 match idx with
adamc@118 125 | inl pf => match pf with
adamc@118 126 | refl_equal => fst mls
adamc@118 127 end
adamc@118 128 | inr idx' => fhget ls' (snd mls) idx'
adamc@118 129 end
adamc@118 130 end.
adamc@118 131 End fhlist.
adamc@118 132
adamc@118 133 Implicit Arguments fhget [A B elm ls].
adamc@118 134
adamc@118 135 (** We can define a [map]-like function for [fhlist]s. *)
adamc@118 136
adamc@118 137 Section fhlist_map.
adamc@118 138 Variables A : Type.
adamc@118 139 Variables B C : A -> Type.
adamc@118 140 Variable f : forall x, B x -> C x.
adamc@118 141
adamc@118 142 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
adamc@118 143 match ls return fhlist B ls -> fhlist C ls with
adamc@118 144 | nil => fun _ => tt
adamc@118 145 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
adamc@118 146 end.
adamc@118 147
adamc@118 148 Implicit Arguments fhmap [ls].
adamc@118 149
adamc@118 150 (** 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 151
adamc@118 152 Variable elm : A.
adamc@118 153
adamc@118 154 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
adamc@118 155 fhget (fhmap hls) mem = f (fhget hls mem).
adamc@118 156 induction ls; crush.
adamc@118 157
adamc@118 158 (** Part of our single remaining subgoal is:
adamc@118 159
adamc@118 160 [[
adamc@118 161
adamc@118 162 a0 : a = elm
adamc@118 163 ============================
adamc@118 164 match a0 in (_ = a2) return (C a2) with
adamc@118 165 | refl_equal => f a1
adamc@118 166 end = f match a0 in (_ = a2) return (B a2) with
adamc@118 167 | refl_equal => a1
adamc@118 168 end
adamc@118 169 ]]
adamc@118 170
adamc@118 171 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 172
adamc@118 173 [[
adamc@118 174
adamc@118 175 destruct a0.
adamc@118 176
adamc@118 177 [[
adamc@118 178 User error: Cannot solve a second-order unification problem
adamc@118 179 ]]
adamc@118 180
adamc@118 181 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 182
adamc@118 183 [[
adamc@118 184
adamc@118 185 assert (a0 = refl_equal _).
adamc@118 186
adamc@118 187 [[
adamc@118 188 The term "refl_equal ?98" has type "?98 = ?98"
adamc@118 189 while it is expected to have type "a = elm"
adamc@118 190 ]]
adamc@118 191
adamc@118 192 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 193
adamc@118 194 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 195
adamc@118 196 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 197
adamc@118 198 case a0.
adamc@118 199 (** [[
adamc@118 200
adamc@118 201 ============================
adamc@118 202 f a1 = f a1
adamc@118 203 ]]
adamc@118 204
adamc@118 205 It seems that [destruct] was trying to be too smart for its own good. *)
adamc@118 206
adamc@118 207 reflexivity.
adamc@118 208 Qed.
adamc@118 209
adamc@118 210 (** 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 211
adamc@118 212 Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
adamc@118 213 simple destruct pf; reflexivity.
adamc@118 214 Qed.
adamc@118 215
adamc@118 216 (** [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 217
adamc@118 218 Print lemma1.
adamc@118 219
adamc@118 220 (** [[
adamc@118 221
adamc@118 222 lemma1 =
adamc@118 223 fun (x : A) (pf : x = elm) =>
adamc@118 224 match pf as e in (_ = y) return (0 = match e with
adamc@118 225 | refl_equal => 0
adamc@118 226 end) with
adamc@118 227 | refl_equal => refl_equal 0
adamc@118 228 end
adamc@118 229 : forall (x : A) (pf : x = elm), 0 = match pf with
adamc@118 230 | refl_equal => 0
adamc@118 231 end
adamc@118 232 ]]
adamc@118 233
adamc@118 234 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
adamc@118 235
adamc@118 236 Definition lemma1' :=
adamc@118 237 fun (x : A) (pf : x = elm) =>
adamc@118 238 match pf return (0 = match pf with
adamc@118 239 | refl_equal => 0
adamc@118 240 end) with
adamc@118 241 | refl_equal => refl_equal 0
adamc@118 242 end.
adamc@118 243
adamc@118 244 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)
adamc@118 245
adamc@118 246 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
adamc@118 247 (** [[
adamc@118 248
adamc@118 249 simple destruct pf.
adamc@118 250
adamc@118 251 [[
adamc@118 252
adamc@118 253 User error: Cannot solve a second-order unification problem
adamc@118 254 ]] *)
adamc@118 255 Abort.
adamc@118 256
adamc@118 257 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
adamc@118 258
adamc@118 259 Definition lemma2' :=
adamc@118 260 fun (x : A) (pf : x = x) =>
adamc@118 261 match pf return (0 = match pf with
adamc@118 262 | refl_equal => 0
adamc@118 263 end) with
adamc@118 264 | refl_equal => refl_equal 0
adamc@118 265 end.
adamc@118 266
adamc@118 267 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
adamc@118 268
adamc@118 269 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@118 270 (** [[
adamc@118 271
adamc@118 272 simple destruct pf.
adamc@118 273
adamc@118 274 [[
adamc@118 275
adamc@118 276 User error: Cannot solve a second-order unification problem
adamc@118 277 ]] *)
adamc@118 278 Abort.
adamc@118 279
adamc@118 280 (** This time, even our manual attempt fails.
adamc@118 281
adamc@118 282 [[
adamc@118 283
adamc@118 284 Definition lemma3' :=
adamc@118 285 fun (x : A) (pf : x = x) =>
adamc@118 286 match pf as pf' in (_ = x') return (pf' = refl_equal x') with
adamc@118 287 | refl_equal => refl_equal _
adamc@118 288 end.
adamc@118 289
adamc@118 290 [[
adamc@118 291
adamc@118 292 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
adamc@118 293 "x = x'"
adamc@118 294 ]]
adamc@118 295
adamc@118 296 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 297
adamc@118 298 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)
adamc@118 299
adamc@118 300 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@118 301 intros; apply UIP_refl.
adamc@118 302 Qed.
adamc@118 303
adamc@118 304 Check UIP_refl.
adamc@118 305 (** [[
adamc@118 306
adamc@118 307 UIP_refl
adamc@118 308 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
adamc@118 309 ]]
adamc@118 310
adamc@118 311 [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 312
adamc@118 313 Print eq_rect_eq.
adamc@118 314 (** [[
adamc@118 315
adamc@118 316 eq_rect_eq =
adamc@118 317 fun U : Type => Eq_rect_eq.eq_rect_eq U
adamc@118 318 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@118 319 x = eq_rect p Q x p h
adamc@118 320 ]]
adamc@118 321
adamc@118 322 [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 323
adamc@118 324 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 325
adamc@118 326 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
adamc@118 327
adamc@118 328 Print Streicher_K.
adamc@118 329 (** [[
adamc@118 330
adamc@118 331 Streicher_K =
adamc@118 332 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
adamc@118 333 : forall (U : Type) (x : U) (P : x = x -> Prop),
adamc@118 334 P (refl_equal x) -> forall p : x = x, P p
adamc@118 335 ]]
adamc@118 336
adamc@118 337 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 338
adamc@118 339 End fhlist_map.
adamc@118 340
adamc@119 341
adamc@119 342 (** * Type-Casts in Theorem Statements *)
adamc@119 343
adamc@119 344 (** 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 345
adamc@119 346 Section fhapp.
adamc@119 347 Variable A : Type.
adamc@119 348 Variable B : A -> Type.
adamc@119 349
adamc@119 350 Fixpoint fhapp (ls1 ls2 : list A) {struct ls1}
adamc@119 351 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
adamc@119 352 match ls1 return fhlist _ ls1 -> _ -> fhlist _ (ls1 ++ ls2) with
adamc@119 353 | nil => fun _ hls2 => hls2
adamc@119 354 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
adamc@119 355 end.
adamc@119 356
adamc@119 357 Implicit Arguments fhapp [ls1 ls2].
adamc@119 358
adamc@119 359 (** We might like to prove that [fhapp] is associative.
adamc@119 360
adamc@119 361 [[
adamc@119 362
adamc@119 363 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 364 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 365 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
adamc@119 366
adamc@119 367 [[
adamc@119 368
adamc@119 369 The term
adamc@119 370 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
adamc@119 371 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
adamc@119 372 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
adamc@119 373 ]]
adamc@119 374
adamc@119 375 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 376
adamc@119 377 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 378 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
adamc@119 379 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 380 fhapp hls1 (fhapp hls2 hls3)
adamc@119 381 = match pf in (_ = ls) return fhlist _ ls with
adamc@119 382 | refl_equal => fhapp (fhapp hls1 hls2) hls3
adamc@119 383 end.
adamc@119 384 induction ls1; crush.
adamc@119 385
adamc@119 386 (** The first remaining subgoal looks trivial enough:
adamc@119 387
adamc@119 388 [[
adamc@119 389
adamc@119 390 ============================
adamc@119 391 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 392 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 393 | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 394 end
adamc@119 395 ]]
adamc@119 396
adamc@119 397 We can try what worked in previous examples.
adamc@119 398
adamc@119 399 [[
adamc@119 400 case pf.
adamc@119 401
adamc@119 402 [[
adamc@119 403
adamc@119 404 User error: Cannot solve a second-order unification problem
adamc@119 405 ]]
adamc@119 406
adamc@119 407 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 408
adamc@119 409 rewrite (UIP_refl _ _ pf).
adamc@119 410 (** [[
adamc@119 411
adamc@119 412 ============================
adamc@119 413 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 414 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 415 ]] *)
adamc@119 416
adamc@119 417 reflexivity.
adamc@119 418
adamc@119 419 (** Our second subgoal is trickier.
adamc@119 420
adamc@119 421 [[
adamc@119 422
adamc@119 423 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 424 ============================
adamc@119 425 (a0,
adamc@119 426 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 427 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 428 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 429 | refl_equal =>
adamc@119 430 (a0,
adamc@119 431 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 432 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 433 end
adamc@119 434 ]]
adamc@119 435
adamc@119 436
adamc@119 437 [[
adamc@119 438
adamc@119 439 rewrite (UIP_refl _ _ pf).
adamc@119 440
adamc@119 441 [[
adamc@119 442 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
adamc@119 443 while it is expected to have type "?556 = ?556"
adamc@119 444 ]]
adamc@119 445
adamc@119 446 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 447
adamc@119 448 injection pf; intro pf'.
adamc@119 449 (** [[
adamc@119 450
adamc@119 451 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 452 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
adamc@119 453 ============================
adamc@119 454 (a0,
adamc@119 455 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 456 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 457 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 458 | refl_equal =>
adamc@119 459 (a0,
adamc@119 460 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 461 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 462 end
adamc@119 463 ]]
adamc@119 464
adamc@119 465 Now we can rewrite using the inductive hypothesis. *)
adamc@119 466
adamc@119 467 rewrite (IHls1 _ _ pf').
adamc@119 468 (** [[
adamc@119 469
adamc@119 470 ============================
adamc@119 471 (a0,
adamc@119 472 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 473 | refl_equal =>
adamc@119 474 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 475 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
adamc@119 476 end) =
adamc@119 477 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 478 | refl_equal =>
adamc@119 479 (a0,
adamc@119 480 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 481 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 482 end
adamc@119 483 ]]
adamc@119 484
adamc@119 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. *)
adamc@119 486
adamc@119 487 generalize (fhapp (fhapp b hls2) hls3).
adamc@119 488 (** [[
adamc@119 489
adamc@119 490 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
adamc@119 491 (a0,
adamc@119 492 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 493 | refl_equal => f
adamc@119 494 end) =
adamc@119 495 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 496 | refl_equal => (a0, f)
adamc@119 497 end
adamc@119 498 ]]
adamc@119 499
adamc@119 500 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 501
adamc@119 502 In this case, it is helpful to generalize over our two proofs as well. *)
adamc@119 503
adamc@119 504 generalize pf pf'.
adamc@119 505 (** [[
adamc@119 506
adamc@119 507 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 508 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 509 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
adamc@119 510 (a0,
adamc@119 511 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 512 | refl_equal => f
adamc@119 513 end) =
adamc@119 514 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 515 | refl_equal => (a0, f)
adamc@119 516 end
adamc@119 517 ]]
adamc@119 518
adamc@119 519 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 520
adamc@119 521 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 522
adamc@119 523 rewrite app_ass.
adamc@119 524 (** [[
adamc@119 525
adamc@119 526 ============================
adamc@119 527 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 528 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 529 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
adamc@119 530 (a0,
adamc@119 531 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 532 | refl_equal => f
adamc@119 533 end) =
adamc@119 534 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 535 | refl_equal => (a0, f)
adamc@119 536 end
adamc@119 537 ]]
adamc@119 538
adamc@119 539 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 540
adamc@119 541 intros.
adamc@119 542 rewrite (UIP_refl _ _ pf0).
adamc@119 543 rewrite (UIP_refl _ _ pf'0).
adamc@119 544 reflexivity.
adamc@119 545 Qed.
adamc@119 546 End fhapp.
adamc@120 547
adamc@120 548 Implicit Arguments fhapp [A B ls1 ls2].
adamc@120 549
adamc@120 550
adamc@120 551 (** * Heterogeneous Equality *)
adamc@120 552
adamc@120 553 (** There is another equality predicate, defined in the [JMeq] module of the standard library, implementing %\textit{%#<i>#heterogeneous equality#</i>#%}%. *)
adamc@120 554
adamc@120 555 Print JMeq.
adamc@120 556 (** [[
adamc@120 557
adamc@120 558 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
adamc@120 559 JMeq_refl : JMeq x x
adamc@120 560 ]]
adamc@120 561
adamc@120 562 [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 563
adamc@120 564 Infix "==" := JMeq (at level 70, no associativity).
adamc@120 565
adamc@121 566 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
adamc@120 567 match pf return (pf == refl_equal _) with
adamc@120 568 | refl_equal => JMeq_refl _
adamc@120 569 end.
adamc@120 570
adamc@120 571 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
adamc@120 572
adamc@121 573 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 574
adamc@120 575 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
adamc@120 576 O = match pf with refl_equal => O end.
adamc@121 577 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@120 578 Qed.
adamc@120 579
adamc@120 580 (** 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 581
adamc@120 582 Check JMeq_eq.
adamc@120 583 (** [[
adamc@120 584
adamc@120 585 JMeq_eq
adamc@120 586 : forall (A : Type) (x y : A), x == y -> x = y
adamc@120 587 ]] *)
adamc@120 588
adamc@120 589 (** 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 590
adamc@120 591 We can redo our [fhapp] associativity proof based around [JMeq]. *)
adamc@120 592
adamc@120 593 Section fhapp'.
adamc@120 594 Variable A : Type.
adamc@120 595 Variable B : A -> Type.
adamc@120 596
adamc@120 597 (** This time, the naive theorem statement type-checks. *)
adamc@120 598
adamc@120 599 Theorem fhapp_ass' : forall ls1 ls2 ls3
adamc@120 600 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@120 601 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adamc@120 602 induction ls1; crush.
adamc@120 603
adamc@120 604 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
adamc@120 605
adamc@120 606 [[
adamc@120 607
adamc@120 608 ============================
adamc@120 609 (a0,
adamc@120 610 fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@120 611 (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) ==
adamc@120 612 (a0,
adamc@120 613 fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@120 614 (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@120 615 ]]
adamc@120 616
adamc@120 617 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial.
adamc@120 618
adamc@120 619 [[
adamc@120 620
adamc@120 621 rewrite IHls1.
adamc@120 622
adamc@120 623 [[
adamc@120 624
adamc@120 625 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
adamc@120 626 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
adamc@120 627 ]]
adamc@120 628
adamc@120 629 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 630
adamc@120 631 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 632
adamc@120 633 generalize (fhapp b (fhapp hls2 hls3))
adamc@120 634 (fhapp (fhapp b hls2) hls3)
adamc@120 635 (IHls1 _ _ b hls2 hls3).
adamc@120 636 (** [[
adamc@120 637
adamc@120 638 ============================
adamc@120 639 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
adamc@120 640 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
adamc@120 641 ]]
adamc@120 642
adamc@120 643 Now we can rewrite with append associativity, as before. *)
adamc@120 644
adamc@120 645 rewrite app_ass.
adamc@120 646 (** [[
adamc@120 647
adamc@120 648 ============================
adamc@120 649 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
adamc@120 650 ]]
adamc@120 651
adamc@120 652 From this point, the goal is trivial. *)
adamc@120 653
adamc@120 654 intros f f0 H; rewrite H; reflexivity.
adamc@120 655 Qed.
adamc@120 656 End fhapp'.
adamc@121 657
adamc@121 658
adamc@121 659 (** * Equivalence of Equality Axioms *)
adamc@121 660
adamc@121 661 (** 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 662
adamc@121 663 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 664
adamc@121 665 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
adamc@121 666 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@121 667 Qed.
adamc@121 668
adamc@121 669 (** 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 670
adamc@121 671 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
adamc@121 672 exists pf : B = A, x = match pf with refl_equal => y end.
adamc@121 673
adamc@121 674 Infix "===" := JMeq' (at level 70, no associativity).
adamc@121 675
adamc@121 676 (** 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 677
adamc@121 678 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
adamc@121 679
adamc@121 680 (** remove printing exists *)
adamc@121 681 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
adamc@121 682 intros; unfold JMeq'; exists (refl_equal A); reflexivity.
adamc@121 683 Qed.
adamc@121 684
adamc@121 685 (** printing exists $\exists$ *)
adamc@121 686
adamc@121 687 (** 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 688
adamc@121 689 Theorem JMeq_eq' : forall (A : Type) (x y : A),
adamc@121 690 x === y -> x = y.
adamc@121 691 unfold JMeq'; intros.
adamc@121 692 (** [[
adamc@121 693
adamc@121 694 H : exists pf : A = A,
adamc@121 695 x = match pf in (_ = T) return T with
adamc@121 696 | refl_equal => y
adamc@121 697 end
adamc@121 698 ============================
adamc@121 699 x = y
adamc@121 700 ]] *)
adamc@121 701
adamc@121 702 destruct H.
adamc@121 703 (** [[
adamc@121 704
adamc@121 705 x0 : A = A
adamc@121 706 H : x = match x0 in (_ = T) return T with
adamc@121 707 | refl_equal => y
adamc@121 708 end
adamc@121 709 ============================
adamc@121 710 x = y
adamc@121 711 ]] *)
adamc@121 712
adamc@121 713 rewrite H.
adamc@121 714 (** [[
adamc@121 715
adamc@121 716 x0 : A = A
adamc@121 717 ============================
adamc@121 718 match x0 in (_ = T) return T with
adamc@121 719 | refl_equal => y
adamc@121 720 end = y
adamc@121 721 ]] *)
adamc@121 722
adamc@121 723 rewrite (UIP_refl _ _ x0); reflexivity.
adamc@121 724 Qed.
adamc@121 725
adamc@121 726 (** 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. *)