Equality.v 38.4 KB
Newer Older
Adam Chlipala's avatar
Adam Chlipala committed
1 2 3 4 5 6 7 8 9 10
(* Copyright (c) 2008, Adam Chlipala
 * 
 * This work is licensed under a
 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
 * Unported License.
 * The license text is available at:
 *   http://creativecommons.org/licenses/by-nc-nd/3.0/
 *)

(* begin hide *)
Adam Chlipala's avatar
Adam Chlipala committed
11
Require Import Eqdep JMeq List.
Adam Chlipala's avatar
Adam Chlipala committed
12

Adam Chlipala's avatar
Adam Chlipala committed
13
Require Import Tactics.
Adam Chlipala's avatar
Adam Chlipala committed
14 15 16 17 18 19 20 21 22 23

Set Implicit Arguments.
(* end hide *)


(** %\chapter{Reasoning About Equality Proofs}% *)

(** 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. *)


Adam Chlipala's avatar
Adam Chlipala committed
24 25 26 27 28 29 30 31 32 33 34 35 36
(** * The Definitional Equality *)

(** 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.

   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 [1] when applied to [0]. *)

Definition pred' (x : nat) :=
  match x with
    | O => O
    | S n' => let y := n' in y
  end.

Theorem reduce_me : pred' 1 = 0.
Adam Chlipala's avatar
Adam Chlipala committed
37
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
38 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 that encodes terms canonically.

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. *)
Adam Chlipala's avatar
Adam Chlipala committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92

  cbv delta.
  (** [[

  ============================
   (fun x : nat => match x with
                   | 0 => 0
                   | S n' => let y := n' in y
                   end) 1 = 0
      ]]

      At this point, we want to apply the famous beta reduction of lambda calculus, to simplify the application of a known function abstraction. *)

  cbv beta.
  (** [[

  ============================
   match 1 with
   | 0 => 0
   | S n' => let y := n' in y
   end = 0
   ]]

   Next on the list is the iota reduction, which simplifies a single [match] term by determining which pattern matches. *)

  cbv iota.
  (** [[

  ============================
   (fun n' : nat => let y := n' in y) 0 = 0
      ]]

   Now we need another beta reduction. *)

  cbv beta.
  (** [[

  ============================
   (let y := 0 in y) = 0
      ]]
   
      The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term subsituted. *)

  cbv zeta.
  (** [[

  ============================
   0 = 0
   ]] *)

  reflexivity.
Qed.
Adam Chlipala's avatar
Adam Chlipala committed
93
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
94 95 96 97 98 99

(** 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.

   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." *)


Adam Chlipala's avatar
Adam Chlipala committed
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
(** * Heterogeneous Lists Revisited *)

(** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. *)

Section fhlist.
  Variable A : Type.
  Variable B : A -> Type.

  Fixpoint fhlist (ls : list A) : Type :=
    match ls with
      | nil => unit
      | x :: ls' => B x * fhlist ls'
    end%type.

  Variable elm : A.

  Fixpoint fmember (ls : list A) : Type :=
    match ls with
      | nil => Empty_set
      | x :: ls' => (x = elm) + fmember ls'
    end%type.

  Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
    match ls return fhlist ls -> fmember ls -> B elm with
      | nil => fun _ idx => match idx with end
      | _ :: ls' => fun mls idx =>
        match idx with
          | inl pf => match pf with
                        | refl_equal => fst mls
                      end
          | inr idx' => fhget ls' (snd mls) idx'
        end
    end.
End fhlist.

Implicit Arguments fhget [A B elm ls].

(** We can define a [map]-like function for [fhlist]s. *)

Section fhlist_map.
  Variables A : Type.
  Variables B C : A -> Type.
  Variable f : forall x, B x -> C x.

  Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
    match ls return fhlist B ls -> fhlist C ls with
      | nil => fun _ => tt
      | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
    end.

  Implicit Arguments fhmap [ls].

  (** 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. *)

  Variable elm : A.

  Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
    fhget (fhmap hls) mem = f (fhget hls mem).
Adam Chlipala's avatar
Adam Chlipala committed
158
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211
    induction ls; crush.

    (** Part of our single remaining subgoal is:

       [[
   
  a0 : a = elm
  ============================
   match a0 in (_ = a2) return (C a2) with
   | refl_equal => f a1
   end = f match a0 in (_ = a2) return (B a2) with
           | refl_equal => a1
           end
       ]]

   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.

    [[

    destruct a0.

    [[
User error: Cannot solve a second-order unification problem
]]

    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.

    [[

    assert (a0 = refl_equal _).

    [[
The term "refl_equal ?98" has type "?98 = ?98"
 while it is expected to have type "a = elm"
    ]]

    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!

    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.

    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. *)

    case a0.
    (** [[

  ============================
   f a1 = f a1
   ]]

    It seems that [destruct] was trying to be too smart for its own good. *)

    reflexivity.
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
212
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
213 214 215 216

  (** It will be helpful to examine the proof terms generated by this sort of strategy.  A simpler example illustrates what is going on. *)

  Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
Adam Chlipala's avatar
Adam Chlipala committed
217
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
218 219
    simple destruct pf; reflexivity.
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
220
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241

  (** [simple destruct pf] is a convenient form for applying [case].  It runs [intro] to bring into scope all quantified variables up to its argument. *)

  Print lemma1.

  (** [[

lemma1 = 
fun (x : A) (pf : x = elm) =>
match pf as e in (_ = y) return (0 = match e with
                                     | refl_equal => 0
                                     end) with
| refl_equal => refl_equal 0
end
     : forall (x : A) (pf : x = elm), 0 = match pf with
                                          | refl_equal => 0
                                          end
    ]]

    Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)

Adam Chlipala's avatar
Adam Chlipala committed
242
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
243 244 245 246 247 248 249
  Definition lemma1' :=
    fun (x : A) (pf : x = elm) =>
      match pf return (0 = match pf with
                             | refl_equal => 0
                           end) with
        | refl_equal => refl_equal 0
      end.
Adam Chlipala's avatar
Adam Chlipala committed
250
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
251 252 253 254

  (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)

  Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
Adam Chlipala's avatar
Adam Chlipala committed
255
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
256 257 258 259 260 261 262 263 264 265 266 267
    (** [[

    simple destruct pf.
    
      [[

User error: Cannot solve a second-order unification problem
      ]] *)
  Abort.

  (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)

Adam Chlipala's avatar
Adam Chlipala committed
268 269
(* begin thide *)
  Definition lemma2 :=
Adam Chlipala's avatar
Adam Chlipala committed
270 271 272 273 274 275
    fun (x : A) (pf : x = x) =>
      match pf return (0 = match pf with
                             | refl_equal => 0
                           end) with
        | refl_equal => refl_equal 0
      end.
Adam Chlipala's avatar
Adam Chlipala committed
276
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
277 278 279 280

  (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)

  Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
Adam Chlipala's avatar
Adam Chlipala committed
281
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340
    (** [[

    simple destruct pf.
    
      [[

User error: Cannot solve a second-order unification problem
      ]] *)
  Abort.

  (** This time, even our manual attempt fails.

     [[

  Definition lemma3' :=
    fun (x : A) (pf : x = x) =>
      match pf as pf' in (_ = x') return (pf' = refl_equal x') with
        | refl_equal => refl_equal _
      end.

     [[

The term "refl_equal x'" has type "x' = x'" while it is expected to have type
 "x = x'"
     ]]

     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.

     Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)

  Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
    intros; apply UIP_refl.
  Qed.

  Check UIP_refl.
  (** [[

UIP_refl
     : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
     ]]

     [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>#%}%. *)

  Print eq_rect_eq.
  (** [[

eq_rect_eq = 
fun U : Type => Eq_rect_eq.eq_rect_eq U
     : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
       x = eq_rect p Q x p h
      ]]

      [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.

      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.

      This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)

  Print Streicher_K.
Adam Chlipala's avatar
Adam Chlipala committed
341
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
342 343 344 345 346 347 348 349 350 351 352 353
(** [[

Streicher_K = 
fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
     : forall (U : Type) (x : U) (P : x = x -> Prop),
       P (refl_equal x) -> forall p : x = x, P p
  ]]

  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. *)

End fhlist_map.

Adam Chlipala's avatar
Adam Chlipala committed
354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371

(** * Type-Casts in Theorem Statements *)

(** 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. *)

Section fhapp.
  Variable A : Type.
  Variable B : A -> Type.

  Fixpoint fhapp (ls1 ls2 : list A) {struct ls1}
    : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
    match ls1 return fhlist _ ls1 -> _ -> fhlist _ (ls1 ++ ls2) with
      | nil => fun _ hls2 => hls2
      | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
    end.

  Implicit Arguments fhapp [ls1 ls2].

Adam Chlipala's avatar
Adam Chlipala committed
372 373 374
  (* EX: Prove that fhapp is associative. *)
(* begin thide *)

Adam Chlipala's avatar
Adam Chlipala committed
375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561
  (** We might like to prove that [fhapp] is associative.

     [[

  Theorem fhapp_ass : forall ls1 ls2 ls3
    (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
    fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.

     [[

The term
 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
    hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
     ]]

     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. *)

  Theorem fhapp_ass : forall ls1 ls2 ls3
    (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
    (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
    fhapp hls1 (fhapp hls2 hls3)
    = match pf in (_ = ls) return fhlist _ ls with
        | refl_equal => fhapp (fhapp hls1 hls2) hls3
      end.
    induction ls1; crush.

    (** The first remaining subgoal looks trivial enough:

       [[

  ============================
   fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
   match pf in (_ = ls) return (fhlist B ls) with
   | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
   end
       ]]

       We can try what worked in previous examples.

       [[
    case pf.

       [[

User error: Cannot solve a second-order unification problem
         ]]

        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. *)

    rewrite (UIP_refl _ _ pf).
    (** [[

  ============================
   fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
   fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
        ]] *)

    reflexivity.

    (** Our second subgoal is trickier.

       [[

  pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
  ============================
   (a0,
   fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
     (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
   match pf in (_ = ls) return (fhlist B ls) with
   | refl_equal =>
       (a0,
       fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
         (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
   end
       ]]


       [[

    rewrite (UIP_refl _ _ pf).

       [[
The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
 while it is expected to have type "?556 = ?556"
       ]]

       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. *)

    injection pf; intro pf'.
    (** [[

  pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
  pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
  ============================
   (a0,
   fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
     (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
   match pf in (_ = ls) return (fhlist B ls) with
   | refl_equal =>
       (a0,
       fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
         (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
   end
   ]]

   Now we can rewrite using the inductive hypothesis. *)

    rewrite (IHls1 _ _ pf').
    (** [[

  ============================
   (a0,
   match pf' in (_ = ls) return (fhlist B ls) with
   | refl_equal =>
       fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
         (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
   end) =
   match pf in (_ = ls) return (fhlist B ls) with
   | refl_equal =>
       (a0,
       fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
         (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
   end
        ]]

        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. *)

    generalize (fhapp (fhapp b hls2) hls3).
    (** [[

   forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
   (a0,
   match pf' in (_ = ls) return (fhlist B ls) with
   | refl_equal => f
   end) =
   match pf in (_ = ls) return (fhlist B ls) with
   | refl_equal => (a0, f)
   end
        ]]

        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.

        In this case, it is helpful to generalize over our two proofs as well. *)

    generalize pf pf'.
    (** [[

   forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
     (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
     (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
   (a0,
   match pf'0 in (_ = ls) return (fhlist B ls) with
   | refl_equal => f
   end) =
   match pf0 in (_ = ls) return (fhlist B ls) with
   | refl_equal => (a0, f)
   end
        ]]

        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.

        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. *)

    rewrite app_ass.
    (** [[

  ============================
   forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
     (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
     (f : fhlist B (ls1 ++ ls2 ++ ls3)),
   (a0,
   match pf'0 in (_ = ls) return (fhlist B ls) with
   | refl_equal => f
   end) =
   match pf0 in (_ = ls) return (fhlist B ls) with
   | refl_equal => (a0, f)
   end
        ]]

        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]. *)

    intros.
    rewrite (UIP_refl _ _ pf0).
    rewrite (UIP_refl _ _ pf'0).
    reflexivity.
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
562
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
563
End fhapp.
Adam Chlipala's avatar
Adam Chlipala committed
564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582

Implicit Arguments fhapp [A B ls1 ls2].


(** * Heterogeneous Equality *)

(** There is another equality predicate, defined in the [JMeq] module of the standard library, implementing %\textit{%#<i>#heterogeneous equality#</i>#%}%. *)

Print JMeq.
(** [[

Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
    JMeq_refl : JMeq x x
    ]]

[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. *)

Infix "==" := JMeq (at level 70, no associativity).

Adam Chlipala's avatar
Adam Chlipala committed
583 584
(* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
585
Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
Adam Chlipala's avatar
Adam Chlipala committed
586 587 588
  match pf return (pf == refl_equal _) with
    | refl_equal => JMeq_refl _
  end.
Adam Chlipala's avatar
Adam Chlipala committed
589
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
590 591 592

(** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.

Adam Chlipala's avatar
Adam Chlipala committed
593
   Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *)
Adam Chlipala's avatar
Adam Chlipala committed
594 595 596

Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
  O = match pf with refl_equal => O end.
Adam Chlipala's avatar
Adam Chlipala committed
597
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
598
  intros; rewrite (UIP_refl' pf); reflexivity.
Adam Chlipala's avatar
Adam Chlipala committed
599
Qed.
Adam Chlipala's avatar
Adam Chlipala committed
600
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620

(** 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: *)

Check JMeq_eq.
(** [[

JMeq_eq
     : forall (A : Type) (x y : A), x == y -> x = y
    ]] *)

(** 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.

   We can redo our [fhapp] associativity proof based around [JMeq]. *)

Section fhapp'.
  Variable A : Type.
  Variable B : A -> Type.

  (** This time, the naive theorem statement type-checks. *)

Adam Chlipala's avatar
Adam Chlipala committed
621 622 623
  (* EX: Prove [fhapp] associativity using [JMeq]. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680
  Theorem fhapp_ass' : forall ls1 ls2 ls3
    (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
    fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
    induction ls1; crush.

    (** Even better, [crush] discharges the first subgoal automatically.  The second subgoal is:

       [[

  ============================
   (a0,
   fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b
     (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) ==
   (a0,
   fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3)
     (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
       ]]

       It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial.

       [[

    rewrite IHls1.

       [[

Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
       ]]

       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.

       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]. *)

    generalize (fhapp b (fhapp hls2 hls3))
      (fhapp (fhapp b hls2) hls3)
      (IHls1 _ _ b hls2 hls3).
    (** [[

  ============================
   forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
     (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
        ]]

        Now we can rewrite with append associativity, as before. *)

    rewrite app_ass.
    (** [[

  ============================
   forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
       ]]

       From this point, the goal is trivial. *)

    intros f f0 H; rewrite H; reflexivity.
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
681
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
682
End fhapp'.
Adam Chlipala's avatar
Adam Chlipala committed
683 684 685 686


(** * Equivalence of Equality Axioms *)

Adam Chlipala's avatar
Adam Chlipala committed
687 688 689
(* EX: Show that the approaches based on K and JMeq are equivalent logically. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754
(** 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.

   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. *)

Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
  intros; rewrite (UIP_refl' pf); reflexivity.
Qed.

(** 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. *)

Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
  exists pf : B = A, x = match pf with refl_equal => y end.

Infix "===" := JMeq' (at level 70, no associativity).

(** 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.

   We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)

(** remove printing exists *)
Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
  intros; unfold JMeq'; exists (refl_equal A); reflexivity.
Qed.

(** printing exists $\exists$ *)

(** The proof of an analogue to [JMeq_eq] is a little more interesting, but most of the action is in appealing to [UIP_refl]. *)

Theorem JMeq_eq' : forall (A : Type) (x y : A),
  x === y -> x = y.
  unfold JMeq'; intros.
  (** [[

  H : exists pf : A = A,
        x = match pf in (_ = T) return T with
            | refl_equal => y
            end
  ============================
   x = y
      ]] *)

  destruct H.
  (** [[

  x0 : A = A
  H : x = match x0 in (_ = T) return T with
          | refl_equal => y
          end
  ============================
   x = y
      ]] *)

  rewrite H.
  (** [[

  x0 : A = A
  ============================
   match x0 in (_ = T) return T with
   | refl_equal => y
   end = y
      ]] *)

  rewrite (UIP_refl _ _ x0); reflexivity.
Qed.

Adam Chlipala's avatar
Adam Chlipala committed
755 756 757
(** 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.

   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. *)
Adam Chlipala's avatar
Adam Chlipala committed
758
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
759 760 761 762 763 764 765 766 767 768


(** * Equality of Functions *)

(** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[

   Theorem S_eta : S = (fun n => S n).

   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. *)

Adam Chlipala's avatar
Adam Chlipala committed
769
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
770 771 772
Axiom ext_eq : forall A B (f g : A -> B),
  (forall x, f x = g x)
  -> f = g.
Adam Chlipala's avatar
Adam Chlipala committed
773
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
774 775 776 777

(** 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. *)

Theorem S_eta : S = (fun n => S n).
Adam Chlipala's avatar
Adam Chlipala committed
778
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
779 780
  apply ext_eq; reflexivity.
Qed.
Adam Chlipala's avatar
Adam Chlipala committed
781
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
782 783 784 785 786 787 788 789 790 791 792

(** The same axiom can help us prove equality of types, where we need to "reason under quantifiers." *)

Theorem forall_eq : (forall x : nat, match x with
                                      | O => True
                                      | S _ => True
                                    end)
  = (forall _ : nat, True).

  (** There are no immediate opportunities to apply [ext_eq], but we can use [change] to fix that. *)

Adam Chlipala's avatar
Adam Chlipala committed
793
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820
  change ((forall x : nat, (fun x => match x with
                                       | 0 => True
                                       | S _ => True
                                     end) x) = (nat -> True)).
  rewrite (ext_eq (fun x => match x with
                              | 0 => True
                              | S _ => True
                            end) (fun _ => True)).
  (** [[

2 subgoals
  
  ============================
   (nat -> True) = (nat -> True)

subgoal 2 is:
 forall x : nat, match x with
                 | 0 => True
                 | S _ => True
                 end = True
      ]] *)


  reflexivity.

  destruct x; constructor.
Qed.
Adam Chlipala's avatar
Adam Chlipala committed
821
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858


(** * Exercises *)

(** %\begin{enumerate}%#<ol>#

%\item%#<li># Implement and prove correct a substitution function for simply-typed lambda calculus.  In particular:
%\begin{enumerate}%#<ol>#
  %\item%#<li># Define a datatype [type] of lambda types, including just booleans and function types.#</li>#
  %\item%#<li># Define a type family [exp : list type -> type -> Type] of lambda expressions, including boolean constants, variables, and function application and abstraction.#</li>#
  %\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>#
  %\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>#
  %\item%#<li># Prove that [subst] preserves program meanings.  That is, prove
  [[
forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts),
  expDenote (subst e e') s = expDenote e (expDenote e' s ::: s)
  ]]
  where [:::] is an infix operator for heterogeneous "cons" that is defined in the book's [DepList] module.#</li>#
#</ol>#%\end{enumerate}%
  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.
%\begin{enumerate}%#<ol>#
  %\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>#
  %\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>#
  %\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>#
  %\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>#
  %\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>#
  %\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>#
  %\item%#<li># Now [subst] should be a one-liner, defined in terms of [subst'].#</li>#
  %\item%#<li># Prove a correctness theorem for each auxiliary function, leading up to the proof of [subst] correctness.#</li>#
  %\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>#
  %\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>#
  %\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>#
  %\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>#
#</ol>#%\end{enumerate}%
#</li>#
   
#</ol>#%\end{enumerate}% *)