Mercurial > cpdt > repo

annotate src/Equality.v @ 364:2fbb47fb02bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through old content of Equality
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 Nov 2011 16:25:45 -0500
parents d5787b70cf48
children 990151eac6af
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@364 92 (** 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 93
adam@294 94 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 95
adamc@122 96
adamc@118 97 (** * Heterogeneous Lists Revisited *)
adamc@118 98
adam@292 99 (** 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 100
adamc@118 101 Section fhlist.
adamc@118 102 Variable A : Type.
adamc@118 103 Variable B : A -> Type.
adamc@118 104
adamc@118 105 Fixpoint fhlist (ls : list A) : Type :=
adamc@118 106 match ls with
adamc@118 107 | nil => unit
adamc@118 108 | x :: ls' => B x * fhlist ls'
adamc@118 109 end%type.
adamc@118 110
adamc@118 111 Variable elm : A.
adamc@118 112
adamc@118 113 Fixpoint fmember (ls : list A) : Type :=
adamc@118 114 match ls with
adamc@118 115 | nil => Empty_set
adamc@118 116 | x :: ls' => (x = elm) + fmember ls'
adamc@118 117 end%type.
adamc@118 118
adamc@118 119 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@118 120 match ls return fhlist ls -> fmember ls -> B elm with
adamc@118 121 | nil => fun _ idx => match idx with end
adamc@118 122 | _ :: ls' => fun mls idx =>
adamc@118 123 match idx with
adamc@118 124 | inl pf => match pf with
adamc@118 125 | refl_equal => fst mls
adamc@118 126 end
adamc@118 127 | inr idx' => fhget ls' (snd mls) idx'
adamc@118 128 end
adamc@118 129 end.
adamc@118 130 End fhlist.
adamc@118 131
adamc@118 132 Implicit Arguments fhget [A B elm ls].
adamc@118 133
adamc@118 134 (** We can define a [map]-like function for [fhlist]s. *)
adamc@118 135
adamc@118 136 Section fhlist_map.
adamc@118 137 Variables A : Type.
adamc@118 138 Variables B C : A -> Type.
adamc@118 139 Variable f : forall x, B x -> C x.
adamc@118 140
adamc@118 141 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
adamc@118 142 match ls return fhlist B ls -> fhlist C ls with
adamc@118 143 | nil => fun _ => tt
adamc@118 144 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
adamc@118 145 end.
adamc@118 146
adamc@118 147 Implicit Arguments fhmap [ls].
adamc@118 148
adamc@118 149 (** 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 150
adamc@118 151 Variable elm : A.
adamc@118 152
adamc@118 153 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
adamc@118 154 fhget (fhmap hls) mem = f (fhget hls mem).
adam@298 155 (* begin hide *)
adam@298 156 induction ls; crush; case a0; reflexivity.
adam@298 157 (* end hide *)
adam@364 158 (** %\vspace{-.2in}%[[
adamc@118 159 induction ls; crush.
adam@298 160 ]]
adamc@118 161
adam@364 162 %\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 163
adam@297 164 Part of our single remaining subgoal is:
adamc@118 165 [[
adamc@118 166 a0 : a = elm
adamc@118 167 ============================
adamc@118 168 match a0 in (_ = a2) return (C a2) with
adamc@118 169 | refl_equal => f a1
adamc@118 170 end = f match a0 in (_ = a2) return (B a2) with
adamc@118 171 | refl_equal => a1
adamc@118 172 end
adamc@118 173 ]]
adamc@118 174
adamc@118 175 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 176 [[
adamc@118 177 destruct a0.
adamc@118 178 ]]
adamc@118 179
adam@364 180 <<
adam@364 181 User error: Cannot solve a second-order unification problem
adam@364 182 >>
adam@364 183
adamc@118 184 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 185 [[
adamc@118 186 assert (a0 = refl_equal _).
adam@364 187 ]]
adamc@118 188
adam@364 189 <<
adamc@118 190 The term "refl_equal ?98" has type "?98 = ?98"
adamc@118 191 while it is expected to have type "a = elm"
adam@364 192 >>
adamc@118 193
adamc@118 194 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 195
adam@292 196 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 197
adam@297 198 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 199 [[
adamc@118 200 case a0.
adam@297 201
adamc@118 202 ============================
adamc@118 203 f a1 = f a1
adamc@118 204 ]]
adamc@118 205
adam@297 206 It seems that [destruct] was trying to be too smart for its own good.
adam@297 207 [[
adamc@118 208 reflexivity.
adam@302 209 ]]
adam@364 210 %\vspace{-.2in}% *)
adamc@118 211 Qed.
adamc@124 212 (* end thide *)
adamc@118 213
adamc@118 214 (** 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 215
adamc@118 216 Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
adamc@124 217 (* begin thide *)
adamc@118 218 simple destruct pf; reflexivity.
adamc@118 219 Qed.
adamc@124 220 (* end thide *)
adamc@118 221
adam@364 222 (** 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 223
adamc@118 224 Print lemma1.
adamc@218 225 (** %\vspace{-.15in}% [[
adamc@118 226 lemma1 =
adamc@118 227 fun (x : A) (pf : x = elm) =>
adamc@118 228 match pf as e in (_ = y) return (0 = match e with
adamc@118 229 | refl_equal => 0
adamc@118 230 end) with
adamc@118 231 | refl_equal => refl_equal 0
adamc@118 232 end
adamc@118 233 : forall (x : A) (pf : x = elm), 0 = match pf with
adamc@118 234 | refl_equal => 0
adamc@118 235 end
adamc@218 236
adamc@118 237 ]]
adamc@118 238
adamc@118 239 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
adamc@118 240
adamc@124 241 (* begin thide *)
adamc@118 242 Definition lemma1' :=
adamc@118 243 fun (x : A) (pf : x = elm) =>
adamc@118 244 match pf return (0 = match pf with
adamc@118 245 | refl_equal => 0
adamc@118 246 end) with
adamc@118 247 | refl_equal => refl_equal 0
adamc@118 248 end.
adamc@124 249 (* end thide *)
adamc@118 250
adamc@118 251 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)
adamc@118 252
adamc@118 253 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
adamc@124 254 (* begin thide *)
adam@364 255 (** %\vspace{-.25in}%[[
adamc@118 256 simple destruct pf.
adam@364 257 ]]
adamc@205 258
adam@364 259 <<
adamc@118 260 User error: Cannot solve a second-order unification problem
adam@364 261 >>
adam@302 262 *)
adamc@118 263 Abort.
adamc@118 264
adamc@118 265 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
adamc@118 266
adamc@124 267 (* begin thide *)
adamc@124 268 Definition lemma2 :=
adamc@118 269 fun (x : A) (pf : x = x) =>
adamc@118 270 match pf return (0 = match pf with
adamc@118 271 | refl_equal => 0
adamc@118 272 end) with
adamc@118 273 | refl_equal => refl_equal 0
adamc@118 274 end.
adamc@124 275 (* end thide *)
adamc@118 276
adamc@118 277 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
adamc@118 278
adamc@118 279 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@124 280 (* begin thide *)
adam@364 281 (** %\vspace{-.25in}%[[
adamc@118 282 simple destruct pf.
adam@364 283 ]]
adamc@205 284
adam@364 285 <<
adamc@118 286 User error: Cannot solve a second-order unification problem
adam@364 287 >>
adam@364 288 %\vspace{-.15in}%*)
adamc@218 289
adamc@118 290 Abort.
adamc@118 291
adamc@118 292 (** This time, even our manual attempt fails.
adamc@118 293 [[
adamc@118 294 Definition lemma3' :=
adamc@118 295 fun (x : A) (pf : x = x) =>
adamc@118 296 match pf as pf' in (_ = x') return (pf' = refl_equal x') with
adamc@118 297 | refl_equal => refl_equal _
adamc@118 298 end.
adam@364 299 ]]
adamc@118 300
adam@364 301 <<
adamc@118 302 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
adamc@118 303 "x = x'"
adam@364 304 >>
adamc@118 305
adam@296 306 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 307
adamc@118 308 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)
adamc@118 309
adamc@118 310 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
adamc@118 311 intros; apply UIP_refl.
adamc@118 312 Qed.
adamc@118 313
adamc@118 314 Check UIP_refl.
adamc@218 315 (** %\vspace{-.15in}% [[
adamc@118 316 UIP_refl
adamc@118 317 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
adamc@118 318 ]]
adamc@118 319
adam@364 320 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 321
adamc@118 322 Print eq_rect_eq.
adamc@218 323 (** %\vspace{-.15in}% [[
adamc@118 324 eq_rect_eq =
adamc@118 325 fun U : Type => Eq_rect_eq.eq_rect_eq U
adamc@118 326 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@118 327 x = eq_rect p Q x p h
adamc@118 328 ]]
adamc@118 329
adam@364 330 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 331
adam@364 332 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@364 333 x = eq_rect p Q x p h).
adam@364 334 (** %\vspace{-.15in}%[[
adam@364 335 = forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@364 336 x = match h in (_ = y) return (Q y) with
adam@364 337 | eq_refl => x
adam@364 338 end
adam@364 339 ]]
adam@364 340
adam@364 341 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 342
adamc@118 343 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
adamc@118 344
adamc@118 345 Print Streicher_K.
adamc@124 346 (* end thide *)
adamc@218 347 (** %\vspace{-.15in}% [[
adamc@118 348 Streicher_K =
adamc@118 349 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
adamc@118 350 : forall (U : Type) (x : U) (P : x = x -> Prop),
adamc@118 351 P (refl_equal x) -> forall p : x = x, P p
adamc@118 352 ]]
adamc@118 353
adam@364 354 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 355
adamc@118 356 End fhlist_map.
adamc@118 357
adam@364 358 (** 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 359
adamc@119 360
adamc@119 361 (** * Type-Casts in Theorem Statements *)
adamc@119 362
adamc@119 363 (** 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 364
adamc@119 365 Section fhapp.
adamc@119 366 Variable A : Type.
adamc@119 367 Variable B : A -> Type.
adamc@119 368
adamc@218 369 Fixpoint fhapp (ls1 ls2 : list A)
adamc@119 370 : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
adamc@218 371 match ls1 with
adamc@119 372 | nil => fun _ hls2 => hls2
adamc@119 373 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
adamc@119 374 end.
adamc@119 375
adamc@119 376 Implicit Arguments fhapp [ls1 ls2].
adamc@119 377
adamc@124 378 (* EX: Prove that fhapp is associative. *)
adamc@124 379 (* begin thide *)
adamc@124 380
adamc@119 381 (** We might like to prove that [fhapp] is associative.
adamc@119 382 [[
adamc@119 383 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 384 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 385 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
adam@364 386 ]]
adamc@119 387
adam@364 388 <<
adamc@119 389 The term
adamc@119 390 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
adamc@119 391 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
adamc@119 392 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
adam@364 393 >>
adamc@119 394
adam@364 395 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 396
adamc@119 397 Theorem fhapp_ass : forall ls1 ls2 ls3
adamc@119 398 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
adamc@119 399 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
adamc@119 400 fhapp hls1 (fhapp hls2 hls3)
adamc@119 401 = match pf in (_ = ls) return fhlist _ ls with
adamc@119 402 | refl_equal => fhapp (fhapp hls1 hls2) hls3
adamc@119 403 end.
adamc@119 404 induction ls1; crush.
adamc@119 405
adamc@119 406 (** The first remaining subgoal looks trivial enough:
adamc@119 407 [[
adamc@119 408 ============================
adamc@119 409 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 410 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 411 | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adamc@119 412 end
adamc@119 413 ]]
adamc@119 414
adamc@119 415 We can try what worked in previous examples.
adamc@119 416 [[
adamc@119 417 case pf.
adam@364 418 ]]
adamc@119 419
adam@364 420 <<
adamc@119 421 User error: Cannot solve a second-order unification problem
adam@364 422 >>
adamc@119 423
adamc@119 424 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 425
adamc@119 426 rewrite (UIP_refl _ _ pf).
adamc@119 427 (** [[
adamc@119 428 ============================
adamc@119 429 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
adamc@119 430 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
adam@302 431 ]]
adam@302 432 *)
adamc@119 433
adamc@119 434 reflexivity.
adamc@119 435
adamc@119 436 (** Our second subgoal is trickier.
adamc@119 437 [[
adamc@119 438 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 439 ============================
adamc@119 440 (a0,
adamc@119 441 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 442 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 443 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 444 | refl_equal =>
adamc@119 445 (a0,
adamc@119 446 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 447 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 448 end
adamc@119 449
adamc@119 450 rewrite (UIP_refl _ _ pf).
adam@364 451 ]]
adamc@119 452
adam@364 453 <<
adamc@119 454 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
adamc@119 455 while it is expected to have type "?556 = ?556"
adam@364 456 >>
adamc@119 457
adamc@119 458 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 459
adamc@119 460 injection pf; intro pf'.
adamc@119 461 (** [[
adamc@119 462 pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
adamc@119 463 pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
adamc@119 464 ============================
adamc@119 465 (a0,
adamc@119 466 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
adamc@119 467 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
adamc@119 468 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 469 | refl_equal =>
adamc@119 470 (a0,
adamc@119 471 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 472 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 473 end
adamc@119 474 ]]
adamc@119 475
adamc@119 476 Now we can rewrite using the inductive hypothesis. *)
adamc@119 477
adamc@119 478 rewrite (IHls1 _ _ pf').
adamc@119 479 (** [[
adamc@119 480 ============================
adamc@119 481 (a0,
adamc@119 482 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 483 | refl_equal =>
adamc@119 484 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 485 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
adamc@119 486 end) =
adamc@119 487 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 488 | refl_equal =>
adamc@119 489 (a0,
adamc@119 490 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
adamc@119 491 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
adamc@119 492 end
adamc@119 493 ]]
adamc@119 494
adam@364 495 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 496
adamc@119 497 generalize (fhapp (fhapp b hls2) hls3).
adamc@119 498 (** [[
adamc@119 499 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
adamc@119 500 (a0,
adamc@119 501 match pf' in (_ = ls) return (fhlist B ls) with
adamc@119 502 | refl_equal => f
adamc@119 503 end) =
adamc@119 504 match pf in (_ = ls) return (fhlist B ls) with
adamc@119 505 | refl_equal => (a0, f)
adamc@119 506 end
adamc@119 507 ]]
adamc@119 508
adamc@119 509 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 510
adamc@119 511 In this case, it is helpful to generalize over our two proofs as well. *)
adamc@119 512
adamc@119 513 generalize pf pf'.
adamc@119 514 (** [[
adamc@119 515 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 516 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 517 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
adamc@119 518 (a0,
adamc@119 519 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 520 | refl_equal => f
adamc@119 521 end) =
adamc@119 522 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 523 | refl_equal => (a0, f)
adamc@119 524 end
adamc@119 525 ]]
adamc@119 526
adamc@119 527 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 528
adamc@119 529 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 530
adamc@119 531 rewrite app_ass.
adamc@119 532 (** [[
adamc@119 533 ============================
adamc@119 534 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
adamc@119 535 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
adamc@119 536 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
adamc@119 537 (a0,
adamc@119 538 match pf'0 in (_ = ls) return (fhlist B ls) with
adamc@119 539 | refl_equal => f
adamc@119 540 end) =
adamc@119 541 match pf0 in (_ = ls) return (fhlist B ls) with
adamc@119 542 | refl_equal => (a0, f)
adamc@119 543 end
adamc@119 544 ]]
adamc@119 545
adamc@119 546 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 547
adamc@119 548 intros.
adamc@119 549 rewrite (UIP_refl _ _ pf0).
adamc@119 550 rewrite (UIP_refl _ _ pf'0).
adamc@119 551 reflexivity.
adamc@119 552 Qed.
adamc@124 553 (* end thide *)
adamc@119 554 End fhapp.
adamc@120 555
adamc@120 556 Implicit Arguments fhapp [A B ls1 ls2].
adamc@120 557
adam@364 558 (** 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 559
adamc@120 560
adamc@120 561 (** * Heterogeneous Equality *)
adamc@120 562
adam@364 563 (** 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 564
adamc@120 565 Print JMeq.
adamc@218 566 (** %\vspace{-.15in}% [[
adamc@120 567 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
adamc@120 568 JMeq_refl : JMeq x x
adamc@120 569 ]]
adamc@120 570
adam@364 571 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 572
adamc@120 573 Infix "==" := JMeq (at level 70, no associativity).
adamc@120 574
adamc@124 575 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
adamc@124 576 (* begin thide *)
adamc@121 577 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
adamc@120 578 match pf return (pf == refl_equal _) with
adamc@120 579 | refl_equal => JMeq_refl _
adamc@120 580 end.
adamc@124 581 (* end thide *)
adamc@120 582
adamc@120 583 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
adamc@120 584
adamc@271 585 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 586
adamc@120 587 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
adamc@120 588 O = match pf with refl_equal => O end.
adamc@124 589 (* begin thide *)
adamc@121 590 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@120 591 Qed.
adamc@124 592 (* end thide *)
adamc@120 593
adamc@120 594 (** 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 595
adamc@120 596 Check JMeq_eq.
adamc@218 597 (** %\vspace{-.15in}% [[
adamc@120 598 JMeq_eq
adamc@120 599 : forall (A : Type) (x y : A), x == y -> x = y
adamc@218 600 ]]
adamc@120 601
adamc@218 602 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 603
adamc@120 604 We can redo our [fhapp] associativity proof based around [JMeq]. *)
adamc@120 605
adamc@120 606 Section fhapp'.
adamc@120 607 Variable A : Type.
adamc@120 608 Variable B : A -> Type.
adamc@120 609
adamc@120 610 (** This time, the naive theorem statement type-checks. *)
adamc@120 611
adamc@124 612 (* EX: Prove [fhapp] associativity using [JMeq]. *)
adamc@124 613
adamc@124 614 (* begin thide *)
adam@364 615 Theorem fhapp_ass' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)
adam@364 616 (hls3 : fhlist B ls3),
adamc@120 617 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
adamc@120 618 induction ls1; crush.
adamc@120 619
adamc@120 620 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
adamc@120 621 [[
adamc@120 622 ============================
adam@297 623 (a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
adamc@120 624 ]]
adamc@120 625
adam@297 626 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 627 [[
adamc@120 628 rewrite IHls1.
adam@364 629 ]]
adamc@120 630
adam@364 631 <<
adamc@120 632 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
adamc@120 633 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
adam@364 634 >>
adamc@120 635
adam@297 636 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 637
adamc@120 638 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 639
adamc@120 640 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 641
adamc@120 642 generalize (fhapp b (fhapp hls2 hls3))
adamc@120 643 (fhapp (fhapp b hls2) hls3)
adamc@120 644 (IHls1 _ _ b hls2 hls3).
adam@364 645 (** %\vspace{-.15in}%[[
adamc@120 646 ============================
adamc@120 647 forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
adamc@120 648 (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
adamc@120 649 ]]
adamc@120 650
adamc@120 651 Now we can rewrite with append associativity, as before. *)
adamc@120 652
adamc@120 653 rewrite app_ass.
adam@364 654 (** %\vspace{-.15in}%[[
adamc@120 655 ============================
adamc@120 656 forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
adamc@120 657 ]]
adamc@120 658
adamc@120 659 From this point, the goal is trivial. *)
adamc@120 660
adamc@120 661 intros f f0 H; rewrite H; reflexivity.
adamc@120 662 Qed.
adamc@124 663 (* end thide *)
adamc@120 664 End fhapp'.
adamc@121 665
adam@364 666 (** 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 667
adamc@121 668
adamc@121 669 (** * Equivalence of Equality Axioms *)
adamc@121 670
adamc@124 671 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
adamc@124 672
adamc@124 673 (* begin thide *)
adamc@272 674 (** 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 675
adamc@121 676 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 677
adamc@121 678 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
adamc@121 679 intros; rewrite (UIP_refl' pf); reflexivity.
adamc@121 680 Qed.
adamc@121 681
adamc@121 682 (** 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 683
adamc@121 684 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
adamc@121 685 exists pf : B = A, x = match pf with refl_equal => y end.
adamc@121 686
adamc@121 687 Infix "===" := JMeq' (at level 70, no associativity).
adamc@121 688
adamc@121 689 (** 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 690
adamc@121 691 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
adamc@121 692
adamc@121 693 (** remove printing exists *)
adamc@121 694 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
adamc@121 695 intros; unfold JMeq'; exists (refl_equal A); reflexivity.
adamc@121 696 Qed.
adamc@121 697
adamc@121 698 (** printing exists $\exists$ *)
adamc@121 699
adamc@121 700 (** 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 701
adamc@121 702 Theorem JMeq_eq' : forall (A : Type) (x y : A),
adamc@121 703 x === y -> x = y.
adamc@121 704 unfold JMeq'; intros.
adamc@121 705 (** [[
adamc@121 706 H : exists pf : A = A,
adamc@121 707 x = match pf in (_ = T) return T with
adamc@121 708 | refl_equal => y
adamc@121 709 end
adamc@121 710 ============================
adamc@121 711 x = y
adam@302 712 ]]
adam@302 713 *)
adamc@121 714
adamc@121 715 destruct H.
adamc@121 716 (** [[
adamc@121 717 x0 : A = A
adamc@121 718 H : x = match x0 in (_ = T) return T with
adamc@121 719 | refl_equal => y
adamc@121 720 end
adamc@121 721 ============================
adamc@121 722 x = y
adam@302 723 ]]
adam@302 724 *)
adamc@121 725
adamc@121 726 rewrite H.
adamc@121 727 (** [[
adamc@121 728 x0 : A = A
adamc@121 729 ============================
adamc@121 730 match x0 in (_ = T) return T with
adamc@121 731 | refl_equal => y
adamc@121 732 end = y
adam@302 733 ]]
adam@302 734 *)
adamc@121 735
adamc@121 736 rewrite (UIP_refl _ _ x0); reflexivity.
adamc@121 737 Qed.
adamc@121 738
adam@364 739 (** 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 740
adamc@124 741 (* end thide *)
adamc@123 742
adamc@123 743
adamc@123 744 (** * Equality of Functions *)
adamc@123 745
adamc@123 746 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
adamc@123 747 Theorem S_eta : S = (fun n => S n).
adamc@205 748 ]]
adamc@205 749
adam@364 750 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 751
adamc@124 752 (* begin thide *)
adamc@123 753 Axiom ext_eq : forall A B (f g : A -> B),
adamc@123 754 (forall x, f x = g x)
adamc@123 755 -> f = g.
adamc@124 756 (* end thide *)
adamc@123 757
adamc@123 758 (** 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 759
adamc@123 760 Theorem S_eta : S = (fun n => S n).
adamc@124 761 (* begin thide *)
adamc@123 762 apply ext_eq; reflexivity.
adamc@123 763 Qed.
adamc@124 764 (* end thide *)
adamc@123 765
adam@292 766 (** The same axiom can help us prove equality of types, where we need to %``%#"#reason under quantifiers.#"#%''% *)
adamc@123 767
adamc@123 768 Theorem forall_eq : (forall x : nat, match x with
adamc@123 769 | O => True
adamc@123 770 | S _ => True
adamc@123 771 end)
adamc@123 772 = (forall _ : nat, True).
adamc@123 773
adam@364 774 (** There are no immediate opportunities to apply [ext_eq], but we can use %\index{tactics!change}%[change] to fix that. *)
adamc@123 775
adamc@124 776 (* begin thide *)
adamc@123 777 change ((forall x : nat, (fun x => match x with
adamc@123 778 | 0 => True
adamc@123 779 | S _ => True
adamc@123 780 end) x) = (nat -> True)).
adamc@123 781 rewrite (ext_eq (fun x => match x with
adamc@123 782 | 0 => True
adamc@123 783 | S _ => True
adamc@123 784 end) (fun _ => True)).
adamc@123 785 (** [[
adamc@123 786 2 subgoals
adamc@123 787
adamc@123 788 ============================
adamc@123 789 (nat -> True) = (nat -> True)
adamc@123 790
adamc@123 791 subgoal 2 is:
adamc@123 792 forall x : nat, match x with
adamc@123 793 | 0 => True
adamc@123 794 | S _ => True
adamc@123 795 end = True
adam@302 796 ]]
adam@302 797 *)
adamc@123 798
adamc@123 799 reflexivity.
adamc@123 800
adamc@123 801 destruct x; constructor.
adamc@123 802 Qed.
adamc@124 803 (* end thide *)
adamc@127 804
adam@364 805 (** 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 806
adamc@127 807
adamc@127 808 (** * Exercises *)
adamc@127 809
adamc@127 810 (** %\begin{enumerate}%#<ol>#
adamc@127 811
adam@364 812 %\item%#<li># Implement and prove correct a substitution function for simply typed lambda calculus. In particular:
adamc@127 813 %\begin{enumerate}%#<ol>#
adamc@127 814 %\item%#<li># Define a datatype [type] of lambda types, including just booleans and function types.#</li>#
adamc@127 815 %\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 816 %\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 817 %\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 818 %\item%#<li># Prove that [subst] preserves program meanings. That is, prove
adamc@127 819 [[
adamc@127 820 forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts),
adamc@127 821 expDenote (subst e e') s = expDenote e (expDenote e' s ::: s)
adamc@127 822 ]]
adam@292 823 where [:::] is an infix operator for heterogeneous %``%#"#cons#"#%''% that is defined in the book's [DepList] module.#</li>#
adamc@127 824 #</ol>#%\end{enumerate}%
adamc@127 825 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 826 %\begin{enumerate}%#<ol>#
adamc@127 827 %\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 828 %\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 829 %\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 830 %\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 831 %\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 832 %\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 833 %\item%#<li># Now [subst] should be a one-liner, defined in terms of [subst'].#</li>#
adamc@127 834 %\item%#<li># Prove a correctness theorem for each auxiliary function, leading up to the proof of [subst] correctness.#</li>#
adam@292 835 %\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 836 %\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 837 %\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 838 %\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 839 #</ol>#%\end{enumerate}%
adamc@127 840 #</li>#
adamc@127 841
adamc@127 842 #</ol>#%\end{enumerate}% *)