Mercurial > cpdt > repo

annotate src/Equality.v @ 429:5744842c36a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through Universes, to incorporate new coqdoc features
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 11:55:52 -0400
parents 5e6b76ca14de
children a54a4a2ea6e4
rev   line source
adam@398 1 (* Copyright (c) 2008-2012, 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@314 13 Require Import CpdtTactics.
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
adam@294 21 (** In traditional mathematics, the concept of equality is usually taken as a given. On the other hand, in type theory, equality is a very contentious subject. There are at least three different notions of equality that are important, and researchers are actively investigating new definitions of what it means for two terms to be equal. Even once we fix a notion of equality, there are inevitably tricky issues that arise in proving properties of programs that manipulate equality proofs explicitly. In this chapter, I will focus on design patterns for circumventing these tricky issues, and I will introduce the different notions of equality as they are germane. *)
adamc@118 22
adamc@118 23
adamc@122 24 (** * The Definitional Equality *)
adamc@122 25
adam@427 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%\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 27
adam@364 28 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 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@218 37
adamc@124 38 (* begin thide *)
adam@364 39 (** 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 40
adam@364 41 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 42
adamc@122 43 cbv delta.
adam@364 44 (** %\vspace{-.15in}%[[
adamc@122 45 ============================
adamc@122 46 (fun x : nat => match x with
adamc@122 47 | 0 => 0
adamc@122 48 | S n' => let y := n' in y
adamc@122 49 end) 1 = 0
adamc@122 50 ]]
adamc@122 51
adam@364 52 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 53
adamc@122 54 cbv beta.
adam@364 55 (** %\vspace{-.15in}%[[
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
adam@364 63 Next on the list is the %\index{iota reduction}%iota reduction, which simplifies a single [match] term by determining which pattern matches. *)
adamc@122 64
adamc@122 65 cbv iota.
adam@364 66 (** %\vspace{-.15in}%[[
adamc@122 67 ============================
adamc@122 68 (fun n' : nat => let y := n' in y) 0 = 0
adamc@122 69 ]]
adamc@122 70
adamc@122 71 Now we need another beta reduction. *)
adamc@122 72
adamc@122 73 cbv beta.
adam@364 74 (** %\vspace{-.15in}%[[
adamc@122 75 ============================
adamc@122 76 (let y := 0 in y) = 0
adamc@122 77 ]]
adamc@122 78
adam@364 79 The final reduction rule is %\index{zeta reduction}%zeta, which replaces a [let] expression by its body with the appropriate term substituted. *)
adamc@122 80
adamc@122 81 cbv zeta.
adam@364 82 (** %\vspace{-.15in}%[[
adamc@122 83 ============================
adamc@122 84 0 = 0
adam@302 85 ]]
adam@302 86 *)
adamc@122 87
adamc@122 88 reflexivity.
adamc@122 89 Qed.
adamc@124 90 (* end thide *)
adamc@122 91
adam@365 92 (** 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 93
adam@365 94 Definition id (n : nat) := n.
adam@365 95
adam@365 96 Eval compute in fun x => id x.
adam@365 97 (** %\vspace{-.15in}%[[
adam@365 98 = fun x : nat => x
adam@365 99 ]]
adam@365 100 *)
adam@365 101
adam@365 102 Fixpoint id' (n : nat) := n.
adam@365 103
adam@365 104 Eval compute in fun x => id' x.
adam@365 105 (** %\vspace{-.15in}%[[
adam@365 106 = fun x : nat => (fix id' (n : nat) : nat := n) x
adam@365 107 ]]
adam@365 108
adam@427 109 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 naively "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 110
adam@365 111 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 112
adam@365 113 Fixpoint addLists (ls1 ls2 : list nat) : list nat :=
adam@365 114 match ls1, ls2 with
adam@365 115 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists ls1' ls2'
adam@365 116 | _, _ => nil
adam@365 117 end.
adam@365 118
adam@365 119 (** 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 120
adam@365 121 Eval compute in fun ls => addLists nil ls.
adam@365 122 (** %\vspace{-.15in}%[[
adam@365 123 = fun _ : list nat => nil
adam@365 124 ]]
adam@365 125 *)
adam@365 126
adam@365 127 Eval compute in fun ls => addLists ls nil.
adam@365 128 (** %\vspace{-.15in}%[[
adam@365 129 = fun ls : list nat =>
adam@365 130 (fix addLists (ls1 ls2 : list nat) : list nat :=
adam@365 131 match ls1 with
adam@365 132 | nil => nil
adam@365 133 | n1 :: ls1' =>
adam@365 134 match ls2 with
adam@365 135 | nil => nil
adam@365 136 | n2 :: ls2' =>
adam@365 137 (fix plus (n m : nat) : nat :=
adam@365 138 match n with
adam@365 139 | 0 => m
adam@365 140 | S p => S (plus p m)
adam@365 141 end) n1 n2 :: addLists ls1' ls2'
adam@365 142 end
adam@365 143 end) ls nil
adam@365 144 ]]
adam@365 145
adam@427 146 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 147
adam@427 148 The opposite behavior pertains to a version of [addLists] with [ls2] marked as recursive. *)
adam@365 149
adam@365 150 Fixpoint addLists' (ls1 ls2 : list nat) {struct ls2} : list nat :=
adam@365 151 match ls1, ls2 with
adam@365 152 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists' ls1' ls2'
adam@365 153 | _, _ => nil
adam@365 154 end.
adam@365 155
adam@427 156 (* begin hide *)
adam@427 157 Definition foo := @eq.
adam@427 158 (* end hide *)
adam@427 159
adam@365 160 Eval compute in fun ls => addLists' ls nil.
adam@365 161 (** %\vspace{-.15in}%[[
adam@365 162 = fun ls : list nat => match ls with
adam@365 163 | nil => nil
adam@365 164 | _ :: _ => nil
adam@365 165 end
adam@365 166 ]]
adam@365 167
adam@365 168 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 169
adam@365 170 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 171
adam@365 172 %\medskip%
adam@365 173
adam@407 174 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 175
adam@427 176 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 177
adamc@122 178
adamc@118 179 (** * Heterogeneous Lists Revisited *)
adamc@118 180
adam@427 181 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [fmember] types. *)
adamc@118 182
adamc@118 183 Section fhlist.
adamc@118 184 Variable A : Type.
adamc@118 185 Variable B : A -> Type.
adamc@118 186
adamc@118 187 Fixpoint fhlist (ls : list A) : Type :=
adamc@118 188 match ls with
adamc@118 189 | nil => unit
adamc@118 190 | x :: ls' => B x * fhlist ls'
adamc@118 191 end%type.
adamc@118 192
adamc@118 193 Variable elm : A.
adamc@118 194
adamc@118 195 Fixpoint fmember (ls : list A) : Type :=
adamc@118 196 match ls with
adamc@118 197 | nil => Empty_set
adamc@118 198 | x :: ls' => (x = elm) + fmember ls'
adamc@118 199 end%type.
adamc@118 200
adamc@118 201 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@118 202 match ls return fhlist ls -> fmember ls -> B elm with
adamc@118 203 | nil => fun _ idx => match idx with end
adamc@118 204 | _ :: ls' => fun mls idx =>
adamc@118 205 match idx with
adamc@118 206 | inl pf => match pf with
adam@426 207 | eq_refl => fst mls
adamc@118 208 end
adamc@118 209 | inr idx' => fhget ls' (snd mls) idx'
adamc@118 210 end
adamc@118 211 end.
adamc@118 212 End fhlist.
adamc@118 213
adamc@118 214 Implicit Arguments fhget [A B elm ls].
adamc@118 215
adam@427 216 (* begin hide *)
adam@427 217 Definition map := O.
adam@427 218 (* end hide *)
adam@427 219
adamc@118 220 (** We can define a [map]-like function for [fhlist]s. *)
adamc@118 221
adamc@118 222 Section fhlist_map.
adamc@118 223 Variables A : Type.
adamc@118 224 Variables B C : A -> Type.
adamc@118 225 Variable f : forall x, B x -> C x.
adamc@118 226
adamc@118 227 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
adamc@118 228 match ls return fhlist B ls -> fhlist C ls with
adamc@118 229 | nil => fun _ => tt
adamc@118 230 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
adamc@118 231 end.
adamc@118 232
adamc@118 233 Implicit Arguments fhmap [ls].
adamc@118 234
adam@427 235 (* begin hide *)
adam@427 236 Definition ilist := O.
adam@427 237 Definition get := O.
adam@427 238 Definition imap := O.
adam@427 239 (* end hide *)
adam@427 240
adamc@118 241 (** 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 242
adamc@118 243 Variable elm : A.
adamc@118 244
adamc@118 245 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
adamc@118 246 fhget (fhmap hls) mem = f (fhget hls mem).
adam@298 247 (* begin hide *)
adam@298 248 induction ls; crush; case a0; reflexivity.
adam@298 249 (* end hide *)
adam@364 250 (** %\vspace{-.2in}%[[
adamc@118 251 induction ls; crush.
adam@298 252 ]]
adamc@118 253
adam@364 254 %\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 255
adam@297 256 Part of our single remaining subgoal is:
adamc@118 257 [[
adamc@118 258 a0 : a = elm
adamc@118 259 ============================
adamc@118 260 match a0 in (_ = a2) return (C a2) with
adam@426 261 | eq_refl => f a1
adamc@118 262 end = f match a0 in (_ = a2) return (B a2) with
adam@426 263 | eq_refl => a1
adamc@118 264 end
adamc@118 265 ]]
adamc@118 266
adam@426 267 This seems like a trivial enough obligation. The equality proof [a0] must be [eq_refl], 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 268 [[
adamc@118 269 destruct a0.
adamc@118 270 ]]
adamc@118 271
adam@364 272 <<
adam@364 273 User error: Cannot solve a second-order unification problem
adam@364 274 >>
adam@364 275
adamc@118 276 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 277 [[
adam@426 278 assert (a0 = eq_refl _).
adam@364 279 ]]
adamc@118 280
adam@364 281 <<
adam@426 282 The term "eq_refl ?98" has type "?98 = ?98"
adamc@118 283 while it is expected to have type "a = elm"
adam@364 284 >>
adamc@118 285
adamc@118 286 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 287
adam@427 288 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 289
adam@407 290 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 291 [[
adamc@118 292 case a0.
adam@297 293
adamc@118 294 ============================
adamc@118 295 f a1 = f a1
adamc@118 296 ]]
adamc@118 297
adam@297 298 It seems that [destruct] was trying to be too smart for its own good.
adam@297 299 [[
adamc@118 300 reflexivity.
adam@302 301 ]]
adam@364 302 %\vspace{-.2in}% *)
adamc@118 303 Qed.
adamc@124 304 (* end thide *)
adamc@118 305
adamc@118 306 (** 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 307
adam@426 308 Lemma lemma1 : forall x (pf : x = elm), O = match pf with eq_refl => O end.
adamc@124 309 (* begin thide *)
adamc@118 310 simple destruct pf; reflexivity.
adamc@118 311 Qed.
adamc@124 312 (* end thide *)
adamc@118 313
adam@364 314 (** 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 315
adamc@118 316 Print lemma1.
adamc@218 317 (** %\vspace{-.15in}% [[
adamc@118 318 lemma1 =
adamc@118 319 fun (x : A) (pf : x = elm) =>
adamc@118 320 match pf as e in (_ = y) return (0 = match e with
adam@426 321 | eq_refl => 0
adamc@118 322 end) with
adam@426 323 | eq_refl => eq_refl 0
adamc@118 324 end
adamc@118 325 : forall (x : A) (pf : x = elm), 0 = match pf with
adam@426 326 | eq_refl => 0
adamc@118 327 end
adamc@218 328
adamc@118 329 ]]
adamc@118 330
adamc@118 331 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
adamc@118 332
adamc@124 333 (* begin thide *)
adamc@118 334 Definition lemma1' :=
adamc@118 335 fun (x : A) (pf : x = elm) =>
adamc@118 336 match pf return (0 = match pf with
adam@426 337 | eq_refl => 0
adamc@118 338 end) with
adam@426 339 | eq_refl => eq_refl 0
adamc@118 340 end.
adamc@124 341 (* end thide *)
adamc@118 342
adam@398 343 (** Surprisingly, what seems at first like a _simpler_ lemma is harder to prove. *)
adamc@118 344
adam@426 345 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with eq_refl => O end.
adamc@124 346 (* begin thide *)
adam@364 347 (** %\vspace{-.25in}%[[
adamc@118 348 simple destruct pf.
adam@364 349 ]]
adamc@205 350
adam@364 351 <<
adamc@118 352 User error: Cannot solve a second-order unification problem
adam@364 353 >>
adam@302 354 *)
adamc@118 355 Abort.
adamc@118 356
adamc@118 357 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
adamc@118 358
adamc@124 359 (* begin thide *)
adamc@124 360 Definition lemma2 :=
adamc@118 361 fun (x : A) (pf : x = x) =>
adamc@118 362 match pf return (0 = match pf with
adam@426 363 | eq_refl => 0
adamc@118 364 end) with
adam@426 365 | eq_refl => eq_refl 0
adamc@118 366 end.
adamc@124 367 (* end thide *)
adamc@118 368
adamc@118 369 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
adamc@118 370
adam@427 371 (* begin hide *)
adam@427 372 Definition lemma3' := O.
adam@427 373 (* end hide *)
adam@427 374
adam@426 375 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
adamc@124 376 (* begin thide *)
adam@364 377 (** %\vspace{-.25in}%[[
adamc@118 378 simple destruct pf.
adam@364 379 ]]
adamc@205 380
adam@364 381 <<
adamc@118 382 User error: Cannot solve a second-order unification problem
adam@364 383 >>
adam@364 384 %\vspace{-.15in}%*)
adamc@218 385
adamc@118 386 Abort.
adamc@118 387
adamc@118 388 (** This time, even our manual attempt fails.
adamc@118 389 [[
adamc@118 390 Definition lemma3' :=
adamc@118 391 fun (x : A) (pf : x = x) =>
adam@426 392 match pf as pf' in (_ = x') return (pf' = eq_refl x') with
adam@426 393 | eq_refl => eq_refl _
adamc@118 394 end.
adam@364 395 ]]
adamc@118 396
adam@364 397 <<
adam@426 398 The term "eq_refl x'" has type "x' = x'" while it is expected to have type
adamc@118 399 "x = x'"
adam@364 400 >>
adamc@118 401
adam@427 402 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 403
adam@398 404 Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *)
adamc@118 405
adam@426 406 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
adamc@118 407 intros; apply UIP_refl.
adamc@118 408 Qed.
adamc@118 409
adamc@118 410 Check UIP_refl.
adamc@218 411 (** %\vspace{-.15in}% [[
adamc@118 412 UIP_refl
adam@426 413 : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
adamc@118 414 ]]
adamc@118 415
adam@427 416 The theorem %\index{Gallina terms!UIP\_refl}%[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 _axiom_, the term [Eq_rect_eq.eq_rect_eq] below. *)
adam@427 417
adam@427 418 (* begin hide *)
adam@427 419 Definition ere := eq_rect_eq.
adam@427 420 (* end hide *)
adamc@118 421
adamc@118 422 Print eq_rect_eq.
adamc@218 423 (** %\vspace{-.15in}% [[
adamc@118 424 eq_rect_eq =
adamc@118 425 fun U : Type => Eq_rect_eq.eq_rect_eq U
adamc@118 426 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@118 427 x = eq_rect p Q x p h
adamc@118 428 ]]
adamc@118 429
adam@427 430 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 (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *)
adam@427 431
adam@427 432 (* begin hide *)
adam@427 433 Definition False' := False.
adam@427 434 (* end hide *)
adamc@118 435
adam@364 436 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@364 437 x = eq_rect p Q x p h).
adam@364 438 (** %\vspace{-.15in}%[[
adam@364 439 = forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@364 440 x = match h in (_ = y) return (Q y) with
adam@364 441 | eq_refl => x
adam@364 442 end
adam@364 443 ]]
adam@364 444
adam@427 445 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 446
adamc@118 447 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
adamc@118 448
adam@427 449 (* begin hide *)
adam@427 450 Definition Streicher_K' := (Streicher_K, UIP_refl__Streicher_K).
adam@427 451 (* end hide *)
adam@427 452
adamc@118 453 Print Streicher_K.
adamc@124 454 (* end thide *)
adamc@218 455 (** %\vspace{-.15in}% [[
adamc@118 456 Streicher_K =
adamc@118 457 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
adamc@118 458 : forall (U : Type) (x : U) (P : x = x -> Prop),
adam@426 459 P (eq_refl x) -> forall p : x = x, P p
adamc@118 460 ]]
adamc@118 461
adam@427 462 This is the unfortunately 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 463
adamc@118 464 End fhlist_map.
adamc@118 465
adam@364 466 (** 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 467
adamc@119 468
adamc@119 469 (** * Type-Casts in Theorem Statements *)
adamc@119 470
adamc@119 471 (** 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 472
adamc@119 473 Section fhapp.
adamc@119 474 Variable A : Type.
adamc@119 475 Variable B : A -> Type.
adamc@119 476
adamc@218 477 Fixpoint fhapp (ls1 ls2 : list A)
adamc@119 478 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
adamc@218 479 match ls1 with
adamc@119 480 | nil => fun _ hls2 => hls2
adamc@119 481 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
adamc@119 482 end.
adamc@119 483
adamc@119 484 Implicit Arguments fhapp [ls1 ls2].
adamc@119 485
adamc@124 486 (* EX: Prove that fhapp is associative. *)
adamc@124 487 (* begin thide *)
adamc@124 488
adamc@119 489 (** We might like to prove that [fhapp] is associative.
adamc@119 490 [[
adamc@119 491 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 492 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 493 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
adam@364 494 ]]
adamc@119 495
adam@364 496 <<
adamc@119 497 The term
adamc@119 498 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
adamc@119 499 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
adamc@119 500 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
adam@364 501 >>
adamc@119 502
adam@407 503 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 504
adamc@119 505 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 506 (pf : (ls1 ++ ls2) ++ ls3 = 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)
adamc@119 509 = match pf in (_ = ls) return fhlist _ ls with
adam@426 510 | eq_refl => fhapp (fhapp hls1 hls2) hls3
adamc@119 511 end.
adamc@119 512 induction ls1; crush.
adamc@119 513
adamc@119 514 (** The first remaining subgoal looks trivial enough:
adamc@119 515 [[
adamc@119 516 ============================
adamc@119 517 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 518 match pf in (_ = ls) return (fhlist B ls) with
adam@426 519 | eq_refl => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 520 end
adamc@119 521 ]]
adamc@119 522
adamc@119 523 We can try what worked in previous examples.
adamc@119 524 [[
adamc@119 525 case pf.
adam@364 526 ]]
adamc@119 527
adam@364 528 <<
adamc@119 529 User error: Cannot solve a second-order unification problem
adam@364 530 >>
adamc@119 531
adamc@119 532 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 533
adamc@119 534 rewrite (UIP_refl _ _ pf).
adamc@119 535 (** [[
adamc@119 536 ============================
adamc@119 537 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 538 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adam@302 539 ]]
adam@302 540 *)
adamc@119 541
adamc@119 542 reflexivity.
adamc@119 543
adamc@119 544 (** Our second subgoal is trickier.
adamc@119 545 [[
adamc@119 546 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 547 ============================
adamc@119 548 (a0,
adamc@119 549 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 550 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 551 match pf in (_ = ls) return (fhlist B ls) with
adam@426 552 | eq_refl =>
adamc@119 553 (a0,
adamc@119 554 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 555 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 556 end
adamc@119 557
adamc@119 558 rewrite (UIP_refl _ _ pf).
adam@364 559 ]]
adamc@119 560
adam@364 561 <<
adamc@119 562 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
adamc@119 563 while it is expected to have type "?556 = ?556"
adam@364 564 >>
adamc@119 565
adamc@119 566 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 567
adamc@119 568 injection pf; intro pf'.
adamc@119 569 (** [[
adamc@119 570 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 571 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
adamc@119 572 ============================
adamc@119 573 (a0,
adamc@119 574 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 575 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 576 match pf in (_ = ls) return (fhlist B ls) with
adam@426 577 | eq_refl =>
adamc@119 578 (a0,
adamc@119 579 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 580 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 581 end
adamc@119 582 ]]
adamc@119 583
adamc@119 584 Now we can rewrite using the inductive hypothesis. *)
adamc@119 585
adamc@119 586 rewrite (IHls1 _ _ pf').
adamc@119 587 (** [[
adamc@119 588 ============================
adamc@119 589 (a0,
adamc@119 590 match pf' in (_ = ls) return (fhlist B ls) with
adam@426 591 | eq_refl =>
adamc@119 592 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 593 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
adamc@119 594 end) =
adamc@119 595 match pf in (_ = ls) return (fhlist B ls) with
adam@426 596 | eq_refl =>
adamc@119 597 (a0,
adamc@119 598 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 599 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 600 end
adamc@119 601 ]]
adamc@119 602
adam@398 603 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 604
adamc@119 605 generalize (fhapp (fhapp b hls2) hls3).
adamc@119 606 (** [[
adamc@119 607 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
adamc@119 608 (a0,
adamc@119 609 match pf' in (_ = ls) return (fhlist B ls) with
adam@426 610 | eq_refl => f
adamc@119 611 end) =
adamc@119 612 match pf in (_ = ls) return (fhlist B ls) with
adam@426 613 | eq_refl => (a0, f)
adamc@119 614 end
adamc@119 615 ]]
adamc@119 616
adamc@119 617 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 618
adamc@119 619 In this case, it is helpful to generalize over our two proofs as well. *)
adamc@119 620
adamc@119 621 generalize pf pf'.
adamc@119 622 (** [[
adamc@119 623 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 624 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 625 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
adamc@119 626 (a0,
adamc@119 627 match pf'0 in (_ = ls) return (fhlist B ls) with
adam@426 628 | eq_refl => f
adamc@119 629 end) =
adamc@119 630 match pf0 in (_ = ls) return (fhlist B ls) with
adam@426 631 | eq_refl => (a0, f)
adamc@119 632 end
adamc@119 633 ]]
adamc@119 634
adamc@119 635 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 636
adam@398 637 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 638
adamc@119 639 rewrite app_ass.
adamc@119 640 (** [[
adamc@119 641 ============================
adamc@119 642 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 643 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 644 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
adamc@119 645 (a0,
adamc@119 646 match pf'0 in (_ = ls) return (fhlist B ls) with
adam@426 647 | eq_refl => f
adamc@119 648 end) =
adamc@119 649 match pf0 in (_ = ls) return (fhlist B ls) with
adam@426 650 | eq_refl => (a0, f)
adamc@119 651 end
adamc@119 652 ]]
adamc@119 653
adamc@119 654 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 655
adamc@119 656 intros.
adamc@119 657 rewrite (UIP_refl _ _ pf0).
adamc@119 658 rewrite (UIP_refl _ _ pf'0).
adamc@119 659 reflexivity.
adamc@119 660 Qed.
adamc@124 661 (* end thide *)
adamc@119 662 End fhapp.
adamc@120 663
adamc@120 664 Implicit Arguments fhapp [A B ls1 ls2].
adamc@120 665
adam@364 666 (** 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 667
adamc@120 668
adamc@120 669 (** * Heterogeneous Equality *)
adamc@120 670
adam@407 671 (** 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 672
adamc@120 673 Print JMeq.
adamc@218 674 (** %\vspace{-.15in}% [[
adamc@120 675 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
adamc@120 676 JMeq_refl : JMeq x x
adamc@120 677 ]]
adamc@120 678
adam@427 679 The identity [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as a sort of pun 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 680
adamc@120 681 Infix "==" := JMeq (at level 70, no associativity).
adamc@120 682
adam@426 683 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
adamc@124 684 (* begin thide *)
adam@426 685 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == eq_refl x :=
adam@426 686 match pf return (pf == eq_refl _) with
adam@426 687 | eq_refl => JMeq_refl _
adamc@120 688 end.
adamc@124 689 (* end thide *)
adamc@120 690
adamc@120 691 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
adamc@120 692
adamc@271 693 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 694
adamc@120 695 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
adam@426 696 O = match pf with eq_refl => O end.
adamc@124 697 (* begin thide *)
adamc@121 698 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@120 699 Qed.
adamc@124 700 (* end thide *)
adamc@120 701
adamc@120 702 (** 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 703
adamc@120 704 Check JMeq_eq.
adamc@218 705 (** %\vspace{-.15in}% [[
adamc@120 706 JMeq_eq
adamc@120 707 : forall (A : Type) (x y : A), x == y -> x = y
adamc@218 708 ]]
adamc@120 709
adamc@218 710 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 711
adamc@120 712 We can redo our [fhapp] associativity proof based around [JMeq]. *)
adamc@120 713
adamc@120 714 Section fhapp'.
adamc@120 715 Variable A : Type.
adamc@120 716 Variable B : A -> Type.
adamc@120 717
adamc@120 718 (** This time, the naive theorem statement type-checks. *)
adamc@120 719
adamc@124 720 (* EX: Prove [fhapp] associativity using [JMeq]. *)
adamc@124 721
adamc@124 722 (* begin thide *)
adam@364 723 Theorem fhapp_ass' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
adam@364 724 (hls3 : fhlist B ls3),
adamc@120 725 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adamc@120 726 induction ls1; crush.
adamc@120 727
adamc@120 728 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
adamc@120 729 [[
adamc@120 730 ============================
adam@297 731 (a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
adamc@120 732 ]]
adamc@120 733
adam@297 734 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 735 [[
adamc@120 736 rewrite IHls1.
adam@364 737 ]]
adamc@120 738
adam@364 739 <<
adamc@120 740 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
adamc@120 741 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
adam@364 742 >>
adamc@120 743
adam@407 744 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 745
adamc@120 746 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 747
adamc@120 748 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 749
adamc@120 750 generalize (fhapp b (fhapp hls2 hls3))
adamc@120 751 (fhapp (fhapp b hls2) hls3)
adamc@120 752 (IHls1 _ _ b hls2 hls3).
adam@364 753 (** %\vspace{-.15in}%[[
adamc@120 754 ============================
adamc@120 755 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
adamc@120 756 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
adamc@120 757 ]]
adamc@120 758
adamc@120 759 Now we can rewrite with append associativity, as before. *)
adamc@120 760
adamc@120 761 rewrite app_ass.
adam@364 762 (** %\vspace{-.15in}%[[
adamc@120 763 ============================
adamc@120 764 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
adamc@120 765 ]]
adamc@120 766
adamc@120 767 From this point, the goal is trivial. *)
adamc@120 768
adamc@120 769 intros f f0 H; rewrite H; reflexivity.
adamc@120 770 Qed.
adamc@124 771 (* end thide *)
adamc@121 772
adam@385 773 End fhapp'.
adam@385 774
adam@385 775 (** 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 776
adam@385 777 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 778
adam@385 779 Print Assumptions fhapp_ass'.
adam@385 780 (** %\vspace{-.15in}%[[
adam@385 781 Axioms:
adam@385 782 JMeq_eq : forall (A : Type) (x y : A), x == y -> x = y
adam@385 783 ]]
adam@385 784
adam@385 785 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 786
adam@385 787 Lemma pair_cong : forall A1 A2 B1 B2 (x1 : A1) (x2 : A2) (y1 : B1) (y2 : B2),
adam@385 788 x1 == x2
adam@385 789 -> y1 == y2
adam@385 790 -> (x1, y1) == (x2, y2).
adam@385 791 intros until y2; intros Hx Hy; rewrite Hx; rewrite Hy; reflexivity.
adam@385 792 Qed.
adam@385 793
adam@385 794 Hint Resolve pair_cong.
adam@385 795
adam@385 796 Section fhapp''.
adam@385 797 Variable A : Type.
adam@385 798 Variable B : A -> Type.
adam@385 799
adam@385 800 Theorem fhapp_ass'' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
adam@385 801 (hls3 : fhlist B ls3),
adam@385 802 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adam@385 803 induction ls1; crush.
adam@385 804 Qed.
adam@385 805 End fhapp''.
adam@385 806
adam@385 807 Print Assumptions fhapp_ass''.
adam@385 808 (** <<
adam@385 809 Closed under the global context
adam@385 810 >>
adam@385 811
adam@385 812 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 [fhap_ass'], 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 813
adam@385 814 Check eq_ind_r.
adam@385 815 (** %\vspace{-.15in}%[[
adam@385 816 eq_ind_r
adam@385 817 : forall (A : Type) (x : A) (P : A -> Prop),
adam@385 818 P x -> forall y : A, y = x -> P y
adam@385 819 ]]
adam@385 820
adam@398 821 The corresponding lemma used for [JMeq] in the proof of [pair_cong] is %\index{Gallina terms!internal\_JMeq\_rew\_r}%[internal_JMeq_rew_r], which, confusingly, is defined by [rewrite] as needed, so it is not available for checking until after we apply it. *)
adam@385 822
adam@398 823 Check internal_JMeq_rew_r.
adam@385 824 (** %\vspace{-.15in}%[[
adam@398 825 internal_JMeq_rew_r
adam@385 826 : forall (A : Type) (x : A) (B : Type) (b : B)
adam@385 827 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x
adam@385 828 ]]
adam@385 829
adam@398 830 The key difference is that, where the [eq] lemma is parametrized 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 [internal_JMeq_rew_r], 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 naively leads to a type error.
adam@385 831
adam@398 832 When [rewrite] cannot figure out how to apply [internal_JMeq_rew_r] for [x == y] where [x] and [y] have the same type, the tactic can instead use an alternate theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *)
adam@385 833
adam@385 834 Check JMeq_ind_r.
adam@385 835 (** %\vspace{-.15in}%[[
adam@385 836 JMeq_ind_r
adam@385 837 : forall (A : Type) (x : A) (P : A -> Prop),
adam@385 838 P x -> forall y : A, y == x -> P y
adam@385 839 ]]
adam@385 840
adam@398 841 Ironically, where in the proof of [fhapp_ass'] we used [rewrite app_ass] 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 [internal_JMeq_rew_r]!
adam@385 842
adam@385 843 For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *)
adam@385 844
adam@385 845 Theorem out_of_luck : forall n m : nat,
adam@385 846 n == m
adam@385 847 -> S n == S m.
adam@385 848 intros n m H.
adam@385 849
adam@385 850 (** 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. *)
adam@385 851
adam@385 852 pattern n.
adam@385 853 (** %\vspace{-.15in}%[[
adam@385 854 n : nat
adam@385 855 m : nat
adam@385 856 H : n == m
adam@385 857 ============================
adam@385 858 (fun n0 : nat => S n0 == S m) n
adam@385 859 ]]
adam@385 860 *)
adam@385 861 apply JMeq_ind_r with (x := m); auto.
adam@385 862
adam@398 863 (** However, we run into trouble trying to get the goal into a form compatible with [internal_JMeq_rew_r.] *)
adam@427 864
adam@385 865 Undo 2.
adam@385 866 (** %\vspace{-.15in}%[[
adam@385 867 pattern nat, n.
adam@385 868 ]]
adam@385 869 <<
adam@385 870 Error: The abstracted term "fun (P : Set) (n0 : P) => S n0 == S m"
adam@385 871 is not well typed.
adam@385 872 Illegal application (Type Error):
adam@385 873 The term "S" of type "nat -> nat"
adam@385 874 cannot be applied to the term
adam@385 875 "n0" : "P"
adam@385 876 This term has type "P" which should be coercible to
adam@385 877 "nat".
adam@385 878 >>
adam@385 879
adam@385 880 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 881
adam@385 882 Abort.
adam@385 883
adam@427 884 (** Why did we not run into this problem in our proof of [fhapp_ass'']? 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 885
adamc@121 886
adamc@121 887 (** * Equivalence of Equality Axioms *)
adamc@121 888
adamc@124 889 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
adamc@124 890
adamc@124 891 (* begin thide *)
adamc@272 892 (** 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 of the previous two sections' approaches reduces to the other logically.
adamc@121 893
adamc@121 894 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 895
adam@426 896 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = eq_refl x.
adamc@121 897 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@121 898 Qed.
adamc@121 899
adamc@121 900 (** 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 901
adamc@121 902 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
adam@426 903 exists pf : B = A, x = match pf with eq_refl => y end.
adamc@121 904
adamc@121 905 Infix "===" := JMeq' (at level 70, no associativity).
adamc@121 906
adam@427 907 (** remove printing exists *)
adam@427 908
adamc@121 909 (** 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 910
adamc@121 911 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
adamc@121 912
adamc@121 913 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
adam@426 914 intros; unfold JMeq'; exists (eq_refl A); reflexivity.
adamc@121 915 Qed.
adamc@121 916
adamc@121 917 (** printing exists $\exists$ *)
adamc@121 918
adamc@121 919 (** 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 920
adamc@121 921 Theorem JMeq_eq' : forall (A : Type) (x y : A),
adamc@121 922 x === y -> x = y.
adamc@121 923 unfold JMeq'; intros.
adamc@121 924 (** [[
adamc@121 925 H : exists pf : A = A,
adamc@121 926 x = match pf in (_ = T) return T with
adam@426 927 | eq_refl => y
adamc@121 928 end
adamc@121 929 ============================
adamc@121 930 x = y
adam@302 931 ]]
adam@302 932 *)
adamc@121 933
adamc@121 934 destruct H.
adamc@121 935 (** [[
adamc@121 936 x0 : A = A
adamc@121 937 H : x = match x0 in (_ = T) return T with
adam@426 938 | eq_refl => y
adamc@121 939 end
adamc@121 940 ============================
adamc@121 941 x = y
adam@302 942 ]]
adam@302 943 *)
adamc@121 944
adamc@121 945 rewrite H.
adamc@121 946 (** [[
adamc@121 947 x0 : A = A
adamc@121 948 ============================
adamc@121 949 match x0 in (_ = T) return T with
adam@426 950 | eq_refl => y
adamc@121 951 end = y
adam@302 952 ]]
adam@302 953 *)
adamc@121 954
adamc@121 955 rewrite (UIP_refl _ _ x0); reflexivity.
adamc@121 956 Qed.
adamc@121 957
adam@427 958 (** 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 959
adamc@124 960 (* end thide *)
adamc@123 961
adamc@123 962
adamc@123 963 (** * Equality of Functions *)
adamc@123 964
adamc@123 965 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
adam@407 966 Theorem two_identities : (fun n => n) = (fun n => n + 0).
adamc@205 967 ]]
adamc@205 968
adam@407 969 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 970
adam@407 971 Require Import FunctionalExtensionality.
adam@407 972 About functional_extensionality.
adam@407 973 (** %\vspace{-.15in}%[[
adam@407 974 functional_extensionality :
adam@407 975 forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g
adam@407 976 ]]
adam@407 977 *)
adamc@123 978
adamc@123 979 (** This axiom has been verified metatheoretically to be consistent with CIC and the two equality axioms we considered previously. With it, the proof of [S_eta] is trivial. *)
adamc@123 980
adam@407 981 Theorem two_identities : (fun n => n) = (fun n => n + 0).
adamc@124 982 (* begin thide *)
adam@407 983 apply functional_extensionality; crush.
adamc@123 984 Qed.
adamc@124 985 (* end thide *)
adamc@123 986
adam@427 987 (** The same axiom can help us prove equality of types, where we need to "reason under quantifiers." *)
adamc@123 988
adamc@123 989 Theorem forall_eq : (forall x : nat, match x with
adamc@123 990 | O => True
adamc@123 991 | S _ => True
adamc@123 992 end)
adamc@123 993 = (forall _ : nat, True).
adamc@123 994
adam@364 995 (** There are no immediate opportunities to apply [ext_eq], but we can use %\index{tactics!change}%[change] to fix that. *)
adamc@123 996
adamc@124 997 (* begin thide *)
adamc@123 998 change ((forall x : nat, (fun x => match x with
adamc@123 999 | 0 => True
adamc@123 1000 | S _ => True
adamc@123 1001 end) x) = (nat -> True)).
adam@407 1002 rewrite (functional_extensionality (fun x => match x with
adam@407 1003 | 0 => True
adam@407 1004 | S _ => True
adam@407 1005 end) (fun _ => True)).
adamc@123 1006 (** [[
adamc@123 1007 2 subgoals
adamc@123 1008
adamc@123 1009 ============================
adamc@123 1010 (nat -> True) = (nat -> True)
adamc@123 1011
adamc@123 1012 subgoal 2 is:
adamc@123 1013 forall x : nat, match x with
adamc@123 1014 | 0 => True
adamc@123 1015 | S _ => True
adamc@123 1016 end = True
adam@302 1017 ]]
adam@302 1018 *)
adamc@123 1019
adamc@123 1020 reflexivity.
adamc@123 1021
adamc@123 1022 destruct x; constructor.
adamc@123 1023 Qed.
adamc@124 1024 (* end thide *)
adamc@127 1025
adam@407 1026 (** 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. *)