Certified Programming with Dependent Types: src/Coinductive.v comparison

comparison src/Coinductive.v @ 67:55199444e5e7

Finish Coinductive chapter

author	Adam Chlipala <adamc@hcoop.net>
date	Wed, 01 Oct 2008 09:56:32 -0400
parents	21bb59c56b98
children	943478e5a32d

comparison

equal deleted inserted replaced

-:b52204928c7d
+:55199444e5e7
 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness.  One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case.  Alternatively, there are tricks that can be played with "hiding" the co-inductive hypothesis.  We will see examples of effective co-inductive proving in later chapters. *)
 (** * Simple Modeling of Non-Terminating Programs *)
-(** 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 an optimization function is sound.  We start by defining a type of instructions. *)
+(** 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 an optimization function is sound.  We start by defining types of registers, program labels, and instructions. *)
 Inductive reg : Set := R1 | R2.
 Definition label := nat.
 Inductive instrs : Set :=
 | Const : reg -> nat -> instrs -> instrs
 | Add : reg -> reg -> reg -> instrs -> instrs
 | Halt : reg -> instrs
 | Jeq : reg -> reg -> label -> instrs -> instrs.
+(** [Const] stores a constant in a register; [Add] stores in the first register the sum of the values in the second two; [Halt] ends the program, returning the value of its register argument; and [Jeq] jumps to a label if the values in two registers are equal.  Each instruction but [Halt] takes an [instrs], which can be read as "list of instructions," as the normal continuation of control flow.
+We can define a program as a list of lists of instructions, where labels will be interpreted as indexing into such a list. *)
 Definition program := list instrs.
+(** We define a polymorphic map type for register keys, with its associated operations. *)
 Section regmap.
 Variable A : Set.
 Record regmap : Set := Regmap {
 VR1 : A;
 VR2 : A
 }.
-Definition empty v : regmap := Regmap v v.
+Definition empty (v : A) : regmap := Regmap v v.
 Definition get (rm : regmap) (r : reg) : A :=
 match r with
 | R1 => VR1 rm
 | R2 => VR2 rm
 end.
 match r with
 | R1 => Regmap v (VR2 rm)
 | R2 => Regmap (VR1 rm) v
 end.
 End regmap.
+(** Now comes the interesting part. We define a co-inductive semantics for programs.  The definition itself is not surprising.  We could change [CoInductive] to [Inductive] and arrive at a valid semantics that only covers terminating program executions.  Using [CoInductive] admits infinite derivations for infinite executions. *)
 Section run.
 Variable prog : program.
 CoInductive run : regmap nat -> instrs -> nat -> Prop :=
 get rm r1 <> get rm r2
 -> run rm is v
 -> run rm (Jeq r1 r2 l is) v.
 End run.
+(** We can write a function which tracks known register values to attempt to constant fold a sequence of instructions.  We track register values with a [regmap (option nat)], where a mapping to [None] indicates no information, and a mapping to [Some n] indicates that the corresponding register is known to have value [n]. *)
 Fixpoint constFold (rm : regmap (option nat)) (is : instrs) {struct is} : instrs :=
 match is with
 | Const r n is => Const r n (constFold (set rm r (Some n)) is)
 | Add r r1 r2 is =>
 match get rm r1, get rm r2 with
-| Some n1, Some n2 => Const r (n1 + n2) (constFold (set rm r (Some (n1 + n2))) is)
+| Some n1, Some n2 =>
+Const r (n1 + n2) (constFold (set rm r (Some (n1 + n2))) is)
 | _, _ => Add r r1 r2 (constFold (set rm r None) is)
 end
 | Halt _ => is
 | Jeq r1 r2 l is => Jeq r1 r2 l (constFold rm is)
 end.
+(** We characterize when the two types of register maps we are using agree with each other. *)
 Definition regmapCompat (rm : regmap nat) (rm' : regmap (option nat)) :=
 forall r, match get rm' r with
 | None => True
 | Some v => get rm r = v
 end.
+(** We prove two lemmas about how register map modifications affect compatibility.  A tactic [compat] abstracts the common structure of the two proofs. *)
+(** remove printing * *)
 Ltac compat := unfold regmapCompat in *; crush;
 match goal with
 | [ |- match get _ ?R with Some _ => _ | None => _ end ] => destruct R; crush
 end.
 regmapCompat rm rm'
 -> regmapCompat (set rm r n) (set rm' r (Some n)).
 destruct r; compat.
 Qed.
-Require Import Arith.
+(** Finally, we can prove the main theorem. *)
 Section constFold_ok.
 Variable prog : program.
 Theorem constFold_ok : forall rm is v,
 Hint Constructors run.
 cofix;
 destruct 1; crush; eauto;
 repeat match goal with
-| [ H : regmapCompat _ _ |- run _ _ (match get ?RM ?R with Some _ => _ | None => _ end) _ ] =>
+| [ H : regmapCompat _ _
+|- run _ _ (match get ?RM ?R with
+| Some _ => _
+| None => _
+end) _ ] =>
 generalize (H R); destruct (get RM R); crush
 end.
 Qed.
 End constFold_ok.
+(** 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. *)
 Print constFold_ok.

Mercurial > cpdt > repo

comparison src/Coinductive.v @ 67:55199444e5e7