Mercurial > cpdt > repo

comparison src/Predicates.v @ 439:393b8ed99c2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of improvements to vertical spacing, up through end of InductiveTypes
author Adam Chlipala <adam@chlipala.net>
date Mon, 30 Jul 2012 13:21:36 -0400
parents 5f25705a10ea
children f923024bd284
comparison
equal deleted inserted replaced
438:f1f779c6a232 439:393b8ed99c2f
172 ]] 172 ]]
173 173
174 Every proof of a conjunction provides proofs for both conjuncts, so we get a single subgoal reflecting that. We can proceed by splitting this subgoal into a case for each conjunct of [Q /\ P].%\index{tactics!split}% *) 174 Every proof of a conjunction provides proofs for both conjuncts, so we get a single subgoal reflecting that. We can proceed by splitting this subgoal into a case for each conjunct of [Q /\ P].%\index{tactics!split}% *)
175 175
176 split. 176 split.
177 (** %\vspace{.1in} \noindent 2 \coqdockw{subgoals}\vspace{-.1in}%#<tt>2 subgoals</tt># 177 (** 2 subgoals
178 [[
179 178
180 H : P 179 H : P
181 H0 : Q 180 H0 : Q
182 ============================ 181 ============================
183 Q 182 Q
184 ]] 183
185 %\noindent \coqdockw{subgoal} 2 \coqdockw{is}:%#<tt>subgoal 2 is</tt># 184 subgoal 2 is
186 [[ 185
187 P 186 P
188 187
189 ]] 188 ]]
190 189
191 In each case, the conclusion is among our hypotheses, so the %\index{tactics!assumption}%[assumption] tactic finishes the process. *) 190 In each case, the conclusion is among our hypotheses, so the %\index{tactics!assumption}%[assumption] tactic finishes the process. *)
210 209
211 (* begin thide *) 210 (* begin thide *)
212 (** As in the proof for [and], we begin with case analysis, though this time we are met by two cases instead of one. *) 211 (** As in the proof for [and], we begin with case analysis, though this time we are met by two cases instead of one. *)
213 212
214 destruct 1. 213 destruct 1.
215 (** %\vspace{.1in} \noindent 2 \coqdockw{subgoals}\vspace{-.1in}%#<tt>2 subgoals</tt># 214 (** [[
216 [[ 215 2 subgoals
217 216
218 H : P 217 H : P
219 ============================ 218 ============================
220 Q \/ P 219 Q \/ P
221 ]] 220
222 %\noindent \coqdockw{subgoal} 2 \coqdockw{is}:%#<tt>subgoal 2 is</tt># 221 subgoal 2 is
223 [[ 222
224 Q \/ P 223 Q \/ P
225 224
226 ]] 225 ]]
227 226
228 We can see that, in the first subgoal, we want to prove the disjunction by proving its second disjunct. The %\index{tactics!right}%[right] tactic telegraphs this intent. *) 227 We can see that, in the first subgoal, we want to prove the disjunction by proving its second disjunct. The %\index{tactics!right}%[right] tactic telegraphs this intent. *)