Mercurial > cpdt > repo

annotate src/Equality.v @ 206:3f4576f15130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Revising for 8.2 through first big example
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 16:44:06 -0500
parents f05514cc6c0d
children c8508d277a00
rev   line source
adamc@118 1 (* Copyright (c) 2008, Adam Chlipala
adamc@118 2 *
adamc@118 3 * This work is licensed under a
adamc@118 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@118 5 * Unported License.
adamc@118 6 * The license text is available at:
adamc@118 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@118 8 *)
adamc@118 9
adamc@118 10 (* begin hide *)
adamc@120 11 Require Import Eqdep JMeq List.
adamc@118 12
adamc@132 13 Require Import Tactics.
adamc@118 14
adamc@118 15 Set Implicit Arguments.
adamc@118 16 (* end hide *)
adamc@118 17
adamc@118 18
adamc@118 19 (** %\chapter{Reasoning About Equality Proofs}% *)
adamc@118 20
adamc@118 21 (** In traditional mathematics, the concept of equality is usually taken as a given. On the other hand, in type theory, equality is a very contentious subject. There are at least three different notions of equality that are important, and researchers are actively investigating new definitions of what it means for two terms to be equal. Even once we fix a notion of equality, there are inevitably tricky issues that arise in proving properties of programs that manipulate equality proofs explicitly. In this chapter, we will focus on design patterns for circumventing these tricky issues, and we will introduce the different notions of equality as they are germane. *)
adamc@118 22
adamc@118 23
adamc@122 24 (** * The Definitional Equality *)
adamc@122 25
adamc@122 26 (** We have seen many examples so far where proof goals follow "by computation." That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's %\textit{%#<i>#definitional equality#</i>#%}%. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal.
adamc@122 27
adamc@199 28 The [cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [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@124 37 (* begin thide *)
adamc@122 38 (** CIC follows the traditions of lambda calculus in associating reduction rules with Greek letters. Coq can certainly be said to support the familiar alpha reduction rule, which allows capture-avoiding renaming of bound variables, but we never need to apply alpha explicitly, since Coq uses a de Bruijn representation that encodes terms canonically.
adamc@122 39
adamc@131 40 The delta rule is for unfolding global definitions. We can use it here to unfold the definition of [pred']. We do this with the [cbv] tactic, which takes a list of reduction rules and makes as many call-by-value reduction steps as possible, using only those rules. There is an analogous tactic [lazy] for call-by-need reduction. *)
adamc@122 41
adamc@122 42 cbv delta.
adamc@122 43 (** [[
adamc@122 44
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
adamc@122 52 At this point, we want to apply the famous beta reduction of lambda calculus, to simplify the application of a known function abstraction. *)
adamc@122 53
adamc@122 54 cbv beta.
adamc@122 55 (** [[
adamc@122 56
adamc@122 57 ============================
adamc@122 58 match 1 with
adamc@122 59 | 0 => 0
adamc@122 60 | S n' => let y := n' in y
adamc@122 61 end = 0
adamc@122 62 ]]
adamc@122 63
adamc@122 64 Next on the list is the iota reduction, which simplifies a single [match] term by determining which pattern matches. *)
adamc@122 65
adamc@122 66 cbv iota.
adamc@122 67 (** [[
adamc@122 68
adamc@122 69 ============================
adamc@122 70 (fun n' : nat => let y := n' in y) 0 = 0
adamc@122 71 ]]
adamc@122 72
adamc@122 73 Now we need another beta reduction. *)
adamc@122 74
adamc@122 75 cbv beta.
adamc@122 76 (** [[
adamc@122 77
adamc@122 78 ============================
adamc@122 79 (let y := 0 in y) = 0
adamc@122 80 ]]
adamc@122 81
adamc@122 82 The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term subsituted. *)
adamc@122 83
adamc@122 84 cbv zeta.
adamc@122 85 (** [[
adamc@122 86
adamc@122 87 ============================
adamc@122 88 0 = 0
adamc@122 89 ]] *)
adamc@122 90
adamc@122 91 reflexivity.
adamc@122 92 Qed.
adamc@124 93 (* end thide *)
adamc@122 94
adamc@122 95 (** The standard [eq] relation is critically dependent on the definitional equality. [eq] is often called a %\textit{%#<i>#propositional equality#</i>#%}%, because it reifies definitional equality as a proposition that may or may not hold. Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity. In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina. We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use.
adamc@122 96
adamc@122 97 This all may make it sound like the choice of [eq]'s definition is unimportant. To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs. Before that point, we will introduce effective proof methods for goals that use proofs of the standard propositional equality "as data." *)
adamc@122 98
adamc@122 99
adamc@118 100 (** * Heterogeneous Lists Revisited *)
adamc@118 101
adamc@118 102 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. *)
adamc@118 103
adamc@118 104 Section fhlist.
adamc@118 105 Variable A : Type.
adamc@118 106 Variable B : A -> Type.
adamc@118 107
adamc@118 108 Fixpoint fhlist (ls : list A) : Type :=
adamc@118 109 match ls with
adamc@118 110 | nil => unit
adamc@118 111 | x :: ls' => B x * fhlist ls'
adamc@118 112 end%type.
adamc@118 113
adamc@118 114 Variable elm : A.
adamc@118 115
adamc@118 116 Fixpoint fmember (ls : list A) : Type :=
adamc@118 117 match ls with
adamc@118 118 | nil => Empty_set
adamc@118 119 | x :: ls' => (x = elm) + fmember ls'
adamc@118 120 end%type.
adamc@118 121
adamc@118 122 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@118 123 match ls return fhlist ls -> fmember ls -> B elm with
adamc@118 124 | nil => fun _ idx => match idx with end
adamc@118 125 | _ :: ls' => fun mls idx =>
adamc@118 126 match idx with
adamc@118 127 | inl pf => match pf with
adamc@118 128 | refl_equal => fst mls
adamc@118 129 end
adamc@118 130 | inr idx' => fhget ls' (snd mls) idx'
adamc@118 131 end
adamc@118 132 end.
adamc@118 133 End fhlist.
adamc@118 134
adamc@118 135 Implicit Arguments fhget [A B elm ls].
adamc@118 136
adamc@118 137 (** We can define a [map]-like function for [fhlist]s. *)
adamc@118 138
adamc@118 139 Section fhlist_map.
adamc@118 140 Variables A : Type.
adamc@118 141 Variables B C : A -> Type.
adamc@118 142 Variable f : forall x, B x -> C x.
adamc@118 143
adamc@118 144 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
adamc@118 145 match ls return fhlist B ls -> fhlist C ls with
adamc@118 146 | nil => fun _ => tt
adamc@118 147 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
adamc@118 148 end.
adamc@118 149
adamc@118 150 Implicit Arguments fhmap [ls].
adamc@118 151
adamc@118 152 (** 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 153
adamc@118 154 Variable elm : A.
adamc@118 155
adamc@118 156 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
adamc@118 157 fhget (fhmap hls) mem = f (fhget hls mem).
adamc@124 158 (* begin thide *)
adamc@118 159 induction ls; crush.
adamc@118 160
adamc@118 161 (** Part of our single remaining subgoal is:
adamc@118 162
adamc@118 163 [[
adamc@118 164
adamc@118 165 a0 : a = elm
adamc@118 166 ============================
adamc@118 167 match a0 in (_ = a2) return (C a2) with
adamc@118 168 | refl_equal => f a1
adamc@118 169 end = f match a0 in (_ = a2) return (B a2) with
adamc@118 170 | refl_equal => a1
adamc@118 171 end
adamc@118 172 ]]
adamc@118 173
adamc@118 174 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 175
adamc@118 176 [[
adamc@118 177
adamc@118 178 destruct a0.
adamc@118 179
adamc@205 180 ]]
adamc@205 181
adamc@118 182 [[
adamc@118 183 User error: Cannot solve a second-order unification problem
adamc@118 184 ]]
adamc@118 185
adamc@118 186 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 187
adamc@118 188 [[
adamc@118 189
adamc@118 190 assert (a0 = refl_equal _).
adamc@118 191
adamc@205 192 ]]
adamc@205 193
adamc@118 194 [[
adamc@118 195 The term "refl_equal ?98" has type "?98 = ?98"
adamc@118 196 while it is expected to have type "a = elm"
adamc@118 197 ]]
adamc@118 198
adamc@118 199 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 200
adamc@118 201 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 202
adamc@118 203 For this particular example, the solution is surprisingly straightforward. [destruct] has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments. *)
adamc@118 204
adamc@118 205 case a0.
adamc@118 206 (** [[
adamc@118 207
adamc@118 208 ============================
adamc@118 209 f a1 = f a1
adamc@118 210 ]]
adamc@118 211
adamc@118 212 It seems that [destruct] was trying to be too smart for its own good. *)
adamc@118 213
adamc@118 214 reflexivity.
adamc@118 215 Qed.
adamc@124 216 (* end thide *)
adamc@118 217
adamc@118 218 (** 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 219
adamc@118 220 Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
adamc@124 221 (* begin thide *)
adamc@118 222 simple destruct pf; reflexivity.
adamc@118 223 Qed.
adamc@124 224 (* end thide *)
adamc@118 225
adamc@118 226 (** [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 227
adamc@118 228 Print lemma1.
adamc@118 229
adamc@118 230 (** [[
adamc@118 231
adamc@118 232 lemma1 =
adamc@118 233 fun (x : A) (pf : x = elm) =>
adamc@118 234 match pf as e in (_ = y) return (0 = match e with
adamc@118 235 | refl_equal => 0
adamc@118 236 end) with
adamc@118 237 | refl_equal => refl_equal 0
adamc@118 238 end
adamc@118 239 : forall (x : A) (pf : x = elm), 0 = match pf with
adamc@118 240 | refl_equal => 0
adamc@118 241 end
adamc@118 242 ]]
adamc@118 243
adamc@118 244 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
adamc@118 245
adamc@124 246 (* begin thide *)
adamc@118 247 Definition lemma1' :=
adamc@118 248 fun (x : A) (pf : x = elm) =>
adamc@118 249 match pf return (0 = match pf with
adamc@118 250 | refl_equal => 0
adamc@118 251 end) with
adamc@118 252 | refl_equal => refl_equal 0
adamc@118 253 end.
adamc@124 254 (* end thide *)
adamc@118 255
adamc@118 256 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)
adamc@118 257
adamc@118 258 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
adamc@124 259 (* begin thide *)
adamc@118 260 (** [[
adamc@118 261
adamc@118 262 simple destruct pf.
adamc@205 263
adamc@205 264 ]]
adamc@118 265
adamc@118 266 [[
adamc@118 267
adamc@118 268 User error: Cannot solve a second-order unification problem
adamc@118 269 ]] *)
adamc@118 270 Abort.
adamc@118 271
adamc@118 272 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
adamc@118 273
adamc@124 274 (* begin thide *)
adamc@124 275 Definition lemma2 :=
adamc@118 276 fun (x : A) (pf : x = x) =>
adamc@118 277 match pf return (0 = match pf with
adamc@118 278 | refl_equal => 0
adamc@118 279 end) with
adamc@118 280 | refl_equal => refl_equal 0
adamc@118 281 end.
adamc@124 282 (* end thide *)
adamc@118 283
adamc@118 284 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
adamc@118 285
adamc@118 286 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@124 287 (* begin thide *)
adamc@118 288 (** [[
adamc@118 289
adamc@118 290 simple destruct pf.
adamc@205 291
adamc@205 292 ]]
adamc@118 293
adamc@118 294 [[
adamc@118 295
adamc@118 296 User error: Cannot solve a second-order unification problem
adamc@118 297 ]] *)
adamc@118 298 Abort.
adamc@118 299
adamc@118 300 (** This time, even our manual attempt fails.
adamc@118 301
adamc@118 302 [[
adamc@118 303
adamc@118 304 Definition lemma3' :=
adamc@118 305 fun (x : A) (pf : x = x) =>
adamc@118 306 match pf as pf' in (_ = x') return (pf' = refl_equal x') with
adamc@118 307 | refl_equal => refl_equal _
adamc@118 308 end.
adamc@118 309
adamc@205 310 ]]
adamc@205 311
adamc@118 312 [[
adamc@118 313
adamc@118 314 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
adamc@118 315 "x = x'"
adamc@118 316 ]]
adamc@118 317
adamc@118 318 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], refering to the [in]-bound variable [x']. To do a dependent [match], we %\textit{%#<i>#must#</i>#%}% choose a fresh name for the second argument of [eq]. We are just as constrained to use the "real" value [x] for the first argument. Thus, within the [return] clause, the proof we are matching on %\textit{%#<i>#must#</i>#%}% equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
adamc@118 319
adamc@118 320 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)
adamc@118 321
adamc@118 322 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@118 323 intros; apply UIP_refl.
adamc@118 324 Qed.
adamc@118 325
adamc@118 326 Check UIP_refl.
adamc@118 327 (** [[
adamc@118 328
adamc@118 329 UIP_refl
adamc@118 330 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
adamc@118 331 ]]
adamc@118 332
adamc@118 333 [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 334
adamc@118 335 Print eq_rect_eq.
adamc@118 336 (** [[
adamc@118 337
adamc@118 338 eq_rect_eq =
adamc@118 339 fun U : Type => Eq_rect_eq.eq_rect_eq U
adamc@118 340 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@118 341 x = eq_rect p Q x p h
adamc@118 342 ]]
adamc@118 343
adamc@118 344 [eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. [eq_rect] is the automatically-generated recursion principle for [eq]. Calling [eq_rect] is another way of [match]ing on an equality proof. The proof we match on is the argument [h], and [x] is the body of the [match]. [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed.
adamc@118 345
adamc@118 346 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an axiom; that is, a proposition asserted as true without proof. We cannot assert just any statement without proof. Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant. In general, we need to be sure that we never assert %\textit{%#<i>#inconsistent#</i>#%}% sets of axioms. A set of axioms is inconsistent if its conjunction implies [False]. For the case of [eq_rect_eq], consistency has been verified outside of Coq via "informal" metatheory.
adamc@118 347
adamc@118 348 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
adamc@118 349
adamc@118 350 Print Streicher_K.
adamc@124 351 (* end thide *)
adamc@118 352 (** [[
adamc@118 353
adamc@118 354 Streicher_K =
adamc@118 355 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
adamc@118 356 : forall (U : Type) (x : U) (P : x = x -> Prop),
adamc@118 357 P (refl_equal x) -> forall p : x = x, P p
adamc@118 358 ]]
adamc@118 359
adamc@118 360 This is the unfortunately-named "Streicher's axiom K," which says that a predicate on properly-typed equality proofs holds of all such proofs if it holds of reflexivity. *)
adamc@118 361
adamc@118 362 End fhlist_map.
adamc@118 363
adamc@119 364
adamc@119 365 (** * Type-Casts in Theorem Statements *)
adamc@119 366
adamc@119 367 (** 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 368
adamc@119 369 Section fhapp.
adamc@119 370 Variable A : Type.
adamc@119 371 Variable B : A -> Type.
adamc@119 372
adamc@119 373 Fixpoint fhapp (ls1 ls2 : list A) {struct ls1}
adamc@119 374 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
adamc@119 375 match ls1 return fhlist _ ls1 -> _ -> fhlist _ (ls1 ++ ls2) with
adamc@119 376 | nil => fun _ hls2 => hls2
adamc@119 377 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
adamc@119 378 end.
adamc@119 379
adamc@119 380 Implicit Arguments fhapp [ls1 ls2].
adamc@119 381
adamc@124 382 (* EX: Prove that fhapp is associative. *)
adamc@124 383 (* begin thide *)
adamc@124 384
adamc@119 385 (** We might like to prove that [fhapp] is associative.
adamc@119 386
adamc@119 387 [[
adamc@119 388
adamc@119 389 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 390 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 391 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
adamc@119 392
adamc@205 393 ]]
adamc@205 394
adamc@119 395 [[
adamc@119 396
adamc@119 397 The term
adamc@119 398 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
adamc@119 399 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
adamc@119 400 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
adamc@119 401 ]]
adamc@119 402
adamc@119 403 This first cut at the theorem statement does not even type-check. We know that the two [fhlist] types appearing in the error message are always equal, by associativity of normal list append, but this fact is not apparent to the type checker. This stems from the fact that Coq's equality is %\textit{%#<i>#intensional#</i>#%}%, in the sense that type equality theorems can never be applied after the fact to get a term to type-check. Instead, we need to make use of equality explicitly in the theorem statement. *)
adamc@119 404
adamc@119 405 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 406 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
adamc@119 407 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 408 fhapp hls1 (fhapp hls2 hls3)
adamc@119 409 = match pf in (_ = ls) return fhlist _ ls with
adamc@119 410 | refl_equal => fhapp (fhapp hls1 hls2) hls3
adamc@119 411 end.
adamc@119 412 induction ls1; crush.
adamc@119 413
adamc@119 414 (** The first remaining subgoal looks trivial enough:
adamc@119 415
adamc@119 416 [[
adamc@119 417
adamc@119 418 ============================
adamc@119 419 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 420 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 421 | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 422 end
adamc@119 423 ]]
adamc@119 424
adamc@119 425 We can try what worked in previous examples.
adamc@119 426
adamc@119 427 [[
adamc@119 428 case pf.
adamc@119 429
adamc@205 430 ]]
adamc@205 431
adamc@119 432 [[
adamc@119 433
adamc@119 434 User error: Cannot solve a second-order unification problem
adamc@119 435 ]]
adamc@119 436
adamc@119 437 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 438
adamc@119 439 rewrite (UIP_refl _ _ pf).
adamc@119 440 (** [[
adamc@119 441
adamc@119 442 ============================
adamc@119 443 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 444 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 445 ]] *)
adamc@119 446
adamc@119 447 reflexivity.
adamc@119 448
adamc@119 449 (** Our second subgoal is trickier.
adamc@119 450
adamc@119 451 [[
adamc@119 452
adamc@119 453 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 454 ============================
adamc@119 455 (a0,
adamc@119 456 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 457 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 458 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 459 | refl_equal =>
adamc@119 460 (a0,
adamc@119 461 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 462 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 463 end
adamc@119 464 ]]
adamc@119 465
adamc@119 466
adamc@119 467 [[
adamc@119 468
adamc@119 469 rewrite (UIP_refl _ _ pf).
adamc@119 470
adamc@205 471 ]]
adamc@205 472
adamc@119 473 [[
adamc@119 474 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
adamc@119 475 while it is expected to have type "?556 = ?556"
adamc@119 476 ]]
adamc@119 477
adamc@119 478 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 479
adamc@119 480 injection pf; intro pf'.
adamc@119 481 (** [[
adamc@119 482
adamc@119 483 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 484 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
adamc@119 485 ============================
adamc@119 486 (a0,
adamc@119 487 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 488 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 489 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 490 | refl_equal =>
adamc@119 491 (a0,
adamc@119 492 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 493 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 494 end
adamc@119 495 ]]
adamc@119 496
adamc@119 497 Now we can rewrite using the inductive hypothesis. *)
adamc@119 498
adamc@119 499 rewrite (IHls1 _ _ pf').
adamc@119 500 (** [[
adamc@119 501
adamc@119 502 ============================
adamc@119 503 (a0,
adamc@119 504 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 505 | refl_equal =>
adamc@119 506 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 507 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
adamc@119 508 end) =
adamc@119 509 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 510 | refl_equal =>
adamc@119 511 (a0,
adamc@119 512 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 513 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 514 end
adamc@119 515 ]]
adamc@119 516
adamc@119 517 We have made an important bit of progress, as now only a single call to [fhapp] appears in the conclusion. Trying case analysis on our proofs still will not work, but there is a move we can make to enable it. Not only does just one call to [fhapp] matter to us now, but it also %\textit{%#<i>#does not matter what the result of the call is#</i>#%}%. In other words, the subgoal should remain true if we replace this [fhapp] call with a fresh variable. The [generalize] tactic helps us do exactly that. *)
adamc@119 518
adamc@119 519 generalize (fhapp (fhapp b hls2) hls3).
adamc@119 520 (** [[
adamc@119 521
adamc@119 522 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
adamc@119 523 (a0,
adamc@119 524 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 525 | refl_equal => f
adamc@119 526 end) =
adamc@119 527 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 528 | refl_equal => (a0, f)
adamc@119 529 end
adamc@119 530 ]]
adamc@119 531
adamc@119 532 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 533
adamc@119 534 In this case, it is helpful to generalize over our two proofs as well. *)
adamc@119 535
adamc@119 536 generalize pf pf'.
adamc@119 537 (** [[
adamc@119 538
adamc@119 539 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 540 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 541 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
adamc@119 542 (a0,
adamc@119 543 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 544 | refl_equal => f
adamc@119 545 end) =
adamc@119 546 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 547 | refl_equal => (a0, f)
adamc@119 548 end
adamc@119 549 ]]
adamc@119 550
adamc@119 551 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 552
adamc@119 553 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 554
adamc@119 555 rewrite app_ass.
adamc@119 556 (** [[
adamc@119 557
adamc@119 558 ============================
adamc@119 559 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 560 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 561 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
adamc@119 562 (a0,
adamc@119 563 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 564 | refl_equal => f
adamc@119 565 end) =
adamc@119 566 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 567 | refl_equal => (a0, f)
adamc@119 568 end
adamc@119 569 ]]
adamc@119 570
adamc@119 571 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 572
adamc@119 573 intros.
adamc@119 574 rewrite (UIP_refl _ _ pf0).
adamc@119 575 rewrite (UIP_refl _ _ pf'0).
adamc@119 576 reflexivity.
adamc@119 577 Qed.
adamc@124 578 (* end thide *)
adamc@119 579 End fhapp.
adamc@120 580
adamc@120 581 Implicit Arguments fhapp [A B ls1 ls2].
adamc@120 582
adamc@120 583
adamc@120 584 (** * Heterogeneous Equality *)
adamc@120 585
adamc@120 586 (** There is another equality predicate, defined in the [JMeq] module of the standard library, implementing %\textit{%#<i>#heterogeneous equality#</i>#%}%. *)
adamc@120 587
adamc@120 588 Print JMeq.
adamc@120 589 (** [[
adamc@120 590
adamc@120 591 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
adamc@120 592 JMeq_refl : JMeq x x
adamc@120 593 ]]
adamc@120 594
adamc@120 595 [JMeq] stands for "John Major equality," a name coined by Conor McBride as a sort of pun about British politics. [JMeq] starts out looking a lot like [eq]. The crucial difference is that we may use [JMeq] %\textit{%#<i>#on arguments of different types#</i>#%}%. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *)
adamc@120 596
adamc@120 597 Infix "==" := JMeq (at level 70, no associativity).
adamc@120 598
adamc@124 599 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
adamc@124 600 (* begin thide *)
adamc@121 601 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
adamc@120 602 match pf return (pf == refl_equal _) with
adamc@120 603 | refl_equal => JMeq_refl _
adamc@120 604 end.
adamc@124 605 (* end thide *)
adamc@120 606
adamc@120 607 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
adamc@120 608
adamc@121 609 Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *)
adamc@120 610
adamc@120 611 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
adamc@120 612 O = match pf with refl_equal => O end.
adamc@124 613 (* begin thide *)
adamc@121 614 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@120 615 Qed.
adamc@124 616 (* end thide *)
adamc@120 617
adamc@120 618 (** 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 619
adamc@120 620 Check JMeq_eq.
adamc@120 621 (** [[
adamc@120 622
adamc@120 623 JMeq_eq
adamc@120 624 : forall (A : Type) (x y : A), x == y -> x = y
adamc@120 625 ]] *)
adamc@120 626
adamc@120 627 (** 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 628
adamc@120 629 We can redo our [fhapp] associativity proof based around [JMeq]. *)
adamc@120 630
adamc@120 631 Section fhapp'.
adamc@120 632 Variable A : Type.
adamc@120 633 Variable B : A -> Type.
adamc@120 634
adamc@120 635 (** This time, the naive theorem statement type-checks. *)
adamc@120 636
adamc@124 637 (* EX: Prove [fhapp] associativity using [JMeq]. *)
adamc@124 638
adamc@124 639 (* begin thide *)
adamc@120 640 Theorem fhapp_ass' : forall ls1 ls2 ls3
adamc@120 641 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@120 642 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adamc@120 643 induction ls1; crush.
adamc@120 644
adamc@120 645 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
adamc@120 646
adamc@120 647 [[
adamc@120 648
adamc@120 649 ============================
adamc@120 650 (a0,
adamc@120 651 fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@120 652 (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) ==
adamc@120 653 (a0,
adamc@120 654 fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@120 655 (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@120 656 ]]
adamc@120 657
adamc@120 658 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial.
adamc@120 659
adamc@120 660 [[
adamc@120 661
adamc@120 662 rewrite IHls1.
adamc@120 663
adamc@205 664 ]]
adamc@205 665
adamc@120 666 [[
adamc@120 667
adamc@120 668 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
adamc@120 669 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
adamc@120 670 ]]
adamc@120 671
adamc@120 672 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 673
adamc@120 674 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 675
adamc@120 676 generalize (fhapp b (fhapp hls2 hls3))
adamc@120 677 (fhapp (fhapp b hls2) hls3)
adamc@120 678 (IHls1 _ _ b hls2 hls3).
adamc@120 679 (** [[
adamc@120 680
adamc@120 681 ============================
adamc@120 682 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
adamc@120 683 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
adamc@120 684 ]]
adamc@120 685
adamc@120 686 Now we can rewrite with append associativity, as before. *)
adamc@120 687
adamc@120 688 rewrite app_ass.
adamc@120 689 (** [[
adamc@120 690
adamc@120 691 ============================
adamc@120 692 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
adamc@120 693 ]]
adamc@120 694
adamc@120 695 From this point, the goal is trivial. *)
adamc@120 696
adamc@120 697 intros f f0 H; rewrite H; reflexivity.
adamc@120 698 Qed.
adamc@124 699 (* end thide *)
adamc@120 700 End fhapp'.
adamc@121 701
adamc@121 702
adamc@121 703 (** * Equivalence of Equality Axioms *)
adamc@121 704
adamc@124 705 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
adamc@124 706
adamc@124 707 (* begin thide *)
adamc@121 708 (** Assuming axioms (like axiom K and [JMeq_eq]) is a hazardous business. The due diligence associated with it is necessarily global in scope, since two axioms may be consistent alone but inconsistent together. It turns out that all of the major axioms proposed for reasoning about equality in Coq are logically equivalent, so that we only need to pick one to assert without proof. In this section, we demonstrate this by showing how each the previous two sections' approaches reduces to the other logically.
adamc@121 709
adamc@121 710 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 711
adamc@121 712 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
adamc@121 713 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@121 714 Qed.
adamc@121 715
adamc@121 716 (** 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 717
adamc@121 718 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
adamc@121 719 exists pf : B = A, x = match pf with refl_equal => y end.
adamc@121 720
adamc@121 721 Infix "===" := JMeq' (at level 70, no associativity).
adamc@121 722
adamc@121 723 (** 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 724
adamc@121 725 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
adamc@121 726
adamc@121 727 (** remove printing exists *)
adamc@121 728 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
adamc@121 729 intros; unfold JMeq'; exists (refl_equal A); reflexivity.
adamc@121 730 Qed.
adamc@121 731
adamc@121 732 (** printing exists $\exists$ *)
adamc@121 733
adamc@121 734 (** 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 735
adamc@121 736 Theorem JMeq_eq' : forall (A : Type) (x y : A),
adamc@121 737 x === y -> x = y.
adamc@121 738 unfold JMeq'; intros.
adamc@121 739 (** [[
adamc@121 740
adamc@121 741 H : exists pf : A = A,
adamc@121 742 x = match pf in (_ = T) return T with
adamc@121 743 | refl_equal => y
adamc@121 744 end
adamc@121 745 ============================
adamc@121 746 x = y
adamc@121 747 ]] *)
adamc@121 748
adamc@121 749 destruct H.
adamc@121 750 (** [[
adamc@121 751
adamc@121 752 x0 : A = A
adamc@121 753 H : x = match x0 in (_ = T) return T with
adamc@121 754 | refl_equal => y
adamc@121 755 end
adamc@121 756 ============================
adamc@121 757 x = y
adamc@121 758 ]] *)
adamc@121 759
adamc@121 760 rewrite H.
adamc@121 761 (** [[
adamc@121 762
adamc@121 763 x0 : A = A
adamc@121 764 ============================
adamc@121 765 match x0 in (_ = T) return T with
adamc@121 766 | refl_equal => y
adamc@121 767 end = y
adamc@121 768 ]] *)
adamc@121 769
adamc@121 770 rewrite (UIP_refl _ _ x0); reflexivity.
adamc@121 771 Qed.
adamc@121 772
adamc@123 773 (** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs. One style may be more convenient than the other for some proofs, but we can always intercovert between our results. The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those "simple" proofs. On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements.
adamc@123 774
adamc@123 775 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. *)
adamc@124 776 (* end thide *)
adamc@123 777
adamc@123 778
adamc@123 779 (** * Equality of Functions *)
adamc@123 780
adamc@123 781 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
adamc@123 782
adamc@123 783 Theorem S_eta : S = (fun n => S n).
adamc@123 784
adamc@205 785 ]]
adamc@205 786
adamc@123 787 Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be %\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 788
adamc@124 789 (* begin thide *)
adamc@123 790 Axiom ext_eq : forall A B (f g : A -> B),
adamc@123 791 (forall x, f x = g x)
adamc@123 792 -> f = g.
adamc@124 793 (* end thide *)
adamc@123 794
adamc@123 795 (** 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 796
adamc@123 797 Theorem S_eta : S = (fun n => S n).
adamc@124 798 (* begin thide *)
adamc@123 799 apply ext_eq; reflexivity.
adamc@123 800 Qed.
adamc@124 801 (* end thide *)
adamc@123 802
adamc@123 803 (** The same axiom can help us prove equality of types, where we need to "reason under quantifiers." *)
adamc@123 804
adamc@123 805 Theorem forall_eq : (forall x : nat, match x with
adamc@123 806 | O => True
adamc@123 807 | S _ => True
adamc@123 808 end)
adamc@123 809 = (forall _ : nat, True).
adamc@123 810
adamc@123 811 (** There are no immediate opportunities to apply [ext_eq], but we can use [change] to fix that. *)
adamc@123 812
adamc@124 813 (* begin thide *)
adamc@123 814 change ((forall x : nat, (fun x => match x with
adamc@123 815 | 0 => True
adamc@123 816 | S _ => True
adamc@123 817 end) x) = (nat -> True)).
adamc@123 818 rewrite (ext_eq (fun x => match x with
adamc@123 819 | 0 => True
adamc@123 820 | S _ => True
adamc@123 821 end) (fun _ => True)).
adamc@123 822 (** [[
adamc@123 823
adamc@123 824 2 subgoals
adamc@123 825
adamc@123 826 ============================
adamc@123 827 (nat -> True) = (nat -> True)
adamc@123 828
adamc@123 829 subgoal 2 is:
adamc@123 830 forall x : nat, match x with
adamc@123 831 | 0 => True
adamc@123 832 | S _ => True
adamc@123 833 end = True
adamc@123 834 ]] *)
adamc@123 835
adamc@123 836
adamc@123 837 reflexivity.
adamc@123 838
adamc@123 839 destruct x; constructor.
adamc@123 840 Qed.
adamc@124 841 (* end thide *)
adamc@127 842
adamc@127 843
adamc@127 844 (** * Exercises *)
adamc@127 845
adamc@127 846 (** %\begin{enumerate}%#<ol>#
adamc@127 847
adamc@127 848 %\item%#<li># Implement and prove correct a substitution function for simply-typed lambda calculus. In particular:
adamc@127 849 %\begin{enumerate}%#<ol>#
adamc@127 850 %\item%#<li># Define a datatype [type] of lambda types, including just booleans and function types.#</li>#
adamc@127 851 %\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 852 %\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>#
adamc@127 853 %\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 854 %\item%#<li># Prove that [subst] preserves program meanings. That is, prove
adamc@127 855 [[
adamc@127 856 forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts),
adamc@127 857 expDenote (subst e e') s = expDenote e (expDenote e' s ::: s)
adamc@127 858 ]]
adamc@127 859 where [:::] is an infix operator for heterogeneous "cons" that is defined in the book's [DepList] module.#</li>#
adamc@127 860 #</ol>#%\end{enumerate}%
adamc@127 861 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 862 %\begin{enumerate}%#<ol>#
adamc@127 863 %\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>#
adamc@127 864 %\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>#
adamc@127 865 %\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 866 %\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 867 %\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 868 %\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 869 %\item%#<li># Now [subst] should be a one-liner, defined in terms of [subst'].#</li>#
adamc@127 870 %\item%#<li># Prove a correctness theorem for each auxiliary function, leading up to the proof of [subst] correctness.#</li>#
adamc@127 871 %\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>#
adamc@127 872 %\item%#<li># A variant of the [ext_eq] axiom from the end of this chapter is available in the book module [Axioms], and you will probably want to use it in the [lift'] and [subst'] correctness proofs.#</li>#
adamc@127 873 %\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>#
adamc@127 874 %\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 875 #</ol>#%\end{enumerate}%
adamc@127 876 #</li>#
adamc@127 877
adamc@127 878 #</ol>#%\end{enumerate}% *)