Mercurial > cpdt > repo

comparison src/Subset.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 8077352044b2
children f923024bd284
comparison
equal deleted inserted replaced
438:f1f779c6a232 439:393b8ed99c2f
256 (* begin thide *) 256 (* begin thide *)
257 (** We build [pred_strong4] using tactic-based proving, beginning with a [Definition] command that ends in a period before a definition is given. Such a command enters the interactive proving mode, with the type given for the new identifier as our proof goal. It may seem strange to change perspective so implicitly between programming and proving, but recall that programs and proofs are two sides of the same coin in Coq, thanks to the Curry-Howard correspondence. 257 (** We build [pred_strong4] using tactic-based proving, beginning with a [Definition] command that ends in a period before a definition is given. Such a command enters the interactive proving mode, with the type given for the new identifier as our proof goal. It may seem strange to change perspective so implicitly between programming and proving, but recall that programs and proofs are two sides of the same coin in Coq, thanks to the Curry-Howard correspondence.
258 258
259 We do most of the work with the %\index{tactics!refine}%[refine] tactic, to which we pass a partial "proof" of the type we are trying to prove. There may be some pieces left to fill in, indicated by underscores. Any underscore that Coq cannot reconstruct with type inference is added as a proof subgoal. In this case, we have two subgoals: 259 We do most of the work with the %\index{tactics!refine}%[refine] tactic, to which we pass a partial "proof" of the type we are trying to prove. There may be some pieces left to fill in, indicated by underscores. Any underscore that Coq cannot reconstruct with type inference is added as a proof subgoal. In this case, we have two subgoals:
260 260
261 %\vspace{.1in} \noindent 2 \coqdockw{subgoals}\vspace{-.1in}%#<tt>2 subgoals</tt>#
262 [[ 261 [[
262 2 subgoals
263 263
264 n : nat 264 n : nat
265 _ : 0 > 0 265 _ : 0 > 0
266 ============================ 266 ============================
267 False 267 False
268 ]] 268
269 %\noindent \coqdockw{subgoal} 2 \coqdockw{is}:%#<tt>subgoal 2 is</tt># 269 subgoal 2 is
270 [[ 270
271 S n' = S n' 271 S n' = S n'
272 ]] 272 ]]
273 273
274 We can see that the first subgoal comes from the second underscore passed to [False_rec], and the second subgoal comes from the second underscore passed to [exist]. In the first case, we see that, though we bound the proof variable with an underscore, it is still available in our proof context. It is hard to refer to underscore-named variables in manual proofs, but automation makes short work of them. Both subgoals are easy to discharge that way, so let us back up and ask to prove all subgoals automatically. *) 274 We can see that the first subgoal comes from the second underscore passed to [False_rec], and the second subgoal comes from the second underscore passed to [exist]. In the first case, we see that, though we bound the proof variable with an underscore, it is still available in our proof context. It is hard to refer to underscore-named variables in manual proofs, but automation makes short work of them. Both subgoals are easy to discharge that way, so let us back up and ask to prove all subgoals automatically. *)
275 275