Mercurial > cpdt > repo

comparison src/Large.v @ 240:b28c6e6eca0c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New-rewrite-hint-breaks-old-script example
author Adam Chlipala <adamc@hcoop.net>
date Wed, 09 Dec 2009 11:06:39 -0500
parents a3f0cdcb09c3
children cb3f3ef9d5bb
comparison
equal deleted inserted replaced
239:a3f0cdcb09c3 240:b28c6e6eca0c
399 | None => _ end] ] => 399 | None => _ end] ] =>
400 dep_destruct E 400 dep_destruct E
401 end; crush). 401 end; crush).
402 Qed. 402 Qed.
403 403
404 (** Even after we put together nice automated proofs, we must deal with specification changes that can invalidate them. It is not generally possible to step through single-tactic proofs interactively. There is a command [Debug On] that lets us step through points in tactic execution, but the debugger tends to make counterintuitive choices of which points we would like to stop at, and per-point output is quite verbose, so most Coq users do not find this debugging mode very helpful. How are we to understand what has broken in a script that used to work?
405
406 An example helps demonstrate a useful approach. Consider what would have happened in our proof of [reassoc_correct] if we had first added an unfortunate rewriting hint. *)
407
408 Reset reassoc_correct.
409
410 Theorem confounder : forall e1 e2 e3,
411 eval e1 * eval e2 * eval e3 = eval e1 * (eval e2 + 1 - 1) * eval e3.
412 crush.
413 Qed.
414
415 Hint Rewrite confounder : cpdt.
416
417 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
418 induction e; crush;
419 match goal with
420 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _ | Mult _ _ => _ end] ] =>
421 destruct E; crush
422 end.
423
424 (** One subgoal remains:
425
426 [[
427 ============================
428 eval e1 * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2
429
430 ]]
431
432 The poorly-chosen rewrite rule fired, changing the goal to a form where another hint no longer applies. Imagine that we are in the middle of a large development with many hints. How would we diagnose the problem? First, we might not be sure which case of the inductive proof has gone wrong. It is useful to separate out our automation procedure and apply it manually. *)
433
434 Restart.
435
436 Ltac t := crush; match goal with
437 | [ |- context[match ?E with Const _ => _ | Plus _ _ => _
438 | Mult _ _ => _ end] ] =>
439 destruct E; crush
440 end.
441
442 induction e.
443
444 (** Since we see the subgoals before any simplification occurs, it is clear that this is the case for constants. [t] makes short work of it. *)
445
446 t.
447
448 (** The next subgoal, for addition, is also discharged without trouble. *)
449
450 t.
451
452 (** The final subgoal is for multiplication, and it is here that we get stuck in the proof state summarized above. *)
453
454 t.
455
456 (** What is [t] doing to get us to this point? The [info] command can help us answer this kind of question. *)
457
458 (** remove printing * *)
459 Undo.
460 info t.
461 (** [[
462 == simpl in *; intuition; subst; autorewrite with cpdt in *;
463 simpl in *; intuition; subst; autorewrite with cpdt in *;
464 simpl in *; intuition; subst; destruct (reassoc e2).
465 simpl in *; intuition.
466
467 simpl in *; intuition.
468
469 simpl in *; intuition; subst; autorewrite with cpdt in *;
470 refine (eq_ind_r
471 (fun n : nat =>
472 n * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2) _ IHe1);
473 autorewrite with cpdt in *; simpl in *; intuition;
474 subst; autorewrite with cpdt in *; simpl in *;
475 intuition; subst.
476
477 ]]
478
479 A detailed trace of [t]'s execution appears. Since we are using the very general [crush] tactic, many of these steps have no effect and only occur as instances of a more general strategy. We can copy-and-paste the details to see where things go wrong. *)
480
481 Undo.
482
483 (** We arbitrarily split the script into chunks. The first few seem not to do any harm. *)
484
485 simpl in *; intuition; subst; autorewrite with cpdt in *.
486 simpl in *; intuition; subst; autorewrite with cpdt in *.
487 simpl in *; intuition; subst; destruct (reassoc e2).
488 simpl in *; intuition.
489 simpl in *; intuition.
490
491 (** The next step is revealed as the culprit, bringing us to the final unproved subgoal. *)
492
493 simpl in *; intuition; subst; autorewrite with cpdt in *.
494
495 (** We can split the steps further to assign blame. *)
496
497 Undo.
498
499 simpl in *.
500 intuition.
501 subst.
502 autorewrite with cpdt in *.
503
504 (** It was the final of these four tactics that made the rewrite. We can find out exactly what happened. The [info] command presents hierarchical views of proof steps, and we can zoom down to a lower level of detail by applying [info] to one of the steps that appeared in the original trace. *)
505
506 Undo.
507
508 info autorewrite with cpdt in *.
509 (** [[
510 == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
511 (confounder (reassoc e1) e3 e4)).
512
513 ]]
514
515 The way a rewrite is displayed is somewhat baroque, but we can see that theorem [confounder] is the final culprit. At this point, we could remove that hint, prove an alternate version of the key lemma [rewr], or come up with some other remedy. Fixing this kind of problem tends to be relatively easy once the problem is revealed. *)
516
517 Abort.
518
519 (** printing * $\times$ *)
520
404 Section slow. 521 Section slow.
405 Hint Resolve trans_eq. 522 Hint Resolve trans_eq.
406 523
407 Variable A : Set. 524 Variable A : Set.
408 Variables P Q R S : A -> A -> Prop. 525 Variables P Q R S : A -> A -> Prop.