Mercurial > cpdt > repo

comparison src/Large.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 4662b6f099b0
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
121 (** [[ 121 (** [[
122 rewrite IHe1. 122 rewrite IHe1.
123 123
124 Error: The reference IHe1 was not found in the current environment. 124 Error: The reference IHe1 was not found in the current environment.
125 125
126 ]] *) 126 ]]
127 *)
127 128
128 Abort. 129 Abort.
129 130
130 (** Can you spot what went wrong, without stepping through the script step-by-step? The problem is that [trivial] never fails. Originally, [trivial] had been succeeding in proving an equality that follows by reflexivity. Our change to [times] leads to a case where that equality is no longer true. [trivial] happily leaves the false equality in place, and we continue on to the span of tactics intended for the second inductive case. Unfortunately, those tactics end up being applied to the %\textit{%#<i>#first#</i>#%}% case instead. 131 (** Can you spot what went wrong, without stepping through the script step-by-step? The problem is that [trivial] never fails. Originally, [trivial] had been succeeding in proving an equality that follows by reflexivity. Our change to [times] leads to a case where that equality is no longer true. [trivial] happily leaves the false equality in place, and we continue on to the span of tactics intended for the second inductive case. Unfortunately, those tactics end up being applied to the %\textit{%#<i>#first#</i>#%}% case instead.
131 132
182 trivial 183 trivial
183 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ]. 184 | simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
184 185
185 Error: Expects a disjunctive pattern with 3 branches. 186 Error: Expects a disjunctive pattern with 3 branches.
186 187
187 ]] *) 188 ]]
189 *)
188 190
189 Abort. 191 Abort.
190 192
191 (** Unsurprisingly, the old proof fails, because it explicitly says that there are two inductive cases. To update the script, we must, at a minimum, remember the order in which the inductive cases are generated, so that we can insert the new case in the appropriate place. Even then, it will be painful to add the case, because we cannot walk through proof steps interactively when they occur inside an explicit set of cases. *) 193 (** Unsurprisingly, the old proof fails, because it explicitly says that there are two inductive cases. To update the script, we must, at a minimum, remember the order in which the inductive cases are generated, so that we can insert the new case in the appropriate place. Even then, it will be painful to add the case, because we cannot walk through proof steps interactively when they occur inside an explicit set of cases. *)
192 194
538 540
539 Lemma slow : forall x y, P x y -> Q x y -> S x y -> f x = f y. 541 Lemma slow : forall x y, P x y -> Q x y -> S x y -> f x = f y.
540 Time eauto 6. 542 Time eauto 6.
541 (** [[ 543 (** [[
542 Finished transaction in 0. secs (0.068004u,0.s) 544 Finished transaction in 0. secs (0.068004u,0.s)
543 ]] *) 545 ]]
546 *)
544 547
545 Qed. 548 Qed.
546 549
547 (** Now we add a different hypothesis, which is innocent enough; in fact, it is even provable as a theorem. *) 550 (** Now we add a different hypothesis, which is innocent enough; in fact, it is even provable as a theorem. *)
548 551
720 723
721 Check IntTheorems.unique_ident. 724 Check IntTheorems.unique_ident.
722 (** %\vspace{-.15in}% [[ 725 (** %\vspace{-.15in}% [[
723 IntTheorems.unique_ident 726 IntTheorems.unique_ident
724 : forall e' : Int.G, (forall a : Int.G, Int.f e' a = a) -> e' = Int.e 727 : forall e' : Int.G, (forall a : Int.G, Int.f e' a = a) -> e' = Int.e
725 ]] *) 728 ]]
729 *)
726 730
727 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0. 731 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0.
728 exact IntTheorems.unique_ident. 732 exact IntTheorems.unique_ident.
729 Qed. 733 Qed.
730 734