Mercurial > cpdt > repo

comparison src/Match.v @ 445:0650420c127b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished vertical spacing
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Aug 2012 17:31:56 -0400
parents 8077352044b2
children 38549f152568
comparison
equal deleted inserted replaced
444:0d66f1a710b8 445:0650420c127b
265 Hypothesis H1 : forall x, P x -> Q x /\ R x. 265 Hypothesis H1 : forall x, P x -> Q x /\ R x.
266 Hypothesis H2 : forall x, R x -> S x. 266 Hypothesis H2 : forall x, R x -> S x.
267 267
268 Theorem fo' : forall x, P x -> S x. 268 Theorem fo' : forall x, P x -> S x.
269 (* begin thide *) 269 (* begin thide *)
270 (** [[ 270 (** %\vspace{-.25in}%[[
271 completer'. 271 completer'.
272
273 ]] 272 ]]
274 273 %\vspace{-.15in}%Coq loops forever at this point. What went wrong? *)
275 Coq loops forever at this point. What went wrong? *)
276 274
277 Abort. 275 Abort.
278 (* end thide *) 276 (* end thide *)
279 End firstorder'. 277 End firstorder'.
280 278
290 288
291 (** This one fails. *) 289 (** This one fails. *)
292 290
293 (* begin thide *) 291 (* begin thide *)
294 Theorem t1' : forall x : nat, x = x. 292 Theorem t1' : forall x : nat, x = x.
295 (** [[ 293 (** %\vspace{-.25in}%[[
296 match goal with 294 match goal with
297 | [ |- forall x, ?P ] => trivial 295 | [ |- forall x, ?P ] => trivial
298 end. 296 end.
299 ]] 297 ]]
300 298
318 (* EX: Write a list length function in Ltac. *) 316 (* EX: Write a list length function in Ltac. *)
319 317
320 (** Ltac supports quite convenient functional programming, with a Lisp-with-syntax kind of flavor. However, there are a few syntactic conventions involved in getting programs to be accepted. The Ltac syntax is optimized for tactic-writing, so one has to deal with some inconveniences in writing more standard functional programs. 318 (** Ltac supports quite convenient functional programming, with a Lisp-with-syntax kind of flavor. However, there are a few syntactic conventions involved in getting programs to be accepted. The Ltac syntax is optimized for tactic-writing, so one has to deal with some inconveniences in writing more standard functional programs.
321 319
322 To illustrate, let us try to write a simple list length function. We start out writing it just like in Gallina, simply replacing [Fixpoint] (and its annotations) with [Ltac]. 320 To illustrate, let us try to write a simple list length function. We start out writing it just like in Gallina, simply replacing [Fixpoint] (and its annotations) with [Ltac].
323
324 [[ 321 [[
325 Ltac length ls := 322 Ltac length ls :=
326 match ls with 323 match ls with
327 | nil => O 324 | nil => O
328 | _ :: ls' => S (length ls') 325 | _ :: ls' => S (length ls')
332 << 329 <<
333 Error: The reference ls' was not found in the current environment 330 Error: The reference ls' was not found in the current environment
334 >> 331 >>
335 332
336 At this point, we hopefully remember that pattern variable names must be prefixed by question marks in Ltac. 333 At this point, we hopefully remember that pattern variable names must be prefixed by question marks in Ltac.
337
338 [[ 334 [[
339 Ltac length ls := 335 Ltac length ls :=
340 match ls with 336 match ls with
341 | nil => O 337 | nil => O
342 | _ :: ?ls' => S (length ls') 338 | _ :: ?ls' => S (length ls')
354 match ls with 350 match ls with
355 | nil => O 351 | nil => O
356 | _ :: ?ls' => constr:(S (length ls')) 352 | _ :: ?ls' => constr:(S (length ls'))
357 end. 353 end.
358 354
359 (** This definition is accepted. It can be a little awkward to test Ltac definitions like this. Here is one method. *) 355 (** This definition is accepted. It can be a little awkward to test Ltac definitions like this one. Here is one method. *)
360 356
361 Goal False. 357 Goal False.
362 let n := length (1 :: 2 :: 3 :: nil) in 358 let n := length (1 :: 2 :: 3 :: nil) in
363 pose n. 359 pose n.
364 (** [[ 360 (** [[
365 n := S (length (2 :: 3 :: nil)) : nat 361 n := S (length (2 :: 3 :: nil)) : nat
366 ============================ 362 ============================
367 False 363 False
368
369 ]] 364 ]]
370 365
371 We use the %\index{tactics!pose}%[pose] tactic, which extends the proof context with a new variable that is set equal to a particular term. We could also have used [idtac n] in place of [pose n], which would have printed the result without changing the context. 366 We use the %\index{tactics!pose}%[pose] tactic, which extends the proof context with a new variable that is set equal to a particular term. We could also have used [idtac n] in place of [pose n], which would have printed the result without changing the context.
372 367
373 The value of [n] only has the length calculation unrolled one step. What has happened here is that, by escaping into the [constr] nonterminal, we referred to the [length] function of Gallina, rather than the [length] Ltac function that we are defining. *) 368 The value of [n] only has the length calculation unrolled one step. What has happened here is that, by escaping into the [constr] nonterminal, we referred to the [length] function of Gallina, rather than the [length] Ltac function that we are defining. *)
887 882
888 << 883 <<
889 No more subgoals but non-instantiated existential variables : 884 No more subgoals but non-instantiated existential variables :
890 Existential 1 = 885 Existential 1 =
891 >> 886 >>
892 [[ 887 %\vspace{-.35in}%[[
893 ?4384 : [A : Type 888 ?4384 : [A : Type
894 B : Type 889 B : Type
895 Q : A -> Prop 890 Q : A -> Prop
896 P : A -> B -> Prop 891 P : A -> B -> Prop
897 f : A -> A -> A 892 f : A -> A -> A
902 v1 : A 897 v1 : A
903 v2 : A 898 v2 : A
904 H : Q v1 899 H : Q v1
905 H0 : Q v2 900 H0 : Q v2
906 H' : Q v2 -> exists u : B, P v2 u |- Q v2] 901 H' : Q v2 -> exists u : B, P v2 u |- Q v2]
907
908 ]] 902 ]]
909 903
910 There is another similar line about a different existential variable. Here, "existential variable" means what we have also called "unification variable." In the course of the proof, some unification variable [?4384] was introduced but never unified. Unification variables are just a device to structure proof search; the language of Gallina proof terms does not include them. Thus, we cannot produce a proof term without instantiating the variable. 904 There is another similar line about a different existential variable. Here, "existential variable" means what we have also called "unification variable." In the course of the proof, some unification variable [?4384] was introduced but never unified. Unification variables are just a device to structure proof search; the language of Gallina proof terms does not include them. Thus, we cannot produce a proof term without instantiating the variable.
911 905
912 The error message shows that [?4384] is meant to be a proof of [Q v2] in a particular proof state, whose variables and hypotheses are displayed. It turns out that [?4384] was created by [insterU], as the value of a proof to pass to [H1]. Recall that, in Gallina, implication is just a degenerate case of [forall] quantification, so the [insterU] code to match against [forall] also matched the implication. Since any proof of [Q v2] is as good as any other in this context, there was never any opportunity to use unification to determine exactly which proof is appropriate. We expect similar problems with any implications in arguments to [insterU]. *) 906 The error message shows that [?4384] is meant to be a proof of [Q v2] in a particular proof state, whose variables and hypotheses are displayed. It turns out that [?4384] was created by [insterU], as the value of a proof to pass to [H1]. Recall that, in Gallina, implication is just a degenerate case of [forall] quantification, so the [insterU] code to match against [forall] also matched the implication. Since any proof of [Q v2] is as good as any other in this context, there was never any opportunity to use unification to determine exactly which proof is appropriate. We expect similar problems with any implications in arguments to [insterU]. *)