Mercurial > cpdt > repo

comparison src/StackMachine.v @ 328:cbeccef45f4e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass over Match
author Adam Chlipala <adam@chlipala.net>
date Sun, 25 Sep 2011 13:20:56 -0400
parents 2aaff91f5258
children 7e57c909f0f2
comparison
equal deleted inserted replaced
327:5cdfbf56afbe 328:cbeccef45f4e
503 Lemma compile_correct' : forall e s p, progDenote (compile e ++ p) s = 503 Lemma compile_correct' : forall e s p, progDenote (compile e ++ p) s =
504 progDenote p (expDenote e :: s). 504 progDenote p (expDenote e :: s).
505 induction e; crush. 505 induction e; crush.
506 Qed. 506 Qed.
507 507
508 (** We need only to state the basic inductive proof scheme and call a tactic that automates the tedious reasoning in between. In contrast to the period tactic terminator from our last proof, the %\index{tacticals!semicolon}%semicolon tactic separator supports structured, compositional proofs. The tactic [t1; t2] has the effect of running [t1] and then running [t2] on each remaining subgoal. The semicolon is one of the most fundamental building blocks of effective proof automation. The period terminator is very useful for exploratory proving, where you need to see intermediate proof states, but final proofs of any serious complexity should have just one period, terminating a single compound tactic that probably uses semicolons. 508 (** We need only to state the basic inductive proof scheme and call a tactic that automates the tedious reasoning in between. In contrast to the period tactic terminator from our last proof, the %\index{tactics!semicolon}%semicolon tactic separator supports structured, compositional proofs. The tactic [t1; t2] has the effect of running [t1] and then running [t2] on each remaining subgoal. The semicolon is one of the most fundamental building blocks of effective proof automation. The period terminator is very useful for exploratory proving, where you need to see intermediate proof states, but final proofs of any serious complexity should have just one period, terminating a single compound tactic that probably uses semicolons.
509 509
510 The [crush] tactic comes from the library associated with this book and is not part of the Coq standard library. The book's library contains a number of other tactics that are especially helpful in highly-automated proofs. 510 The [crush] tactic comes from the library associated with this book and is not part of the Coq standard library. The book's library contains a number of other tactics that are especially helpful in highly-automated proofs.
511 511
512 The %\index{Vernacular commands!Qed}%[Qed] command checks that the proof is finished and, if so, saves it. The tactic commands we have written above are an example of a %\emph{%#<i>#proof script#</i>#%}%, or a series of Ltac programs; while [Qed] uses the result of the script to generate a %\emph{%#<i>#proof term#</i>#%}%, a well-typed term of Gallina. To believe that a theorem is true, we only need to trust that the (relatively simple) checker for proof terms is correct; the use of proof scripts is immaterial. Part I of this book will introduce the principles behind encoding all proofs as terms of Gallina. 512 The %\index{Vernacular commands!Qed}%[Qed] command checks that the proof is finished and, if so, saves it. The tactic commands we have written above are an example of a %\emph{%#<i>#proof script#</i>#%}%, or a series of Ltac programs; while [Qed] uses the result of the script to generate a %\emph{%#<i>#proof term#</i>#%}%, a well-typed term of Gallina. To believe that a theorem is true, we only need to trust that the (relatively simple) checker for proof terms is correct; the use of proof scripts is immaterial. Part I of this book will introduce the principles behind encoding all proofs as terms of Gallina.
513 513