Mercurial > cpdt > repo

annotate src/Equality.v @ 539:8dddcaaeb67a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Two English errors fixed
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Aug 2015 15:54:11 -0400
parents d65e9c1c9041
children 81d63d9c1cc5
rev   line source
adam@534 1 (* Copyright (c) 2008-2012, 2015, 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
adam@534 13 Require Import Cpdt.CpdtTactics.
adamc@118 14
adamc@118 15 Set Implicit Arguments.
adam@534 16 Set Asymmetric Patterns.
adamc@118 17 (* end hide *)
adamc@118 18
adamc@118 19
adamc@118 20 (** %\chapter{Reasoning About Equality Proofs}% *)
adamc@118 21
adam@456 22 (** 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 in Coq, 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. *)
adamc@118 23
adamc@118 24
adamc@122 25 (** * The Definitional Equality *)
adamc@122 26
adam@435 27 (** 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%\index{definitional equality}% _definitional equality_. 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 28
adam@364 29 The %\index{tactics!cbv}%[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 [0] when applied to [1]. *)
adamc@122 30
adamc@122 31 Definition pred' (x : nat) :=
adamc@122 32 match x with
adamc@122 33 | O => O
adamc@122 34 | S n' => let y := n' in y
adamc@122 35 end.
adamc@122 36
adamc@122 37 Theorem reduce_me : pred' 1 = 0.
adamc@218 38
adamc@124 39 (* begin thide *)
adam@364 40 (** 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%~\cite{DeBruijn}% that encodes terms canonically.
adamc@122 41
adam@364 42 The %\index{delta reduction}%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 %\index{tactics!lazy}%[lazy] for call-by-need reduction. *)
adamc@122 43
adamc@122 44 cbv delta.
adam@364 45 (** %\vspace{-.15in}%[[
adamc@122 46 ============================
adamc@122 47 (fun x : nat => match x with
adamc@122 48 | 0 => 0
adamc@122 49 | S n' => let y := n' in y
adamc@122 50 end) 1 = 0
adamc@122 51 ]]
adamc@122 52
adam@364 53 At this point, we want to apply the famous %\index{beta reduction}%beta reduction of lambda calculus, to simplify the application of a known function abstraction. *)
adamc@122 54
adamc@122 55 cbv beta.
adam@364 56 (** %\vspace{-.15in}%[[
adamc@122 57 ============================
adamc@122 58 match 1 with
adamc@122 59 | 0 => 0
adamc@122 60 | S n' => let y := n' in y
adamc@122 61 end = 0
adamc@122 62 ]]
adamc@122 63
adam@364 64 Next on the list is the %\index{iota reduction}%iota reduction, which simplifies a single [match] term by determining which pattern matches. *)
adamc@122 65
adamc@122 66 cbv iota.
adam@364 67 (** %\vspace{-.15in}%[[
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.
adam@364 75 (** %\vspace{-.15in}%[[
adamc@122 76 ============================
adamc@122 77 (let y := 0 in y) = 0
adamc@122 78 ]]
adamc@122 79
adam@364 80 The final reduction rule is %\index{zeta reduction}%zeta, which replaces a [let] expression by its body with the appropriate term substituted. *)
adamc@122 81
adamc@122 82 cbv zeta.
adam@364 83 (** %\vspace{-.15in}%[[
adamc@122 84 ============================
adamc@122 85 0 = 0
adam@302 86 ]]
adam@302 87 *)
adamc@122 88
adamc@122 89 reflexivity.
adamc@122 90 Qed.
adamc@124 91 (* end thide *)
adamc@122 92
adam@365 93 (** The [beta] reduction rule applies to recursive functions as well, and its behavior may be surprising in some instances. For instance, we can run some simple tests using the reduction strategy [compute], which applies all applicable rules of the definitional equality. *)
adam@365 94
adam@365 95 Definition id (n : nat) := n.
adam@365 96
adam@365 97 Eval compute in fun x => id x.
adam@365 98 (** %\vspace{-.15in}%[[
adam@365 99 = fun x : nat => x
adam@365 100 ]]
adam@365 101 *)
adam@365 102
adam@365 103 Fixpoint id' (n : nat) := n.
adam@365 104
adam@365 105 Eval compute in fun x => id' x.
adam@365 106 (** %\vspace{-.15in}%[[
adam@365 107 = fun x : nat => (fix id' (n : nat) : nat := n) x
adam@365 108 ]]
adam@365 109
adam@479 110 By running [compute], we ask Coq to run reduction steps until no more apply, so why do we see an application of a known function, where clearly no beta reduction has been performed? The answer has to do with ensuring termination of all Gallina programs. One candidate rule would say that we apply recursive definitions wherever possible. However, this would clearly lead to nonterminating reduction sequences, since the function may appear fully applied within its own definition, and we would %\%naive%{}%ly "simplify" such applications immediately. Instead, Coq only applies the beta rule for a recursive function when _the top-level structure of the recursive argument is known_. For [id'] above, we have only one argument [n], so clearly it is the recursive argument, and the top-level structure of [n] is known when the function is applied to [O] or to some [S e] term. The variable [x] is neither, so reduction is blocked.
adam@365 111
adam@365 112 What are recursive arguments in general? Every recursive function is compiled by Coq to a %\index{Gallina terms!fix}%[fix] expression, for anonymous definition of recursive functions. Further, every [fix] with multiple arguments has one designated as the recursive argument via a [struct] annotation. The recursive argument is the one that must decrease across recursive calls, to appease Coq's termination checker. Coq will generally infer which argument is recursive, though we may also specify it manually, if we want to tweak reduction behavior. For instance, consider this definition of a function to add two lists of [nat]s elementwise: *)
adam@365 113
adam@365 114 Fixpoint addLists (ls1 ls2 : list nat) : list nat :=
adam@365 115 match ls1, ls2 with
adam@365 116 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists ls1' ls2'
adam@365 117 | _, _ => nil
adam@365 118 end.
adam@365 119
adam@365 120 (** By default, Coq chooses [ls1] as the recursive argument. We can see that [ls2] would have been another valid choice. The choice has a critical effect on reduction behavior, as these two examples illustrate: *)
adam@365 121
adam@365 122 Eval compute in fun ls => addLists nil ls.
adam@365 123 (** %\vspace{-.15in}%[[
adam@365 124 = fun _ : list nat => nil
adam@365 125 ]]
adam@365 126 *)
adam@365 127
adam@365 128 Eval compute in fun ls => addLists ls nil.
adam@365 129 (** %\vspace{-.15in}%[[
adam@365 130 = fun ls : list nat =>
adam@365 131 (fix addLists (ls1 ls2 : list nat) : list nat :=
adam@365 132 match ls1 with
adam@365 133 | nil => nil
adam@365 134 | n1 :: ls1' =>
adam@365 135 match ls2 with
adam@365 136 | nil => nil
adam@365 137 | n2 :: ls2' =>
adam@365 138 (fix plus (n m : nat) : nat :=
adam@365 139 match n with
adam@365 140 | 0 => m
adam@365 141 | S p => S (plus p m)
adam@365 142 end) n1 n2 :: addLists ls1' ls2'
adam@365 143 end
adam@365 144 end) ls nil
adam@365 145 ]]
adam@365 146
adam@427 147 The outer application of the [fix] expression for [addLists] was only simplified in the first case, because in the second case the recursive argument is [ls], whose top-level structure is not known.
adam@365 148
adam@427 149 The opposite behavior pertains to a version of [addLists] with [ls2] marked as recursive. *)
adam@365 150
adam@365 151 Fixpoint addLists' (ls1 ls2 : list nat) {struct ls2} : list nat :=
adam@365 152 match ls1, ls2 with
adam@365 153 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists' ls1' ls2'
adam@365 154 | _, _ => nil
adam@365 155 end.
adam@365 156
adam@427 157 (* begin hide *)
adam@437 158 (* begin thide *)
adam@437 159 Definition foo := (@eq, plus).
adam@437 160 (* end thide *)
adam@427 161 (* end hide *)
adam@427 162
adam@365 163 Eval compute in fun ls => addLists' ls nil.
adam@365 164 (** %\vspace{-.15in}%[[
adam@365 165 = fun ls : list nat => match ls with
adam@365 166 | nil => nil
adam@365 167 | _ :: _ => nil
adam@365 168 end
adam@365 169 ]]
adam@365 170
adam@365 171 We see that all use of recursive functions has been eliminated, though the term has not quite simplified to [nil]. We could get it to do so by switching the order of the [match] discriminees in the definition of [addLists'].
adam@365 172
adam@365 173 Recall that co-recursive definitions have a dual rule: a co-recursive call only simplifies when it is the discriminee of a [match]. This condition is built into the beta rule for %\index{Gallina terms!cofix}%[cofix], the anonymous form of [CoFixpoint].
adam@365 174
adam@365 175 %\medskip%
adam@365 176
adam@407 177 The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a%\index{propositional equality}% _propositional equality_, 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 178
adam@427 179 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." *)
adamc@122 180
adamc@122 181
adamc@118 182 (** * Heterogeneous Lists Revisited *)
adamc@118 183
adam@480 184 (** One of our example dependent data structures from the last chapter (code repeated below) was the heterogeneous list and its associated "cursor" type. The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [fmember] types. *)
adamc@118 185
adamc@118 186 Section fhlist.
adamc@118 187 Variable A : Type.
adamc@118 188 Variable B : A -> Type.
adamc@118 189
adamc@118 190 Fixpoint fhlist (ls : list A) : Type :=
adamc@118 191 match ls with
adamc@118 192 | nil => unit
adamc@118 193 | x :: ls' => B x * fhlist ls'
adamc@118 194 end%type.
adamc@118 195
adamc@118 196 Variable elm : A.
adamc@118 197
adamc@118 198 Fixpoint fmember (ls : list A) : Type :=
adamc@118 199 match ls with
adamc@118 200 | nil => Empty_set
adamc@118 201 | x :: ls' => (x = elm) + fmember ls'
adamc@118 202 end%type.
adamc@118 203
adamc@118 204 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@118 205 match ls return fhlist ls -> fmember ls -> B elm with
adamc@118 206 | nil => fun _ idx => match idx with end
adamc@118 207 | _ :: ls' => fun mls idx =>
adamc@118 208 match idx with
adamc@118 209 | inl pf => match pf with
adam@426 210 | eq_refl => fst mls
adamc@118 211 end
adamc@118 212 | inr idx' => fhget ls' (snd mls) idx'
adamc@118 213 end
adamc@118 214 end.
adamc@118 215 End fhlist.
adamc@118 216
adamc@118 217 Implicit Arguments fhget [A B elm ls].
adamc@118 218
adam@427 219 (* begin hide *)
adam@437 220 (* begin thide *)
adam@427 221 Definition map := O.
adam@437 222 (* end thide *)
adam@427 223 (* end hide *)
adam@427 224
adamc@118 225 (** We can define a [map]-like function for [fhlist]s. *)
adamc@118 226
adamc@118 227 Section fhlist_map.
adamc@118 228 Variables A : Type.
adamc@118 229 Variables B C : A -> Type.
adamc@118 230 Variable f : forall x, B x -> C x.
adamc@118 231
adamc@118 232 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
adamc@118 233 match ls return fhlist B ls -> fhlist C ls with
adamc@118 234 | nil => fun _ => tt
adamc@118 235 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
adamc@118 236 end.
adamc@118 237
adamc@118 238 Implicit Arguments fhmap [ls].
adamc@118 239
adam@427 240 (* begin hide *)
adam@437 241 (* begin thide *)
adam@427 242 Definition ilist := O.
adam@427 243 Definition get := O.
adam@427 244 Definition imap := O.
adam@437 245 (* end thide *)
adam@427 246 (* end hide *)
adam@427 247
adam@502 248 (** 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, which sets us on a collision course with the problems that are the subject of this chapter. *)
adamc@118 249
adamc@118 250 Variable elm : A.
adamc@118 251
adam@479 252 Theorem fhget_fhmap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
adamc@118 253 fhget (fhmap hls) mem = f (fhget hls mem).
adam@298 254 (* begin hide *)
adam@298 255 induction ls; crush; case a0; reflexivity.
adam@298 256 (* end hide *)
adam@364 257 (** %\vspace{-.2in}%[[
adamc@118 258 induction ls; crush.
adam@298 259 ]]
adamc@118 260
adam@364 261 %\vspace{-.15in}%In Coq 8.2, one subgoal remains at this point. Coq 8.3 has added some tactic improvements that enable [crush] to complete all of both inductive cases. To introduce the basics of reasoning about equality, it will be useful to review what was necessary in Coq 8.2.
adam@297 262
adam@297 263 Part of our single remaining subgoal is:
adamc@118 264 [[
adamc@118 265 a0 : a = elm
adamc@118 266 ============================
adamc@118 267 match a0 in (_ = a2) return (C a2) with
adam@426 268 | eq_refl => f a1
adamc@118 269 end = f match a0 in (_ = a2) return (B a2) with
adam@426 270 | eq_refl => a1
adamc@118 271 end
adamc@118 272 ]]
adamc@118 273
adam@502 274 This seems like a trivial enough obligation. The equality proof [a0] must be [eq_refl], the only constructor of [eq]. Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
adamc@118 275 [[
adamc@118 276 destruct a0.
adamc@118 277 ]]
adamc@118 278
adam@364 279 <<
adam@364 280 User error: Cannot solve a second-order unification problem
adam@364 281 >>
adam@364 282
adam@502 283 This is one of Coq's standard error messages for informing us of a failure in its heuristics for attempting an instance of an undecidable problem about dependent typing. We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
adamc@118 284 [[
adam@426 285 assert (a0 = eq_refl _).
adam@364 286 ]]
adamc@118 287
adam@364 288 <<
adam@426 289 The term "eq_refl ?98" has type "?98 = ?98"
adamc@118 290 while it is expected to have type "a = elm"
adam@364 291 >>
adamc@118 292
adamc@118 293 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 294
adam@427 295 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 296
adam@407 297 For this particular example, the solution is surprisingly straightforward. The [destruct] tactic has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments.
adam@297 298 [[
adamc@118 299 case a0.
adam@297 300
adamc@118 301 ============================
adamc@118 302 f a1 = f a1
adamc@118 303 ]]
adamc@118 304
adam@297 305 It seems that [destruct] was trying to be too smart for its own good.
adam@297 306 [[
adamc@118 307 reflexivity.
adam@302 308 ]]
adam@364 309 %\vspace{-.2in}% *)
adamc@118 310 Qed.
adamc@124 311 (* end thide *)
adamc@118 312
adamc@118 313 (** 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 314
adam@426 315 Lemma lemma1 : forall x (pf : x = elm), O = match pf with eq_refl => O end.
adamc@124 316 (* begin thide *)
adamc@118 317 simple destruct pf; reflexivity.
adamc@118 318 Qed.
adamc@124 319 (* end thide *)
adamc@118 320
adam@364 321 (** The tactic %\index{tactics!simple destruct}%[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 322
adamc@118 323 Print lemma1.
adamc@218 324 (** %\vspace{-.15in}% [[
adamc@118 325 lemma1 =
adamc@118 326 fun (x : A) (pf : x = elm) =>
adamc@118 327 match pf as e in (_ = y) return (0 = match e with
adam@426 328 | eq_refl => 0
adamc@118 329 end) with
adam@426 330 | eq_refl => eq_refl 0
adamc@118 331 end
adamc@118 332 : forall (x : A) (pf : x = elm), 0 = match pf with
adam@426 333 | eq_refl => 0
adamc@118 334 end
adamc@218 335
adamc@118 336 ]]
adamc@118 337
adamc@118 338 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
adamc@118 339
adamc@124 340 (* begin thide *)
adam@456 341 Definition lemma1' (x : A) (pf : x = elm) :=
adam@456 342 match pf return (0 = match pf with
adam@456 343 | eq_refl => 0
adam@456 344 end) with
adam@456 345 | eq_refl => eq_refl 0
adam@456 346 end.
adamc@124 347 (* end thide *)
adamc@118 348
adam@398 349 (** Surprisingly, what seems at first like a _simpler_ lemma is harder to prove. *)
adamc@118 350
adam@426 351 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with eq_refl => O end.
adamc@124 352 (* begin thide *)
adam@364 353 (** %\vspace{-.25in}%[[
adamc@118 354 simple destruct pf.
adam@364 355 ]]
adamc@205 356
adam@364 357 <<
adamc@118 358 User error: Cannot solve a second-order unification problem
adam@364 359 >>
adam@302 360 *)
adamc@118 361 Abort.
adamc@118 362
adamc@118 363 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
adamc@118 364
adamc@124 365 (* begin thide *)
adamc@124 366 Definition lemma2 :=
adamc@118 367 fun (x : A) (pf : x = x) =>
adamc@118 368 match pf return (0 = match pf with
adam@426 369 | eq_refl => 0
adamc@118 370 end) with
adam@426 371 | eq_refl => eq_refl 0
adamc@118 372 end.
adamc@124 373 (* end thide *)
adamc@118 374
adamc@118 375 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
adamc@118 376
adam@427 377 (* begin hide *)
adam@437 378 (* begin thide *)
adam@427 379 Definition lemma3' := O.
adam@437 380 (* end thide *)
adam@427 381 (* end hide *)
adam@427 382
adam@426 383 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
adamc@124 384 (* begin thide *)
adam@364 385 (** %\vspace{-.25in}%[[
adamc@118 386 simple destruct pf.
adam@364 387 ]]
adamc@205 388
adam@364 389 <<
adamc@118 390 User error: Cannot solve a second-order unification problem
adam@364 391 >>
adam@364 392 %\vspace{-.15in}%*)
adamc@218 393
adamc@118 394 Abort.
adamc@118 395
adamc@118 396 (** This time, even our manual attempt fails.
adamc@118 397 [[
adamc@118 398 Definition lemma3' :=
adamc@118 399 fun (x : A) (pf : x = x) =>
adam@426 400 match pf as pf' in (_ = x') return (pf' = eq_refl x') with
adam@426 401 | eq_refl => eq_refl _
adamc@118 402 end.
adam@364 403 ]]
adamc@118 404
adam@364 405 <<
adam@426 406 The term "eq_refl x'" has type "x' = x'" while it is expected to have type
adamc@118 407 "x = x'"
adam@364 408 >>
adamc@118 409
adam@427 410 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], referring to the [in]-bound variable [x']. To do a dependent [match], we _must_ 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 _must_ equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
adamc@118 411
adam@398 412 Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *)
adamc@118 413
adam@426 414 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
adamc@118 415 intros; apply UIP_refl.
adamc@118 416 Qed.
adamc@118 417
adamc@118 418 Check UIP_refl.
adamc@218 419 (** %\vspace{-.15in}% [[
adamc@118 420 UIP_refl
adam@426 421 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
adamc@118 422 ]]
adamc@118 423
adam@480 424 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. (Its name uses the acronym "UIP" for "unicity of identity proofs.") Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an _axiom_, the term [eq_rect_eq] below. *)
adam@427 425
adam@436 426 (* begin hide *)
adam@436 427 Import Eq_rect_eq.
adam@436 428 (* end hide *)
adamc@118 429 Print eq_rect_eq.
adamc@218 430 (** %\vspace{-.15in}% [[
adam@436 431 *** [ eq_rect_eq :
adam@436 432 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@436 433 x = eq_rect p Q x p h ]
adamc@118 434 ]]
adamc@118 435
adam@502 436 The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. The term [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]. The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed. We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy. *)
adam@427 437
adam@427 438 (* begin hide *)
adam@437 439 (* begin thide *)
adam@427 440 Definition False' := False.
adam@437 441 (* end thide *)
adam@427 442 (* end hide *)
adamc@118 443
adam@364 444 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@364 445 x = eq_rect p Q x p h).
adam@364 446 (** %\vspace{-.15in}%[[
adam@364 447 = forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@364 448 x = match h in (_ = y) return (Q y) with
adam@364 449 | eq_refl => x
adam@364 450 end
adam@364 451 ]]
adam@364 452
adam@427 453 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an %\index{axioms}%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 _inconsistent_ 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%~\cite{AxiomK}%, in a study that also established unprovability of the axiom in CIC.
adamc@118 454
adamc@118 455 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
adamc@118 456
adam@427 457 (* begin hide *)
adam@437 458 (* begin thide *)
adam@437 459 Definition Streicher_K' := UIP_refl__Streicher_K.
adam@437 460 (* end thide *)
adam@427 461 (* end hide *)
adam@427 462
adam@480 463 Check Streicher_K.
adamc@124 464 (* end thide *)
adamc@218 465 (** %\vspace{-.15in}% [[
adam@480 466 Streicher_K
adamc@118 467 : forall (U : Type) (x : U) (P : x = x -> Prop),
adam@480 468 P eq_refl -> forall p : x = x, P p
adamc@118 469 ]]
adamc@118 470
adam@480 471 This is the opaquely named %\index{axiom K}%"Streicher's axiom K," which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
adamc@118 472
adamc@118 473 End fhlist_map.
adamc@118 474
adam@436 475 (* begin hide *)
adam@437 476 (* begin thide *)
adam@436 477 Require Eqdep_dec.
adam@437 478 (* end thide *)
adam@436 479 (* end hide *)
adam@436 480
adam@364 481 (** It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality. The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases. To simplify presentation, we will stick with the axiom version in the rest of this chapter. *)
adam@364 482
adamc@119 483
adamc@119 484 (** * Type-Casts in Theorem Statements *)
adamc@119 485
adamc@119 486 (** 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 487
adamc@119 488 Section fhapp.
adamc@119 489 Variable A : Type.
adamc@119 490 Variable B : A -> Type.
adamc@119 491
adamc@218 492 Fixpoint fhapp (ls1 ls2 : list A)
adamc@119 493 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
adamc@218 494 match ls1 with
adamc@119 495 | nil => fun _ hls2 => hls2
adamc@119 496 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
adamc@119 497 end.
adamc@119 498
adamc@119 499 Implicit Arguments fhapp [ls1 ls2].
adamc@119 500
adamc@124 501 (* EX: Prove that fhapp is associative. *)
adamc@124 502 (* begin thide *)
adamc@124 503
adamc@119 504 (** We might like to prove that [fhapp] is associative.
adamc@119 505 [[
adam@479 506 Theorem fhapp_assoc : forall ls1 ls2 ls3
adamc@119 507 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 508 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
adam@364 509 ]]
adamc@119 510
adam@364 511 <<
adamc@119 512 The term
adamc@119 513 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
adamc@119 514 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
adamc@119 515 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
adam@364 516 >>
adamc@119 517
adam@407 518 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%\index{intensional type theory}% _intensional_, 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 519
adam@479 520 Theorem fhapp_assoc : forall ls1 ls2 ls3
adamc@119 521 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
adamc@119 522 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 523 fhapp hls1 (fhapp hls2 hls3)
adamc@119 524 = match pf in (_ = ls) return fhlist _ ls with
adam@426 525 | eq_refl => fhapp (fhapp hls1 hls2) hls3
adamc@119 526 end.
adamc@119 527 induction ls1; crush.
adamc@119 528
adamc@119 529 (** The first remaining subgoal looks trivial enough:
adamc@119 530 [[
adamc@119 531 ============================
adamc@119 532 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 533 match pf in (_ = ls) return (fhlist B ls) with
adam@426 534 | eq_refl => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 535 end
adamc@119 536 ]]
adamc@119 537
adamc@119 538 We can try what worked in previous examples.
adamc@119 539 [[
adamc@119 540 case pf.
adam@364 541 ]]
adamc@119 542
adam@364 543 <<
adamc@119 544 User error: Cannot solve a second-order unification problem
adam@364 545 >>
adamc@119 546
adamc@119 547 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 548
adamc@119 549 rewrite (UIP_refl _ _ pf).
adamc@119 550 (** [[
adamc@119 551 ============================
adamc@119 552 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 553 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adam@302 554 ]]
adam@302 555 *)
adamc@119 556
adamc@119 557 reflexivity.
adamc@119 558
adamc@119 559 (** Our second subgoal is trickier.
adamc@119 560 [[
adamc@119 561 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 562 ============================
adamc@119 563 (a0,
adamc@119 564 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 565 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 566 match pf in (_ = ls) return (fhlist B ls) with
adam@426 567 | eq_refl =>
adamc@119 568 (a0,
adamc@119 569 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 570 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 571 end
adamc@119 572
adamc@119 573 rewrite (UIP_refl _ _ pf).
adam@364 574 ]]
adamc@119 575
adam@364 576 <<
adamc@119 577 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
adamc@119 578 while it is expected to have type "?556 = ?556"
adam@364 579 >>
adamc@119 580
adamc@119 581 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 582
adamc@119 583 injection pf; intro pf'.
adamc@119 584 (** [[
adamc@119 585 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 586 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
adamc@119 587 ============================
adamc@119 588 (a0,
adamc@119 589 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 590 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 591 match pf in (_ = ls) return (fhlist B ls) with
adam@426 592 | eq_refl =>
adamc@119 593 (a0,
adamc@119 594 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 595 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 596 end
adamc@119 597 ]]
adamc@119 598
adamc@119 599 Now we can rewrite using the inductive hypothesis. *)
adamc@119 600
adamc@119 601 rewrite (IHls1 _ _ pf').
adamc@119 602 (** [[
adamc@119 603 ============================
adamc@119 604 (a0,
adamc@119 605 match pf' in (_ = ls) return (fhlist B ls) with
adam@426 606 | eq_refl =>
adamc@119 607 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 608 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
adamc@119 609 end) =
adamc@119 610 match pf in (_ = ls) return (fhlist B ls) with
adam@426 611 | eq_refl =>
adamc@119 612 (a0,
adamc@119 613 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 614 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 615 end
adamc@119 616 ]]
adamc@119 617
adam@398 618 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 _does not matter what the result of the call is_. In other words, the subgoal should remain true if we replace this [fhapp] call with a fresh variable. The %\index{tactics!generalize}%[generalize] tactic helps us do exactly that. *)
adamc@119 619
adamc@119 620 generalize (fhapp (fhapp b hls2) hls3).
adamc@119 621 (** [[
adamc@119 622 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
adamc@119 623 (a0,
adamc@119 624 match pf' in (_ = ls) return (fhlist B ls) with
adam@426 625 | eq_refl => f
adamc@119 626 end) =
adamc@119 627 match pf in (_ = ls) return (fhlist B ls) with
adam@426 628 | eq_refl => (a0, f)
adamc@119 629 end
adamc@119 630 ]]
adamc@119 631
adam@502 632 The conclusion has gotten markedly simpler. It seems counterintuitive that we can have an easier time of proving a more general theorem, but such a phenomenon applies to the case here and to many other proofs that use dependent types heavily. Speaking informally, the reason why this kind of activity helps is that [match] annotations contain some positions where only variables are allowed. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood.
adamc@119 633
adamc@119 634 In this case, it is helpful to generalize over our two proofs as well. *)
adamc@119 635
adamc@119 636 generalize pf pf'.
adamc@119 637 (** [[
adamc@119 638 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 639 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 640 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
adamc@119 641 (a0,
adamc@119 642 match pf'0 in (_ = ls) return (fhlist B ls) with
adam@426 643 | eq_refl => f
adamc@119 644 end) =
adamc@119 645 match pf0 in (_ = ls) return (fhlist B ls) with
adam@426 646 | eq_refl => (a0, f)
adamc@119 647 end
adamc@119 648 ]]
adamc@119 649
adam@502 650 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 so 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 651
adam@398 652 However, now that we have generalized over the [fhapp] call, the type of the term being type-cast appears explicitly in the goal and _may be rewritten as well_. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append. *)
adamc@119 653
adam@479 654 rewrite app_assoc.
adamc@119 655 (** [[
adamc@119 656 ============================
adamc@119 657 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 658 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 659 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
adamc@119 660 (a0,
adamc@119 661 match pf'0 in (_ = ls) return (fhlist B ls) with
adam@426 662 | eq_refl => f
adamc@119 663 end) =
adamc@119 664 match pf0 in (_ = ls) return (fhlist B ls) with
adam@426 665 | eq_refl => (a0, f)
adamc@119 666 end
adamc@119 667 ]]
adamc@119 668
adamc@119 669 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 670
adamc@119 671 intros.
adamc@119 672 rewrite (UIP_refl _ _ pf0).
adamc@119 673 rewrite (UIP_refl _ _ pf'0).
adamc@119 674 reflexivity.
adamc@119 675 Qed.
adamc@124 676 (* end thide *)
adamc@119 677 End fhapp.
adamc@120 678
adamc@120 679 Implicit Arguments fhapp [A B ls1 ls2].
adamc@120 680
adam@364 681 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics. The next section explores an alternative that leads to simpler developments in some cases. *)
adam@364 682
adamc@120 683
adamc@120 684 (** * Heterogeneous Equality *)
adamc@120 685
adam@407 686 (** There is another equality predicate, defined in the %\index{Gallina terms!JMeq}%[JMeq] module of the standard library, implementing%\index{heterogeneous equality}% _heterogeneous equality_. *)
adamc@120 687
adamc@120 688 Print JMeq.
adamc@218 689 (** %\vspace{-.15in}% [[
adamc@120 690 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
adamc@120 691 JMeq_refl : JMeq x x
adamc@120 692 ]]
adamc@120 693
adam@480 694 The identifier [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as an inside joke about British politics. The definition [JMeq] starts out looking a lot like the definition of [eq]. The crucial difference is that we may use [JMeq] _on arguments of different types_. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *)
adamc@120 695
adamc@120 696 Infix "==" := JMeq (at level 70, no associativity).
adamc@120 697
adam@426 698 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
adamc@124 699 (* begin thide *)
adam@426 700 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == eq_refl x :=
adam@426 701 match pf return (pf == eq_refl _) with
adam@426 702 | eq_refl => JMeq_refl _
adamc@120 703 end.
adamc@124 704 (* end thide *)
adamc@120 705
adamc@120 706 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
adamc@120 707
adamc@271 708 Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *)
adamc@120 709
adamc@120 710 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
adam@426 711 O = match pf with eq_refl => O end.
adamc@124 712 (* begin thide *)
adamc@121 713 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@120 714 Qed.
adamc@124 715 (* end thide *)
adamc@120 716
adamc@120 717 (** 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 718
adamc@120 719 Check JMeq_eq.
adamc@218 720 (** %\vspace{-.15in}% [[
adamc@120 721 JMeq_eq
adamc@120 722 : forall (A : Type) (x y : A), x == y -> x = y
adamc@218 723 ]]
adamc@120 724
adam@480 725 It may be surprising that we cannot prove that heterogeneous equality implies normal equality. The difficulties are the same kind we have seen so far, based on limitations of [match] annotations. The [JMeq_eq] axiom has been proved on paper to be consistent, but asserting it may still be considered to complicate the logic we work in, so there is some motivation for avoiding it.
adamc@120 726
adamc@120 727 We can redo our [fhapp] associativity proof based around [JMeq]. *)
adamc@120 728
adamc@120 729 Section fhapp'.
adamc@120 730 Variable A : Type.
adamc@120 731 Variable B : A -> Type.
adamc@120 732
adam@484 733 (** This time, the %\%naive%{}% theorem statement type-checks. *)
adamc@120 734
adamc@124 735 (* EX: Prove [fhapp] associativity using [JMeq]. *)
adamc@124 736
adamc@124 737 (* begin thide *)
adam@479 738 Theorem fhapp_assoc' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
adam@364 739 (hls3 : fhlist B ls3),
adamc@120 740 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adamc@120 741 induction ls1; crush.
adamc@120 742
adamc@120 743 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
adamc@120 744 [[
adamc@120 745 ============================
adam@297 746 (a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
adamc@120 747 ]]
adamc@120 748
adam@297 749 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial. Here is what happens when we try that in Coq 8.2:
adamc@120 750 [[
adamc@120 751 rewrite IHls1.
adam@364 752 ]]
adamc@120 753
adam@364 754 <<
adamc@120 755 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
adamc@120 756 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
adam@364 757 >>
adamc@120 758
adam@407 759 Coq 8.4 currently gives an error message about an uncaught exception. Perhaps that will be fixed soon. In any case, it is educational to consider a more explicit approach.
adam@297 760
adamc@120 761 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 762
adamc@120 763 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 764
adamc@120 765 generalize (fhapp b (fhapp hls2 hls3))
adamc@120 766 (fhapp (fhapp b hls2) hls3)
adamc@120 767 (IHls1 _ _ b hls2 hls3).
adam@364 768 (** %\vspace{-.15in}%[[
adamc@120 769 ============================
adamc@120 770 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
adamc@120 771 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
adamc@120 772 ]]
adamc@120 773
adamc@120 774 Now we can rewrite with append associativity, as before. *)
adamc@120 775
adam@479 776 rewrite app_assoc.
adam@364 777 (** %\vspace{-.15in}%[[
adamc@120 778 ============================
adamc@120 779 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
adamc@120 780 ]]
adamc@120 781
adamc@120 782 From this point, the goal is trivial. *)
adamc@120 783
adamc@120 784 intros f f0 H; rewrite H; reflexivity.
adamc@120 785 Qed.
adamc@124 786 (* end thide *)
adamc@121 787
adam@385 788 End fhapp'.
adam@385 789
adam@385 790 (** This example illustrates a general pattern: heterogeneous equality often simplifies theorem statements, but we still need to do some work to line up some dependent pattern matches that tactics will generate for us.
adam@385 791
adam@385 792 The proof we have found relies on the [JMeq_eq] axiom, which we can verify with a command%\index{Vernacular commands!Print Assumptions}% that we will discuss more in two chapters. *)
adam@385 793
adam@479 794 Print Assumptions fhapp_assoc'.
adam@385 795 (** %\vspace{-.15in}%[[
adam@385 796 Axioms:
adam@385 797 JMeq_eq : forall (A : Type) (x y : A), x == y -> x = y
adam@385 798 ]]
adam@385 799
adam@385 800 It was the [rewrite H] tactic that implicitly appealed to the axiom. By restructuring the proof, we can avoid axiom dependence. A general lemma about pairs provides the key element. (Our use of [generalize] above can be thought of as reducing the proof to another, more complex and specialized lemma.) *)
adam@385 801
adam@385 802 Lemma pair_cong : forall A1 A2 B1 B2 (x1 : A1) (x2 : A2) (y1 : B1) (y2 : B2),
adam@385 803 x1 == x2
adam@385 804 -> y1 == y2
adam@385 805 -> (x1, y1) == (x2, y2).
adam@385 806 intros until y2; intros Hx Hy; rewrite Hx; rewrite Hy; reflexivity.
adam@385 807 Qed.
adam@385 808
adam@385 809 Hint Resolve pair_cong.
adam@385 810
adam@385 811 Section fhapp''.
adam@385 812 Variable A : Type.
adam@385 813 Variable B : A -> Type.
adam@385 814
adam@479 815 Theorem fhapp_assoc'' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
adam@385 816 (hls3 : fhlist B ls3),
adam@385 817 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adam@385 818 induction ls1; crush.
adam@385 819 Qed.
adam@385 820 End fhapp''.
adam@385 821
adam@479 822 Print Assumptions fhapp_assoc''.
adam@385 823 (** <<
adam@385 824 Closed under the global context
adam@385 825 >>
adam@385 826
adam@479 827 One might wonder exactly which elements of a proof involving [JMeq] imply that [JMeq_eq] must be used. For instance, above we noticed that [rewrite] had brought [JMeq_eq] into the proof of [fhapp_assoc'], yet here we have also used [rewrite] with [JMeq] hypotheses while avoiding axioms! One illuminating exercise is comparing the types of the lemmas that [rewrite] uses under the hood to implement the rewrites. Here is the normal lemma for [eq] rewriting:%\index{Gallina terms!eq\_ind\_r}% *)
adam@385 828
adam@385 829 Check eq_ind_r.
adam@385 830 (** %\vspace{-.15in}%[[
adam@385 831 eq_ind_r
adam@385 832 : forall (A : Type) (x : A) (P : A -> Prop),
adam@385 833 P x -> forall y : A, y = x -> P y
adam@385 834 ]]
adam@385 835
adam@536 836 The corresponding lemma used for [JMeq] in the proof of [pair_cong] is defined internally by [rewrite] as needed, but its type happens to be the following. *)
adam@385 837
adam@385 838 (** %\vspace{-.15in}%[[
adam@398 839 internal_JMeq_rew_r
adam@385 840 : forall (A : Type) (x : A) (B : Type) (b : B)
adam@385 841 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x
adam@385 842 ]]
adam@385 843
adam@534 844 The key difference is that, where the [eq] lemma is parameterized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop]. To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y]. In contrast, to apply the alternative principle, it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and _its type_. In other words, the predicate must be _polymorphic_ in [y]'s type; any type must make sense, from a type-checking standpoint. There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done %\%naive%{}%ly leads to a type error.
adam@385 845
adam@536 846 When [rewrite] cannot figure out how to apply the alternative principle for [x == y] where [x] and [y] have the same type, the tactic can instead use a different theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *)
adam@385 847
adam@385 848 Check JMeq_ind_r.
adam@385 849 (** %\vspace{-.15in}%[[
adam@385 850 JMeq_ind_r
adam@385 851 : forall (A : Type) (x : A) (P : A -> Prop),
adam@385 852 P x -> forall y : A, y == x -> P y
adam@385 853 ]]
adam@385 854
adam@534 855 Ironically, where in the proof of [fhapp_assoc'] we used [rewrite app_assoc] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free principle!
adam@385 856
adam@385 857 For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *)
adam@385 858
adam@385 859 Theorem out_of_luck : forall n m : nat,
adam@385 860 n == m
adam@385 861 -> S n == S m.
adam@385 862 intros n m H.
adam@385 863
adam@480 864 (** Applying [JMeq_ind_r] is easy, as the %\index{tactics!pattern}%[pattern] tactic will transform the goal into an application of an appropriate [fun] to a term that we want to abstract. (In general, [pattern] abstracts over a term by introducing a new anonymous function taking that term as argument.) *)
adam@385 865
adam@385 866 pattern n.
adam@385 867 (** %\vspace{-.15in}%[[
adam@385 868 n : nat
adam@385 869 m : nat
adam@385 870 H : n == m
adam@385 871 ============================
adam@385 872 (fun n0 : nat => S n0 == S m) n
adam@385 873 ]]
adam@385 874 *)
adam@385 875 apply JMeq_ind_r with (x := m); auto.
adam@385 876
adam@534 877 (** However, we run into trouble trying to get the goal into a form compatible with the alternative principle. *)
adam@427 878
adam@385 879 Undo 2.
adam@385 880 (** %\vspace{-.15in}%[[
adam@385 881 pattern nat, n.
adam@385 882 ]]
adam@385 883 <<
adam@385 884 Error: The abstracted term "fun (P : Set) (n0 : P) => S n0 == S m"
adam@385 885 is not well typed.
adam@385 886 Illegal application (Type Error):
adam@385 887 The term "S" of type "nat -> nat"
adam@385 888 cannot be applied to the term
adam@385 889 "n0" : "P"
adam@385 890 This term has type "P" which should be coercible to
adam@385 891 "nat".
adam@385 892 >>
adam@385 893
adam@385 894 In other words, the successor function [S] is insufficiently polymorphic. If we try to generalize over the type of [n], we find that [S] is no longer legal to apply to [n]. *)
adam@385 895
adam@385 896 Abort.
adam@385 897
adam@479 898 (** Why did we not run into this problem in our proof of [fhapp_assoc'']? The reason is that the pair constructor is polymorphic in the types of the pair components, while functions like [S] are not polymorphic at all. Use of such non-polymorphic functions with [JMeq] tends to push toward use of axioms. The example with [nat] here is a bit unrealistic; more likely cases would involve functions that have _some_ polymorphism, but not enough to allow abstractions of the sort we attempted above with [pattern]. For instance, we might have an equality between two lists, where the goal only type-checks when the terms involved really are lists, though everything is polymorphic in the types of list data elements. The {{http://www.mpi-sws.org/~gil/Heq/}Heq} library builds up a slightly different foundation to help avoid such problems. *)
adam@364 899
adamc@121 900
adamc@121 901 (** * Equivalence of Equality Axioms *)
adamc@121 902
adamc@124 903 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
adamc@124 904
adamc@124 905 (* begin thide *)
adam@502 906 (** 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 by showing how each of the previous two sections' approaches reduces to the other logically.
adamc@121 907
adamc@121 908 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 909
adam@426 910 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = eq_refl x.
adamc@121 911 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@121 912 Qed.
adamc@121 913
adamc@121 914 (** 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 915
adamc@121 916 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
adam@426 917 exists pf : B = A, x = match pf with eq_refl => y end.
adamc@121 918
adamc@121 919 Infix "===" := JMeq' (at level 70, no associativity).
adamc@121 920
adam@427 921 (** remove printing exists *)
adam@427 922
adamc@121 923 (** 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 924
adamc@121 925 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
adamc@121 926
adamc@121 927 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
adam@426 928 intros; unfold JMeq'; exists (eq_refl A); reflexivity.
adamc@121 929 Qed.
adamc@121 930
adamc@121 931 (** printing exists $\exists$ *)
adamc@121 932
adamc@121 933 (** 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 934
adamc@121 935 Theorem JMeq_eq' : forall (A : Type) (x y : A),
adamc@121 936 x === y -> x = y.
adamc@121 937 unfold JMeq'; intros.
adamc@121 938 (** [[
adamc@121 939 H : exists pf : A = A,
adamc@121 940 x = match pf in (_ = T) return T with
adam@426 941 | eq_refl => y
adamc@121 942 end
adamc@121 943 ============================
adamc@121 944 x = y
adam@302 945 ]]
adam@302 946 *)
adamc@121 947
adamc@121 948 destruct H.
adamc@121 949 (** [[
adamc@121 950 x0 : A = A
adamc@121 951 H : x = match x0 in (_ = T) return T with
adam@426 952 | eq_refl => y
adamc@121 953 end
adamc@121 954 ============================
adamc@121 955 x = y
adam@302 956 ]]
adam@302 957 *)
adamc@121 958
adamc@121 959 rewrite H.
adamc@121 960 (** [[
adamc@121 961 x0 : A = A
adamc@121 962 ============================
adamc@121 963 match x0 in (_ = T) return T with
adam@426 964 | eq_refl => y
adamc@121 965 end = y
adam@302 966 ]]
adam@302 967 *)
adamc@121 968
adamc@121 969 rewrite (UIP_refl _ _ x0); reflexivity.
adamc@121 970 Qed.
adamc@121 971
adam@427 972 (** 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 interconvert 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. *)
adamc@123 973
adamc@124 974 (* end thide *)
adamc@123 975
adamc@123 976
adamc@123 977 (** * Equality of Functions *)
adamc@123 978
adam@444 979 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory.
adam@444 980 %\vspace{-.15in}%[[
adam@456 981 Theorem two_funs : (fun n => n) = (fun n => n + 0).
adamc@205 982 ]]
adam@444 983 %\vspace{-.15in}%Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be%\index{extensionality of function equality}% _extensional_. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We _can_ assert function extensionality as an axiom, and indeed the standard library already contains that axiom. *)
adamc@123 984
adam@407 985 Require Import FunctionalExtensionality.
adam@407 986 About functional_extensionality.
adam@407 987 (** %\vspace{-.15in}%[[
adam@407 988 functional_extensionality :
adam@407 989 forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g
adam@407 990 ]]
adam@407 991 *)
adamc@123 992
adam@456 993 (** This axiom has been verified metatheoretically to be consistent with CIC and the two equality axioms we considered previously. With it, the proof of [two_funs] is trivial. *)
adamc@123 994
adam@456 995 Theorem two_funs : (fun n => n) = (fun n => n + 0).
adamc@124 996 (* begin thide *)
adam@407 997 apply functional_extensionality; crush.
adamc@123 998 Qed.
adamc@124 999 (* end thide *)
adamc@123 1000
adam@427 1001 (** The same axiom can help us prove equality of types, where we need to "reason under quantifiers." *)
adamc@123 1002
adamc@123 1003 Theorem forall_eq : (forall x : nat, match x with
adamc@123 1004 | O => True
adamc@123 1005 | S _ => True
adamc@123 1006 end)
adamc@123 1007 = (forall _ : nat, True).
adamc@123 1008
adam@456 1009 (** There are no immediate opportunities to apply [functional_extensionality], but we can use %\index{tactics!change}%[change] to fix that problem. *)
adamc@123 1010
adamc@124 1011 (* begin thide *)
adamc@123 1012 change ((forall x : nat, (fun x => match x with
adamc@123 1013 | 0 => True
adamc@123 1014 | S _ => True
adamc@123 1015 end) x) = (nat -> True)).
adam@407 1016 rewrite (functional_extensionality (fun x => match x with
adam@407 1017 | 0 => True
adam@407 1018 | S _ => True
adam@407 1019 end) (fun _ => True)).
adamc@123 1020 (** [[
adamc@123 1021 2 subgoals
adamc@123 1022
adamc@123 1023 ============================
adamc@123 1024 (nat -> True) = (nat -> True)
adamc@123 1025
adamc@123 1026 subgoal 2 is:
adamc@123 1027 forall x : nat, match x with
adamc@123 1028 | 0 => True
adamc@123 1029 | S _ => True
adamc@123 1030 end = True
adam@302 1031 ]]
adam@302 1032 *)
adamc@123 1033
adamc@123 1034 reflexivity.
adamc@123 1035
adamc@123 1036 destruct x; constructor.
adamc@123 1037 Qed.
adamc@124 1038 (* end thide *)
adamc@127 1039
adam@407 1040 (** Unlike in the case of [eq_rect_eq], we have no way of deriving this axiom of%\index{functional extensionality}% _functional extensionality_ for types with decidable equality. To allow equality reasoning without axioms, it may be worth rewriting a development to replace functions with alternate representations, such as finite map types for which extensionality is derivable in CIC. *)