Mercurial > cpdt > repo

comparison src/Equality.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents 123f466faedc
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
85 cbv zeta. 85 cbv zeta.
86 (** [[ 86 (** [[
87 ============================ 87 ============================
88 0 = 0 88 0 = 0
89 89
90 ]] *) 90 ]]
91 *)
91 92
92 reflexivity. 93 reflexivity.
93 Qed. 94 Qed.
94 (* end thide *) 95 (* end thide *)
95 96
215 It seems that [destruct] was trying to be too smart for its own good. 216 It seems that [destruct] was trying to be too smart for its own good.
216 217
217 [[ 218 [[
218 reflexivity. 219 reflexivity.
219 220
220 ]] *) 221 ]]
222 *)
221 223
222 Qed. 224 Qed.
223 (* end thide *) 225 (* end thide *)
224 226
225 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *) 227 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *)
266 (** [[ 268 (** [[
267 simple destruct pf. 269 simple destruct pf.
268 270
269 User error: Cannot solve a second-order unification problem 271 User error: Cannot solve a second-order unification problem
270 272
271 ]] *) 273 ]]
274 *)
272 Abort. 275 Abort.
273 276
274 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *) 277 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
275 278
276 (* begin thide *) 279 (* begin thide *)
289 (* begin thide *) 292 (* begin thide *)
290 (** [[ 293 (** [[
291 simple destruct pf. 294 simple destruct pf.
292 295
293 User error: Cannot solve a second-order unification problem 296 User error: Cannot solve a second-order unification problem
294 ]] *) 297 ]]
298 *)
295 299
296 Abort. 300 Abort.
297 301
298 (** This time, even our manual attempt fails. 302 (** This time, even our manual attempt fails.
299 303
427 (** [[ 431 (** [[
428 ============================ 432 ============================
429 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 = 433 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
430 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 434 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
431 435
432 ]] *) 436 ]]
437 *)
433 438
434 reflexivity. 439 reflexivity.
435 440
436 (** Our second subgoal is trickier. 441 (** Our second subgoal is trickier.
437 442
714 | refl_equal => y 719 | refl_equal => y
715 end 720 end
716 ============================ 721 ============================
717 x = y 722 x = y
718 723
719 ]] *) 724 ]]
725 *)
720 726
721 destruct H. 727 destruct H.
722 (** [[ 728 (** [[
723 x0 : A = A 729 x0 : A = A
724 H : x = match x0 in (_ = T) return T with 730 H : x = match x0 in (_ = T) return T with
725 | refl_equal => y 731 | refl_equal => y
726 end 732 end
727 ============================ 733 ============================
728 x = y 734 x = y
729 735
730 ]] *) 736 ]]
737 *)
731 738
732 rewrite H. 739 rewrite H.
733 (** [[ 740 (** [[
734 x0 : A = A 741 x0 : A = A
735 ============================ 742 ============================
736 match x0 in (_ = T) return T with 743 match x0 in (_ = T) return T with
737 | refl_equal => y 744 | refl_equal => y
738 end = y 745 end = y
739 746
740 ]] *) 747 ]]
748 *)
741 749
742 rewrite (UIP_refl _ _ x0); reflexivity. 750 rewrite (UIP_refl _ _ x0); reflexivity.
743 Qed. 751 Qed.
744 752
745 (** 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. 753 (** 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.
799 subgoal 2 is: 807 subgoal 2 is:
800 forall x : nat, match x with 808 forall x : nat, match x with
801 | 0 => True 809 | 0 => True
802 | S _ => True 810 | S _ => True
803 end = True 811 end = True
804 ]] *) 812 ]]
813 *)
805 814
806 reflexivity. 815 reflexivity.
807 816
808 destruct x; constructor. 817 destruct x; constructor.
809 Qed. 818 Qed.