Mercurial > cpdt > repo

comparison src/Equality.v @ 205:f05514cc6c0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'make doc' works with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 12:15:05 -0500
parents cadeb49dc1ef
children c8508d277a00
comparison
equal deleted inserted replaced
204:cbf2f74a5130 205:f05514cc6c0d
175 175
176 [[ 176 [[
177 177
178 destruct a0. 178 destruct a0.
179 179
180 ]]
181
180 [[ 182 [[
181 User error: Cannot solve a second-order unification problem 183 User error: Cannot solve a second-order unification problem
182 ]] 184 ]]
183 185
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. 186 This is one of Coq's standard error messages for informing us that its heuristics for attempting an instance of an undecidable problem about dependent typing have failed. We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
185 187
186 [[ 188 [[
187 189
188 assert (a0 = refl_equal _). 190 assert (a0 = refl_equal _).
191
192 ]]
189 193
190 [[ 194 [[
191 The term "refl_equal ?98" has type "?98 = ?98" 195 The term "refl_equal ?98" has type "?98 = ?98"
192 while it is expected to have type "a = elm" 196 while it is expected to have type "a = elm"
193 ]] 197 ]]
254 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end. 258 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
255 (* begin thide *) 259 (* begin thide *)
256 (** [[ 260 (** [[
257 261
258 simple destruct pf. 262 simple destruct pf.
263
264 ]]
259 265
260 [[ 266 [[
261 267
262 User error: Cannot solve a second-order unification problem 268 User error: Cannot solve a second-order unification problem
263 ]] *) 269 ]] *)
280 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x. 286 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
281 (* begin thide *) 287 (* begin thide *)
282 (** [[ 288 (** [[
283 289
284 simple destruct pf. 290 simple destruct pf.
291
292 ]]
285 293
286 [[ 294 [[
287 295
288 User error: Cannot solve a second-order unification problem 296 User error: Cannot solve a second-order unification problem
289 ]] *) 297 ]] *)
296 Definition lemma3' := 304 Definition lemma3' :=
297 fun (x : A) (pf : x = x) => 305 fun (x : A) (pf : x = x) =>
298 match pf as pf' in (_ = x') return (pf' = refl_equal x') with 306 match pf as pf' in (_ = x') return (pf' = refl_equal x') with
299 | refl_equal => refl_equal _ 307 | refl_equal => refl_equal _
300 end. 308 end.
309
310 ]]
301 311
302 [[ 312 [[
303 313
304 The term "refl_equal x'" has type "x' = x'" while it is expected to have type 314 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
305 "x = x'" 315 "x = x'"
377 [[ 387 [[
378 388
379 Theorem fhapp_ass : forall ls1 ls2 ls3 389 Theorem fhapp_ass : forall ls1 ls2 ls3
380 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3), 390 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
381 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3. 391 fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
392
393 ]]
382 394
383 [[ 395 [[
384 396
385 The term 397 The term
386 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2) 398 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
412 424
413 We can try what worked in previous examples. 425 We can try what worked in previous examples.
414 426
415 [[ 427 [[
416 case pf. 428 case pf.
429
430 ]]
417 431
418 [[ 432 [[
419 433
420 User error: Cannot solve a second-order unification problem 434 User error: Cannot solve a second-order unification problem
421 ]] 435 ]]
451 465
452 466
453 [[ 467 [[
454 468
455 rewrite (UIP_refl _ _ pf). 469 rewrite (UIP_refl _ _ pf).
470
471 ]]
456 472
457 [[ 473 [[
458 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3" 474 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
459 while it is expected to have type "?556 = ?556" 475 while it is expected to have type "?556 = ?556"
460 ]] 476 ]]
643 659
644 [[ 660 [[
645 661
646 rewrite IHls1. 662 rewrite IHls1.
647 663
664 ]]
665
648 [[ 666 [[
649 667
650 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with 668 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
651 "fhlist B (ls1 ++ ?1572 ++ ?1573)" 669 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
652 ]] 670 ]]
761 (** * Equality of Functions *) 779 (** * Equality of Functions *)
762 780
763 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[ 781 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
764 782
765 Theorem S_eta : S = (fun n => S n). 783 Theorem S_eta : S = (fun n => S n).
784
785 ]]
766 786
767 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. *) 787 Unfortunately, this theorem is not provable in CIC without additional axioms. None of the definitional equality rules force function equality to be %\textit{%#<i>#extensional#</i>#%}%. That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal. We %\textit{%#<i>#can#</i>#%}% assert function extensionality as an axiom. *)
768 788
769 (* begin thide *) 789 (* begin thide *)
770 Axiom ext_eq : forall A B (f g : A -> B), 790 Axiom ext_eq : forall A B (f g : A -> B),