comparison src/Coinductive.v @ 347:36a08cad9245

Finished pass over Coinductive
author Adam Chlipala <adam@chlipala.net>
date Sun, 23 Oct 2011 14:48:52 -0400
parents 5d85de065540
children f3154417cd41
comparison
equal deleted inserted replaced
346:5d85de065540 347:36a08cad9245
255 unguarded recursive call in "ones_eq" 255 unguarded recursive call in "ones_eq"
256 >> 256 >>
257 257
258 Via the Curry-Howard correspondence, the same guardedness condition applies to our co-inductive proofs as to our co-inductive data structures. We should be grateful that this proof is rejected, because, if it were not, the same proof structure could be used to prove any co-inductive theorem vacuously, by direct appeal to itself! 258 Via the Curry-Howard correspondence, the same guardedness condition applies to our co-inductive proofs as to our co-inductive data structures. We should be grateful that this proof is rejected, because, if it were not, the same proof structure could be used to prove any co-inductive theorem vacuously, by direct appeal to itself!
259 259
260 Thinking about how Coq would generate a proof term from the proof script above, we see that the problem is that we are violating the guardedness condition. During our proofs, Coq can help us check whether we have yet gone wrong in this way. We can run the command [Guarded] in any context to see if it is possible to finish the proof in a way that will yield a properly guarded proof term.%\index{Vernacular command!Guarded}% 260 Thinking about how Coq would generate a proof term from the proof script above, we see that the problem is that we are violating the guardedness condition. During our proofs, Coq can help us check whether we have yet gone wrong in this way. We can run the command [Guarded] in any context to see if it is possible to finish the proof in a way that will yield a properly guarded proof term.%\index{Vernacular commands!Guarded}%
261 [[ 261 [[
262 Guarded. 262 Guarded.
263 ]] 263 ]]
264 264
265 Running [Guarded] here gives us the same error message that we got when we tried to run [Qed]. In larger proofs, [Guarded] can be helpful in detecting problems %\textit{%#<i>#before#</i>#%}% we think we are ready to run [Qed]. 265 Running [Guarded] here gives us the same error message that we got when we tried to run [Qed]. In larger proofs, [Guarded] can be helpful in detecting problems %\textit{%#<i>#before#</i>#%}% we think we are ready to run [Qed].
515 (* end thide *) 515 (* end thide *)
516 516
517 517
518 (** * Simple Modeling of Non-Terminating Programs *) 518 (** * Simple Modeling of Non-Terminating Programs *)
519 519
520 (** We close the chapter with a quick motivating example for more complex uses of co-inductive types. We will define a co-inductive semantics for a simple assembly language and use that semantics to prove that assembly programs always run forever. This basic technique can be combined with typing judgments for more advanced languages, where some ill-typed programs can go wrong, but no well-typed programs go wrong. 520 (** We close the chapter with a quick motivating example for more complex uses of co-inductive types. We will define a co-inductive semantics for a simple imperative programming language and use that semantics to prove the correctness of a trivial optimization that removes spurious additions by 0. We follow the technique of %\index{co-inductive big-step operational semantics}\emph{%#<i>#co-inductive big-step operational semantics#</i>#%}~\cite{BigStep}%.
521 521
522 We define suggestive synonyms for [nat], for cases where we use natural numbers as registers or program labels. That is, we consider our idealized machine to have infinitely many registers and infinitely many code addresses. *) 522 We define a suggestive synonym for [nat], as we will consider programs with infinitely many variables, represented as [nat]s. *)
523 523
524 Definition reg := nat. 524 Definition var := nat.
525 Definition label := nat. 525
526 526 (** We define a type [vars] of maps from variables to values. To define a function [set] for setting a variable's value in a map, we import the [Arith] module from Coq's standard library, and we use its function [beq_nat] for comparing natural numbers. *)
527 (** Our instructions are loading of a constant into a register, copying from one register to another, unconditional jump, and conditional jump based on whether the value in a register is not zero. *) 527
528 528 Definition vars := var -> nat.
529 Inductive instr : Set :=
530 | Imm : reg -> nat -> instr
531 | Copy : reg -> reg -> instr
532 | Jmp : label -> instr
533 | Jnz : reg -> label -> instr.
534
535 (** We define a type [regs] of maps from registers to values. To define a function [set] for setting a register's value in a map, we import the [Arith] module from Coq's standard library, and we use its function [beq_nat] for comparing natural numbers. *)
536
537 Definition regs := reg -> nat.
538 Require Import Arith. 529 Require Import Arith.
539 Definition set (rs : regs) (r : reg) (v : nat) : regs := 530 Definition set (vs : vars) (v : var) (n : nat) : vars :=
540 fun r' => if beq_nat r r' then v else rs r'. 531 fun v' => if beq_nat v v' then n else vs v'.
541 532
542 (** An inductive [exec] judgment captures the effect of an instruction on the program counter and register bank. *) 533 (** We define a simple arithmetic expression language with variables, and we give it a semantics via an interpreter. *)
543 534
544 Inductive exec : label -> regs -> instr -> label -> regs -> Prop := 535 Inductive exp : Set :=
545 | E_Imm : forall pc rs r n, exec pc rs (Imm r n) (S pc) (set rs r n) 536 | Const : nat -> exp
546 | E_Copy : forall pc rs r1 r2, exec pc rs (Copy r1 r2) (S pc) (set rs r1 (rs r2)) 537 | Var : var -> exp
547 | E_Jmp : forall pc rs pc', exec pc rs (Jmp pc') pc' rs 538 | Plus : exp -> exp -> exp.
548 | E_JnzF : forall pc rs r pc', rs r = 0 -> exec pc rs (Jnz r pc') (S pc) rs 539
549 | E_JnzT : forall pc rs r pc' n, rs r = S n -> exec pc rs (Jnz r pc') pc' rs. 540 Fixpoint evalExp (vs : vars) (e : exp) : nat :=
550 541 match e with
551 (** We prove that [exec] represents a total function. In our proof script, we use a [match] tactic with a [context] pattern. This particular example finds an occurrence of a pattern [Jnz ?r _] anywhere in the current subgoal's conclusion. We use a Coq library tactic [case_eq] to do case analysis on whether the current value [rs r] of the register [r] is zero or not. [case_eq] differs from [destruct] in saving an equality relating the old variable to the new form we deduce for it. *) 542 | Const n => n
552 543 | Var v => vs v
553 Lemma exec_total : forall pc rs i, 544 | Plus e1 e2 => evalExp vs e1 + evalExp vs e2
554 exists pc', exists rs', exec pc rs i pc' rs'. 545 end.
555 Hint Constructors exec. 546
556 547 (** Finally, we define a language of commands. It includes variable assignment, sequencing, and a %\texttt{%#<tt>#while#</tt>#%}% form that repeats as long as its test expression evaluates to a nonzero value. *)
557 destruct i; crush; eauto; 548
549 Inductive cmd : Set :=
550 | Assign : var -> exp -> cmd
551 | Seq : cmd -> cmd -> cmd
552 | While : exp -> cmd -> cmd.
553
554 (** We could define an inductive relation to characterize the results of command evaluation. However, such a relation would not capture %\emph{%#<i>#nonterminating#</i>#%}% executions. With a co-inductive relation, we can capture both cases. The parameters of the relation are an initial state, a command, and a final state. A program that does not terminate in a particular initial state is related to %\emph{%#<i>#any#</i>#%}% final state. *)
555
556 CoInductive evalCmd : vars -> cmd -> vars -> Prop :=
557 | EvalAssign : forall vs v e, evalCmd vs (Assign v e) (set vs v (evalExp vs e))
558 | EvalSeq : forall vs1 vs2 vs3 c1 c2, evalCmd vs1 c1 vs2
559 -> evalCmd vs2 c2 vs3
560 -> evalCmd vs1 (Seq c1 c2) vs3
561 | EvalWhileFalse : forall vs e c, evalExp vs e = 0
562 -> evalCmd vs (While e c) vs
563 | EvalWhileTrue : forall vs1 vs2 vs3 e c, evalExp vs1 e <> 0
564 -> evalCmd vs1 c vs2
565 -> evalCmd vs2 (While e c) vs3
566 -> evalCmd vs1 (While e c) vs3.
567
568 (** Having learned our lesson in the last section, before proceeding, we build a co-induction principle for [evalCmd]. *)
569
570 Section evalCmd_coind.
571 Variable R : vars -> cmd -> vars -> Prop.
572
573 Hypothesis AssignCase : forall vs1 vs2 v e, R vs1 (Assign v e) vs2
574 -> vs2 = set vs1 v (evalExp vs1 e).
575
576 Hypothesis SeqCase : forall vs1 vs3 c1 c2, R vs1 (Seq c1 c2) vs3
577 -> exists vs2, R vs1 c1 vs2 /\ R vs2 c2 vs3.
578
579 Hypothesis WhileCase : forall vs1 vs3 e c, R vs1 (While e c) vs3
580 -> (evalExp vs1 e = 0 /\ vs3 = vs1)
581 \/ exists vs2, evalExp vs1 e <> 0 /\ R vs1 c vs2 /\ R vs2 (While e c) vs3.
582
583 (** The proof is routine. We make use of a form of %\index{tactics!destruct}%[destruct] that takes an %\index{intro pattern}\emph{%#<i>#intro pattern#</i>#%}% in an [as] clause. These patterns control how deeply we break apart the components of an inductive value, and we refer the reader to the Coq manual for more details. *)
584
585 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2.
586 cofix; intros; destruct c.
587 rewrite (AssignCase H); constructor.
588 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto.
589 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst;
590 [ econstructor | econstructor 4 ]; eauto.
591 Qed.
592 End evalCmd_coind.
593
594 (** Now that we have a co-induction principle, we should use it to prove something! Our example is a trivial program optimizer that finds places to replace [0 + e] with [e]. *)
595
596 Fixpoint optExp (e : exp) : exp :=
597 match e with
598 | Plus (Const 0) e => optExp e
599 | Plus e1 e2 => Plus (optExp e1) (optExp e2)
600 | _ => e
601 end.
602
603 Fixpoint optCmd (c : cmd) : cmd :=
604 match c with
605 | Assign v e => Assign v (optExp e)
606 | Seq c1 c2 => Seq (optCmd c1) (optCmd c2)
607 | While e c => While (optExp e) (optCmd c)
608 end.
609
610 (** Before proving correctness of [optCmd], we prove a lemma about [optExp]. This is where we have to do the most work, choosing pattern match opportunities automatically. *)
611
612 (* begin thide *)
613 Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e.
614 induction e; crush;
615 repeat (match goal with
616 | [ |- context[match ?E with Const _ => _ | Var _ => _
617 | Plus _ _ => _ end] ] => destruct E
618 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
619 end; crush).
620 Qed.
621
622 Hint Rewrite optExp_correct : cpdt.
623
624 (** The final theorem is easy to establish, using our co-induction principle and a bit of Ltac smarts that we leave unexplained for now. Curious readers can consult the Coq manual, or wait for the later chapters of this book about proof automation. *)
625
626 Theorem optCmd_correct : forall vs1 c vs2, evalCmd vs1 c vs2
627 -> evalCmd vs1 (optCmd c) vs2.
628 intros; apply (evalCmd_coind (fun vs1 c' vs2 => exists c, evalCmd vs1 c vs2
629 /\ c' = optCmd c)); eauto; crush;
558 match goal with 630 match goal with
559 | [ |- context[Jnz ?r _] ] => case_eq (rs r) 631 | [ H : _ = optCmd ?E |- _ ] => destruct E; simpl in *; discriminate
560 end; eauto. 632 || injection H; intros; subst
561 Qed. 633 end; match goal with
562 634 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; [])
563 (** We are ready to define a co-inductive judgment capturing the idea that a program runs forever. We define the judgment in terms of a program [prog], represented as a function mapping each label to the instruction found there. That is, to simplify the proof, we consider only infinitely long programs. *) 635 || (inversion H; [|])); subst
564 636 end; crush; eauto 10.
565 Section safe. 637 Qed.
566 Variable prog : label -> instr. 638 (* end thide *)
567 639
568 CoInductive safe : label -> regs -> Prop := 640 (** In this form, the theorem tells us that the optimizer preserves observable behavior of both terminating and nonterminating programs, but we did not have to do more work than for the case of terminating programs alone. We merely took the natural inductive definition for terminating executions, made it co-inductive, and applied the appropriate co-induction principle. Curious readers might experiment with adding command constructs like %\texttt{%#<tt>#if#</tt>#%}%; the same proof should continue working, after the co-induction principle is extended to the new evaluation rules. *)
569 | Step : forall pc r pc' r',
570 exec pc r (prog pc) pc' r'
571 -> safe pc' r'
572 -> safe pc r.
573
574 (** Now we can prove that any starting address and register bank lead to safe infinite execution. Recall that proofs of existentially quantified formulas are all built with a single constructor of the inductive type [ex]. This means that we can use [destruct] to %``%#"#open up#"#%''% such proofs. In the proof below, we want to perform this opening up on an appropriate use of the [exec_total] lemma. This lemma's conclusion begins with two existential quantifiers, so we want to tell [destruct] that it should not stop at the first quantifier. We accomplish our goal by using an %\textit{%#<i>#intro pattern#</i>#%}% with [destruct]. Consult the Coq manual for the details of intro patterns; the specific pattern [[? [? ?]]] that we use here accomplishes our goal of destructing both quantifiers at once. *)
575
576 Theorem always_safe : forall pc rs,
577 safe pc rs.
578 cofix; intros;
579 destruct (exec_total pc rs (prog pc)) as [? [? ?]];
580 econstructor; eauto.
581 Qed.
582 End safe.
583
584 (** If we print the proof term that was generated, we can verify that the proof is structured as a [cofix], with each co-recursive call properly guarded. *)
585
586 Print always_safe.
587 641
588 642
589 (** * Exercises *) 643 (** * Exercises *)
590 644
591 (** %\begin{enumerate}%#<ol># 645 (** %\begin{enumerate}%#<ol>#