Mercurial > cpdt > repo

annotate src/Equality.v @ 366:03e200599633

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove home page reference to Part IV
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 Nov 2011 16:54:40 -0500
parents 990151eac6af
children b809d3a8a5b1
rev   line source
adam@297 1 (* Copyright (c) 2008-2011, 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@364 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}\textit{%#<i>#definitional equality#</i>#%}%. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal.
adamc@122 27
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@365 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 %\emph{%#<i>#the top-level structure of the recursive argument is known#</i>#%}%. 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@365 146 The outer application of the [fix] expression for [addList] 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@365 148 The opposite behavior pertains to a version of [addList] 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@365 156 Eval compute in fun ls => addLists' ls nil.
adam@365 157 (** %\vspace{-.15in}%[[
adam@365 158 = fun ls : list nat => match ls with
adam@365 159 | nil => nil
adam@365 160 | _ :: _ => nil
adam@365 161 end
adam@365 162 ]]
adam@365 163
adam@365 164 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 165
adam@365 166 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 167
adam@365 168 %\medskip%
adam@365 169
adam@365 170 The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a %\index{propositional equality}\textit{%#<i>#propositional equality#</i>#%}%, because it reifies definitional equality as a proposition that may or may not hold. Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity. In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina. We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use.
adamc@122 171
adam@294 172 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 173
adamc@122 174
adamc@118 175 (** * Heterogeneous Lists Revisited *)
adamc@118 176
adam@292 177 (** 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 [member] types. *)
adamc@118 178
adamc@118 179 Section fhlist.
adamc@118 180 Variable A : Type.
adamc@118 181 Variable B : A -> Type.
adamc@118 182
adamc@118 183 Fixpoint fhlist (ls : list A) : Type :=
adamc@118 184 match ls with
adamc@118 185 | nil => unit
adamc@118 186 | x :: ls' => B x * fhlist ls'
adamc@118 187 end%type.
adamc@118 188
adamc@118 189 Variable elm : A.
adamc@118 190
adamc@118 191 Fixpoint fmember (ls : list A) : Type :=
adamc@118 192 match ls with
adamc@118 193 | nil => Empty_set
adamc@118 194 | x :: ls' => (x = elm) + fmember ls'
adamc@118 195 end%type.
adamc@118 196
adamc@118 197 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@118 198 match ls return fhlist ls -> fmember ls -> B elm with
adamc@118 199 | nil => fun _ idx => match idx with end
adamc@118 200 | _ :: ls' => fun mls idx =>
adamc@118 201 match idx with
adamc@118 202 | inl pf => match pf with
adamc@118 203 | refl_equal => fst mls
adamc@118 204 end
adamc@118 205 | inr idx' => fhget ls' (snd mls) idx'
adamc@118 206 end
adamc@118 207 end.
adamc@118 208 End fhlist.
adamc@118 209
adamc@118 210 Implicit Arguments fhget [A B elm ls].
adamc@118 211
adamc@118 212 (** We can define a [map]-like function for [fhlist]s. *)
adamc@118 213
adamc@118 214 Section fhlist_map.
adamc@118 215 Variables A : Type.
adamc@118 216 Variables B C : A -> Type.
adamc@118 217 Variable f : forall x, B x -> C x.
adamc@118 218
adamc@118 219 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
adamc@118 220 match ls return fhlist B ls -> fhlist C ls with
adamc@118 221 | nil => fun _ => tt
adamc@118 222 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
adamc@118 223 end.
adamc@118 224
adamc@118 225 Implicit Arguments fhmap [ls].
adamc@118 226
adamc@118 227 (** 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 228
adamc@118 229 Variable elm : A.
adamc@118 230
adamc@118 231 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
adamc@118 232 fhget (fhmap hls) mem = f (fhget hls mem).
adam@298 233 (* begin hide *)
adam@298 234 induction ls; crush; case a0; reflexivity.
adam@298 235 (* end hide *)
adam@364 236 (** %\vspace{-.2in}%[[
adamc@118 237 induction ls; crush.
adam@298 238 ]]
adamc@118 239
adam@364 240 %\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 241
adam@297 242 Part of our single remaining subgoal is:
adamc@118 243 [[
adamc@118 244 a0 : a = elm
adamc@118 245 ============================
adamc@118 246 match a0 in (_ = a2) return (C a2) with
adamc@118 247 | refl_equal => f a1
adamc@118 248 end = f match a0 in (_ = a2) return (B a2) with
adamc@118 249 | refl_equal => a1
adamc@118 250 end
adamc@118 251 ]]
adamc@118 252
adamc@118 253 This seems like a trivial enough obligation. The equality proof [a0] must be [refl_equal], since that is the only constructor of [eq]. Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
adamc@118 254 [[
adamc@118 255 destruct a0.
adamc@118 256 ]]
adamc@118 257
adam@364 258 <<
adam@364 259 User error: Cannot solve a second-order unification problem
adam@364 260 >>
adam@364 261
adamc@118 262 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 263 [[
adamc@118 264 assert (a0 = refl_equal _).
adam@364 265 ]]
adamc@118 266
adam@364 267 <<
adamc@118 268 The term "refl_equal ?98" has type "?98 = ?98"
adamc@118 269 while it is expected to have type "a = elm"
adam@364 270 >>
adamc@118 271
adamc@118 272 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 273
adam@292 274 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 275
adam@297 276 For this particular example, the solution is surprisingly straightforward. [destruct] has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments.
adam@297 277 [[
adamc@118 278 case a0.
adam@297 279
adamc@118 280 ============================
adamc@118 281 f a1 = f a1
adamc@118 282 ]]
adamc@118 283
adam@297 284 It seems that [destruct] was trying to be too smart for its own good.
adam@297 285 [[
adamc@118 286 reflexivity.
adam@302 287 ]]
adam@364 288 %\vspace{-.2in}% *)
adamc@118 289 Qed.
adamc@124 290 (* end thide *)
adamc@118 291
adamc@118 292 (** 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 293
adamc@118 294 Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
adamc@124 295 (* begin thide *)
adamc@118 296 simple destruct pf; reflexivity.
adamc@118 297 Qed.
adamc@124 298 (* end thide *)
adamc@118 299
adam@364 300 (** 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 301
adamc@118 302 Print lemma1.
adamc@218 303 (** %\vspace{-.15in}% [[
adamc@118 304 lemma1 =
adamc@118 305 fun (x : A) (pf : x = elm) =>
adamc@118 306 match pf as e in (_ = y) return (0 = match e with
adamc@118 307 | refl_equal => 0
adamc@118 308 end) with
adamc@118 309 | refl_equal => refl_equal 0
adamc@118 310 end
adamc@118 311 : forall (x : A) (pf : x = elm), 0 = match pf with
adamc@118 312 | refl_equal => 0
adamc@118 313 end
adamc@218 314
adamc@118 315 ]]
adamc@118 316
adamc@118 317 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
adamc@118 318
adamc@124 319 (* begin thide *)
adamc@118 320 Definition lemma1' :=
adamc@118 321 fun (x : A) (pf : x = elm) =>
adamc@118 322 match pf return (0 = match pf with
adamc@118 323 | refl_equal => 0
adamc@118 324 end) with
adamc@118 325 | refl_equal => refl_equal 0
adamc@118 326 end.
adamc@124 327 (* end thide *)
adamc@118 328
adamc@118 329 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)
adamc@118 330
adamc@118 331 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
adamc@124 332 (* begin thide *)
adam@364 333 (** %\vspace{-.25in}%[[
adamc@118 334 simple destruct pf.
adam@364 335 ]]
adamc@205 336
adam@364 337 <<
adamc@118 338 User error: Cannot solve a second-order unification problem
adam@364 339 >>
adam@302 340 *)
adamc@118 341 Abort.
adamc@118 342
adamc@118 343 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
adamc@118 344
adamc@124 345 (* begin thide *)
adamc@124 346 Definition lemma2 :=
adamc@118 347 fun (x : A) (pf : x = x) =>
adamc@118 348 match pf return (0 = match pf with
adamc@118 349 | refl_equal => 0
adamc@118 350 end) with
adamc@118 351 | refl_equal => refl_equal 0
adamc@118 352 end.
adamc@124 353 (* end thide *)
adamc@118 354
adamc@118 355 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
adamc@118 356
adamc@118 357 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@124 358 (* begin thide *)
adam@364 359 (** %\vspace{-.25in}%[[
adamc@118 360 simple destruct pf.
adam@364 361 ]]
adamc@205 362
adam@364 363 <<
adamc@118 364 User error: Cannot solve a second-order unification problem
adam@364 365 >>
adam@364 366 %\vspace{-.15in}%*)
adamc@218 367
adamc@118 368 Abort.
adamc@118 369
adamc@118 370 (** This time, even our manual attempt fails.
adamc@118 371 [[
adamc@118 372 Definition lemma3' :=
adamc@118 373 fun (x : A) (pf : x = x) =>
adamc@118 374 match pf as pf' in (_ = x') return (pf' = refl_equal x') with
adamc@118 375 | refl_equal => refl_equal _
adamc@118 376 end.
adam@364 377 ]]
adamc@118 378
adam@364 379 <<
adamc@118 380 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
adamc@118 381 "x = x'"
adam@364 382 >>
adamc@118 383
adam@296 384 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 %\textit{%#<i>#must#</i>#%}% choose a fresh name for the second argument of [eq]. We are just as constrained to use the %``%#"#real#"#%''% value [x] for the first argument. Thus, within the [return] clause, the proof we are matching on %\textit{%#<i>#must#</i>#%}% equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
adamc@118 385
adamc@118 386 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)
adamc@118 387
adamc@118 388 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@118 389 intros; apply UIP_refl.
adamc@118 390 Qed.
adamc@118 391
adamc@118 392 Check UIP_refl.
adamc@218 393 (** %\vspace{-.15in}% [[
adamc@118 394 UIP_refl
adamc@118 395 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
adamc@118 396 ]]
adamc@118 397
adam@364 398 The theorem %\index{Gallina terms!UIF\_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 %\textit{%#<i>#axiom#</i>#%}%. *)
adamc@118 399
adamc@118 400 Print eq_rect_eq.
adamc@218 401 (** %\vspace{-.15in}% [[
adamc@118 402 eq_rect_eq =
adamc@118 403 fun U : Type => Eq_rect_eq.eq_rect_eq U
adamc@118 404 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@118 405 x = eq_rect p Q x p h
adamc@118 406 ]]
adamc@118 407
adam@364 408 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). *)
adamc@118 409
adam@364 410 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@364 411 x = eq_rect p Q x p h).
adam@364 412 (** %\vspace{-.15in}%[[
adam@364 413 = forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@364 414 x = match h in (_ = y) return (Q y) with
adam@364 415 | eq_refl => x
adam@364 416 end
adam@364 417 ]]
adam@364 418
adam@364 419 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an %\index{axiom}%axiom; that is, a proposition asserted as true without proof. We cannot assert just any statement without proof. Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant. In general, we need to be sure that we never assert %\textit{%#<i>#inconsistent#</i>#%}% sets of axioms. A set of axioms is inconsistent if its conjunction implies [False]. For the case of [eq_rect_eq], consistency has been verified outside of Coq via %``%#"#informal#"#%''% metatheory%~\cite{AxiomK}%, in a study that also established unprovability of the axiom in CIC.
adamc@118 420
adamc@118 421 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
adamc@118 422
adamc@118 423 Print Streicher_K.
adamc@124 424 (* end thide *)
adamc@218 425 (** %\vspace{-.15in}% [[
adamc@118 426 Streicher_K =
adamc@118 427 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
adamc@118 428 : forall (U : Type) (x : U) (P : x = x -> Prop),
adamc@118 429 P (refl_equal x) -> forall p : x = x, P p
adamc@118 430 ]]
adamc@118 431
adam@364 432 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 433
adamc@118 434 End fhlist_map.
adamc@118 435
adam@364 436 (** 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 437
adamc@119 438
adamc@119 439 (** * Type-Casts in Theorem Statements *)
adamc@119 440
adamc@119 441 (** 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 442
adamc@119 443 Section fhapp.
adamc@119 444 Variable A : Type.
adamc@119 445 Variable B : A -> Type.
adamc@119 446
adamc@218 447 Fixpoint fhapp (ls1 ls2 : list A)
adamc@119 448 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
adamc@218 449 match ls1 with
adamc@119 450 | nil => fun _ hls2 => hls2
adamc@119 451 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
adamc@119 452 end.
adamc@119 453
adamc@119 454 Implicit Arguments fhapp [ls1 ls2].
adamc@119 455
adamc@124 456 (* EX: Prove that fhapp is associative. *)
adamc@124 457 (* begin thide *)
adamc@124 458
adamc@119 459 (** We might like to prove that [fhapp] is associative.
adamc@119 460 [[
adamc@119 461 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 462 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 463 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
adam@364 464 ]]
adamc@119 465
adam@364 466 <<
adamc@119 467 The term
adamc@119 468 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
adamc@119 469 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
adamc@119 470 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
adam@364 471 >>
adamc@119 472
adam@364 473 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}\textit{%#<i>#intensional#</i>#%}%, in the sense that type equality theorems can never be applied after the fact to get a term to type-check. Instead, we need to make use of equality explicitly in the theorem statement. *)
adamc@119 474
adamc@119 475 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 476 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
adamc@119 477 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 478 fhapp hls1 (fhapp hls2 hls3)
adamc@119 479 = match pf in (_ = ls) return fhlist _ ls with
adamc@119 480 | refl_equal => fhapp (fhapp hls1 hls2) hls3
adamc@119 481 end.
adamc@119 482 induction ls1; crush.
adamc@119 483
adamc@119 484 (** The first remaining subgoal looks trivial enough:
adamc@119 485 [[
adamc@119 486 ============================
adamc@119 487 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 488 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 489 | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 490 end
adamc@119 491 ]]
adamc@119 492
adamc@119 493 We can try what worked in previous examples.
adamc@119 494 [[
adamc@119 495 case pf.
adam@364 496 ]]
adamc@119 497
adam@364 498 <<
adamc@119 499 User error: Cannot solve a second-order unification problem
adam@364 500 >>
adamc@119 501
adamc@119 502 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 503
adamc@119 504 rewrite (UIP_refl _ _ pf).
adamc@119 505 (** [[
adamc@119 506 ============================
adamc@119 507 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 508 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adam@302 509 ]]
adam@302 510 *)
adamc@119 511
adamc@119 512 reflexivity.
adamc@119 513
adamc@119 514 (** Our second subgoal is trickier.
adamc@119 515 [[
adamc@119 516 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 517 ============================
adamc@119 518 (a0,
adamc@119 519 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 520 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 521 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 522 | refl_equal =>
adamc@119 523 (a0,
adamc@119 524 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 525 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 526 end
adamc@119 527
adamc@119 528 rewrite (UIP_refl _ _ pf).
adam@364 529 ]]
adamc@119 530
adam@364 531 <<
adamc@119 532 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
adamc@119 533 while it is expected to have type "?556 = ?556"
adam@364 534 >>
adamc@119 535
adamc@119 536 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 537
adamc@119 538 injection pf; intro pf'.
adamc@119 539 (** [[
adamc@119 540 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 541 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
adamc@119 542 ============================
adamc@119 543 (a0,
adamc@119 544 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 545 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 546 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 547 | refl_equal =>
adamc@119 548 (a0,
adamc@119 549 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 550 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 551 end
adamc@119 552 ]]
adamc@119 553
adamc@119 554 Now we can rewrite using the inductive hypothesis. *)
adamc@119 555
adamc@119 556 rewrite (IHls1 _ _ pf').
adamc@119 557 (** [[
adamc@119 558 ============================
adamc@119 559 (a0,
adamc@119 560 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 561 | refl_equal =>
adamc@119 562 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 563 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
adamc@119 564 end) =
adamc@119 565 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 566 | refl_equal =>
adamc@119 567 (a0,
adamc@119 568 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 569 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 570 end
adamc@119 571 ]]
adamc@119 572
adam@364 573 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 %\textit{%#<i>#does not matter what the result of the call is#</i>#%}%. In other words, the subgoal should remain true if we replace this [fhapp] call with a fresh variable. The %\index{tactics!generalize}%[generalize] tactic helps us do exactly that. *)
adamc@119 574
adamc@119 575 generalize (fhapp (fhapp b hls2) hls3).
adamc@119 576 (** [[
adamc@119 577 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
adamc@119 578 (a0,
adamc@119 579 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 580 | refl_equal => f
adamc@119 581 end) =
adamc@119 582 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 583 | refl_equal => (a0, f)
adamc@119 584 end
adamc@119 585 ]]
adamc@119 586
adamc@119 587 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 588
adamc@119 589 In this case, it is helpful to generalize over our two proofs as well. *)
adamc@119 590
adamc@119 591 generalize pf pf'.
adamc@119 592 (** [[
adamc@119 593 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 594 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 595 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
adamc@119 596 (a0,
adamc@119 597 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 598 | refl_equal => f
adamc@119 599 end) =
adamc@119 600 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 601 | refl_equal => (a0, f)
adamc@119 602 end
adamc@119 603 ]]
adamc@119 604
adamc@119 605 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 606
adamc@119 607 However, now that we have generalized over the [fhapp] call, the type of the term being type-cast appears explicitly in the goal and %\textit{%#<i>#may be rewritten as well#</i>#%}%. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append. *)
adamc@119 608
adamc@119 609 rewrite app_ass.
adamc@119 610 (** [[
adamc@119 611 ============================
adamc@119 612 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 613 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 614 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
adamc@119 615 (a0,
adamc@119 616 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 617 | refl_equal => f
adamc@119 618 end) =
adamc@119 619 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 620 | refl_equal => (a0, f)
adamc@119 621 end
adamc@119 622 ]]
adamc@119 623
adamc@119 624 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 625
adamc@119 626 intros.
adamc@119 627 rewrite (UIP_refl _ _ pf0).
adamc@119 628 rewrite (UIP_refl _ _ pf'0).
adamc@119 629 reflexivity.
adamc@119 630 Qed.
adamc@124 631 (* end thide *)
adamc@119 632 End fhapp.
adamc@120 633
adamc@120 634 Implicit Arguments fhapp [A B ls1 ls2].
adamc@120 635
adam@364 636 (** 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 637
adamc@120 638
adamc@120 639 (** * Heterogeneous Equality *)
adamc@120 640
adam@364 641 (** There is another equality predicate, defined in the %\index{Gallina terms!JMeq}%[JMeq] module of the standard library, implementing %\index{heterogeneous equality}\textit{%#<i>#heterogeneous equality#</i>#%}%. *)
adamc@120 642
adamc@120 643 Print JMeq.
adamc@218 644 (** %\vspace{-.15in}% [[
adamc@120 645 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
adamc@120 646 JMeq_refl : JMeq x x
adamc@120 647 ]]
adamc@120 648
adam@364 649 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. [JMeq] starts out looking a lot like [eq]. The crucial difference is that we may use [JMeq] %\textit{%#<i>#on arguments of different types#</i>#%}%. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *)
adamc@120 650
adamc@120 651 Infix "==" := JMeq (at level 70, no associativity).
adamc@120 652
adamc@124 653 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
adamc@124 654 (* begin thide *)
adamc@121 655 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
adamc@120 656 match pf return (pf == refl_equal _) with
adamc@120 657 | refl_equal => JMeq_refl _
adamc@120 658 end.
adamc@124 659 (* end thide *)
adamc@120 660
adamc@120 661 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
adamc@120 662
adamc@271 663 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 664
adamc@120 665 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
adamc@120 666 O = match pf with refl_equal => O end.
adamc@124 667 (* begin thide *)
adamc@121 668 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@120 669 Qed.
adamc@124 670 (* end thide *)
adamc@120 671
adamc@120 672 (** 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 673
adamc@120 674 Check JMeq_eq.
adamc@218 675 (** %\vspace{-.15in}% [[
adamc@120 676 JMeq_eq
adamc@120 677 : forall (A : Type) (x y : A), x == y -> x = y
adamc@218 678 ]]
adamc@120 679
adamc@218 680 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 681
adamc@120 682 We can redo our [fhapp] associativity proof based around [JMeq]. *)
adamc@120 683
adamc@120 684 Section fhapp'.
adamc@120 685 Variable A : Type.
adamc@120 686 Variable B : A -> Type.
adamc@120 687
adamc@120 688 (** This time, the naive theorem statement type-checks. *)
adamc@120 689
adamc@124 690 (* EX: Prove [fhapp] associativity using [JMeq]. *)
adamc@124 691
adamc@124 692 (* begin thide *)
adam@364 693 Theorem fhapp_ass' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
adam@364 694 (hls3 : fhlist B ls3),
adamc@120 695 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adamc@120 696 induction ls1; crush.
adamc@120 697
adamc@120 698 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
adamc@120 699 [[
adamc@120 700 ============================
adam@297 701 (a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
adamc@120 702 ]]
adamc@120 703
adam@297 704 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 705 [[
adamc@120 706 rewrite IHls1.
adam@364 707 ]]
adamc@120 708
adam@364 709 <<
adamc@120 710 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
adamc@120 711 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
adam@364 712 >>
adamc@120 713
adam@297 714 Coq 8.3 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 715
adamc@120 716 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 717
adamc@120 718 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 719
adamc@120 720 generalize (fhapp b (fhapp hls2 hls3))
adamc@120 721 (fhapp (fhapp b hls2) hls3)
adamc@120 722 (IHls1 _ _ b hls2 hls3).
adam@364 723 (** %\vspace{-.15in}%[[
adamc@120 724 ============================
adamc@120 725 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
adamc@120 726 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
adamc@120 727 ]]
adamc@120 728
adamc@120 729 Now we can rewrite with append associativity, as before. *)
adamc@120 730
adamc@120 731 rewrite app_ass.
adam@364 732 (** %\vspace{-.15in}%[[
adamc@120 733 ============================
adamc@120 734 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
adamc@120 735 ]]
adamc@120 736
adamc@120 737 From this point, the goal is trivial. *)
adamc@120 738
adamc@120 739 intros f f0 H; rewrite H; reflexivity.
adamc@120 740 Qed.
adamc@124 741 (* end thide *)
adamc@120 742 End fhapp'.
adamc@121 743
adam@364 744 (** 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@364 745
adamc@121 746
adamc@121 747 (** * Equivalence of Equality Axioms *)
adamc@121 748
adamc@124 749 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
adamc@124 750
adamc@124 751 (* begin thide *)
adamc@272 752 (** 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 753
adamc@121 754 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 755
adamc@121 756 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
adamc@121 757 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@121 758 Qed.
adamc@121 759
adamc@121 760 (** 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 761
adamc@121 762 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
adamc@121 763 exists pf : B = A, x = match pf with refl_equal => y end.
adamc@121 764
adamc@121 765 Infix "===" := JMeq' (at level 70, no associativity).
adamc@121 766
adamc@121 767 (** 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 768
adamc@121 769 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
adamc@121 770
adamc@121 771 (** remove printing exists *)
adamc@121 772 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
adamc@121 773 intros; unfold JMeq'; exists (refl_equal A); reflexivity.
adamc@121 774 Qed.
adamc@121 775
adamc@121 776 (** printing exists $\exists$ *)
adamc@121 777
adamc@121 778 (** 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 779
adamc@121 780 Theorem JMeq_eq' : forall (A : Type) (x y : A),
adamc@121 781 x === y -> x = y.
adamc@121 782 unfold JMeq'; intros.
adamc@121 783 (** [[
adamc@121 784 H : exists pf : A = A,
adamc@121 785 x = match pf in (_ = T) return T with
adamc@121 786 | refl_equal => y
adamc@121 787 end
adamc@121 788 ============================
adamc@121 789 x = y
adam@302 790 ]]
adam@302 791 *)
adamc@121 792
adamc@121 793 destruct H.
adamc@121 794 (** [[
adamc@121 795 x0 : A = A
adamc@121 796 H : x = match x0 in (_ = T) return T with
adamc@121 797 | refl_equal => y
adamc@121 798 end
adamc@121 799 ============================
adamc@121 800 x = y
adam@302 801 ]]
adam@302 802 *)
adamc@121 803
adamc@121 804 rewrite H.
adamc@121 805 (** [[
adamc@121 806 x0 : A = A
adamc@121 807 ============================
adamc@121 808 match x0 in (_ = T) return T with
adamc@121 809 | refl_equal => y
adamc@121 810 end = y
adam@302 811 ]]
adam@302 812 *)
adamc@121 813
adamc@121 814 rewrite (UIP_refl _ _ x0); reflexivity.
adamc@121 815 Qed.
adamc@121 816
adam@364 817 (** 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 818
adamc@124 819 (* end thide *)
adamc@123 820
adamc@123 821
adamc@123 822 (** * Equality of Functions *)
adamc@123 823
adamc@123 824 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
adamc@123 825 Theorem S_eta : S = (fun n => S n).
adamc@205 826 ]]
adamc@205 827
adam@364 828 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}\textit{%#<i>#extensional#</i>#%}%. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We %\textit{%#<i>#can#</i>#%}% assert function extensionality as an axiom. *)
adamc@123 829
adamc@124 830 (* begin thide *)
adamc@123 831 Axiom ext_eq : forall A B (f g : A -> B),
adamc@123 832 (forall x, f x = g x)
adamc@123 833 -> f = g.
adamc@124 834 (* end thide *)
adamc@123 835
adamc@123 836 (** 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 837
adamc@123 838 Theorem S_eta : S = (fun n => S n).
adamc@124 839 (* begin thide *)
adamc@123 840 apply ext_eq; reflexivity.
adamc@123 841 Qed.
adamc@124 842 (* end thide *)
adamc@123 843
adam@292 844 (** The same axiom can help us prove equality of types, where we need to %``%#"#reason under quantifiers.#"#%''% *)
adamc@123 845
adamc@123 846 Theorem forall_eq : (forall x : nat, match x with
adamc@123 847 | O => True
adamc@123 848 | S _ => True
adamc@123 849 end)
adamc@123 850 = (forall _ : nat, True).
adamc@123 851
adam@364 852 (** There are no immediate opportunities to apply [ext_eq], but we can use %\index{tactics!change}%[change] to fix that. *)
adamc@123 853
adamc@124 854 (* begin thide *)
adamc@123 855 change ((forall x : nat, (fun x => match x with
adamc@123 856 | 0 => True
adamc@123 857 | S _ => True
adamc@123 858 end) x) = (nat -> True)).
adamc@123 859 rewrite (ext_eq (fun x => match x with
adamc@123 860 | 0 => True
adamc@123 861 | S _ => True
adamc@123 862 end) (fun _ => True)).
adamc@123 863 (** [[
adamc@123 864 2 subgoals
adamc@123 865
adamc@123 866 ============================
adamc@123 867 (nat -> True) = (nat -> True)
adamc@123 868
adamc@123 869 subgoal 2 is:
adamc@123 870 forall x : nat, match x with
adamc@123 871 | 0 => True
adamc@123 872 | S _ => True
adamc@123 873 end = True
adam@302 874 ]]
adam@302 875 *)
adamc@123 876
adamc@123 877 reflexivity.
adamc@123 878
adamc@123 879 destruct x; constructor.
adamc@123 880 Qed.
adamc@124 881 (* end thide *)
adamc@127 882
adam@364 883 (** Unlike in the case of [eq_rect_eq], we have no way of deriving this axiom of %\index{functional extensionality}\emph{%#<i>#functional extensionality#</i>#%}% 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. *)
adam@364 884
adamc@127 885
adamc@127 886 (** * Exercises *)
adamc@127 887
adamc@127 888 (** %\begin{enumerate}%#<ol>#
adamc@127 889
adam@364 890 %\item%#<li># Implement and prove correct a substitution function for simply typed lambda calculus. In particular:
adamc@127 891 %\begin{enumerate}%#<ol>#
adamc@127 892 %\item%#<li># Define a datatype [type] of lambda types, including just booleans and function types.#</li>#
adamc@127 893 %\item%#<li># Define a type family [exp : list type -> type -> Type] of lambda expressions, including boolean constants, variables, and function application and abstraction.#</li>#
adamc@127 894 %\item%#<li># Implement a definitional interpreter for [exp]s, by way of a recursive function over expressions and substitutions for free variables, like in the related example from the last chapter.#</li>#
adam@292 895 %\item%#<li># Implement a function [subst : forall t' ts t, exp (t' :: ts) t -> exp ts t' -> exp ts t]. The type of the first expression indicates that its most recently bound free variable has type [t']. The second expression also has type [t'], and the job of [subst] is to substitute the second expression for every occurrence of the %``%#"#first#"#%''% variable of the first expression.#</li>#
adamc@127 896 %\item%#<li># Prove that [subst] preserves program meanings. That is, prove
adamc@127 897 [[
adamc@127 898 forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts),
adamc@127 899 expDenote (subst e e') s = expDenote e (expDenote e' s ::: s)
adamc@127 900 ]]
adam@292 901 where [:::] is an infix operator for heterogeneous %``%#"#cons#"#%''% that is defined in the book's [DepList] module.#</li>#
adamc@127 902 #</ol>#%\end{enumerate}%
adamc@127 903 The material presented up to this point should be sufficient to enable a good solution of this exercise, with enough ingenuity. If you get stuck, it may be helpful to use the following structure. None of these elements need to appear in your solution, but we can at least guarantee that there is a reasonable solution based on them.
adamc@127 904 %\begin{enumerate}%#<ol>#
adamc@127 905 %\item%#<li># The [DepList] module will be useful. You can get the standard dependent list definitions there, instead of copying-and-pasting from the last chapter. It is worth reading the source for that module over, since it defines some new helpful functions and notations that we did not use last chapter.#</li>#
adam@292 906 %\item%#<li># Define a recursive function [liftVar : forall ts1 ts2 t t', member t (ts1 ++ ts2) -> member t (ts1 ++ t' :: ts2)]. This function should %``%#"#lift#"#%''% a de Bruijn variable so that its type refers to a new variable inserted somewhere in the index list.#</li>#
adam@292 907 %\item%#<li># Define a recursive function [lift' : forall ts t (e : exp ts t) ts1 ts2 t', ts = ts1 ++ ts2 -> exp (ts1 ++ t' :: ts2) t] which performs a similar lifting on an [exp]. The convoluted type is to get around restrictions on [match] annotations. We delay %``%#"#realizing#"#%''% that the first index of [e] is built with list concatenation until after a dependent [match], and the new explicit proof argument must be used to cast some terms that come up in the [match] body.#</li>#
adamc@127 908 %\item%#<li># Define a function [lift : forall ts t t', exp ts t -> exp (t' :: ts) t], which handles simpler top-level lifts. This should be an easy one-liner based on [lift'].#</li>#
adamc@127 909 %\item%#<li># Define a recursive function [substVar : forall ts1 ts2 t t', member t (ts1 ++ t' :: ts2) -> (t' = t) + member t (ts1 ++ ts2)]. This function is the workhorse behind substitution applied to a variable. It returns [inl] to indicate that the variable we pass to it is the variable that we are substituting for, and it returns [inr] to indicate that the variable we are examining is %\textit{%#<i>#not#</i>#%}% the one we are substituting for. In the first case, we get a proof that the necessary typing relationship holds, and, in the second case, we get the original variable modified to reflect the removal of the substitutee from the typing context.#</li>#
adamc@127 910 %\item%#<li># Define a recursive function [subst' : forall ts t (e : exp ts t) ts1 t' ts2, ts = ts1 ++ t' :: ts2 -> exp (ts1 ++ ts2) t' -> exp (ts1 ++ ts2) t]. This is the workhorse of substitution in expressions, employing the same proof-passing trick as for [lift']. You will probably want to use [lift] somewhere in the definition of [subst'].#</li>#
adamc@127 911 %\item%#<li># Now [subst] should be a one-liner, defined in terms of [subst'].#</li>#
adamc@127 912 %\item%#<li># Prove a correctness theorem for each auxiliary function, leading up to the proof of [subst] correctness.#</li>#
adam@292 913 %\item%#<li># All of the reasoning about equality proofs in these theorems follows a regular pattern. If you have an equality proof that you want to replace with [refl_equal] somehow, run [generalize] on that proof variable. Your goal is to get to the point where you can [rewrite] with the original proof to change the type of the generalized version. To avoid type errors (the infamous %``%#"#second-order unification#"#%''% failure messages), it will be helpful to run [generalize] on other pieces of the proof context that mention the equality's lefthand side. You might also want to use [generalize dependent], which generalizes not just one variable but also all variables whose types depend on it. [generalize dependent] has the sometimes-helpful property of removing from the context all variables that it generalizes. Once you do manage the mind-bending trick of using the equality proof to rewrite its own type, you will be able to rewrite with [UIP_refl].#</li>#
adam@364 914 %\item%#<li># The [ext_eq] axiom from the end of this chapter is available in the Coq standard library as [functional_extensionality] in module [FunctionalExtensionality], and you will probably want to use it in the [lift'] and [subst'] correctness proofs.#</li>#
adam@292 915 %\item%#<li># The [change] tactic should come in handy in the proofs about [lift] and [subst], where you want to introduce %``%#"#extraneous#"#%''% list concatenations with [nil] to match the forms of earlier theorems.#</li>#
adam@292 916 %\item%#<li># Be careful about [destruct]ing a term %``%#"#too early.#"#%''% You can use [generalize] on proof terms to bring into the proof context any important propositions about the term. Then, when you [destruct] the term, it is updated in the extra propositions, too. The [case_eq] tactic is another alternative to this approach, based on saving an equality between the original term and its new form.#</li>#
adamc@127 917 #</ol>#%\end{enumerate}%
adamc@127 918 #</li>#
adamc@127 919
adamc@127 920 #</ol>#%\end{enumerate}% *)