--- a/src/Coinductive.v	Mon Nov 09 13:18:46 2009 -0500
+++ b/src/Coinductive.v	Mon Nov 09 14:48:46 2009 -0500
@@ -25,16 +25,15 @@
 We spent some time in the last chapter discussing the Curry-Howard isomorphism, where proofs are identified with functional programs.  In such a setting, infinite loops, intended or otherwise, are disastrous.  If Coq allowed the full breadth of definitions that Haskell did, we could code up an infinite loop and use it to prove any proposition vacuously.  That is, the addition of general recursion would make CIC %\textit{%#<i>#inconsistent#</i>#%}%.  For an arbitrary proposition [P], we could write:
 
 [[
-
 Fixpoint bad (u : unit) : P := bad u.
-
+ 
 ]]
 
 This would leave us with [bad tt] as a proof of [P].
 
 There are also algorithmic considerations that make universal termination very desirable.  We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules.  Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps.  It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem.
 
-One solution is to use types to contain the possibility of non-termination.  For instance, we can create a "non-termination monad," inside which we must write all of our general-recursive programs.  In later chapters, we will spend some time on this idea and its applications.  For now, we will just say that it is a heavyweight solution, and so we would like to avoid it whenever possible.
+One solution is to use types to contain the possibility of non-termination.  For instance, we can create a "non-termination monad," inside which we must write all of our general-recursive programs.  This is a heavyweight solution, and so we would like to avoid it whenever possible.
 
 Luckily, Coq has special support for a class of lazy data structures that happens to contain most examples found in Haskell.  That mechanism, %\textit{%#<i>#co-inductive types#</i>#%}%, is the subject of this chapter. *)
 
@@ -65,7 +64,7 @@
 
 (** Co-inductive values are fair game as arguments to recursive functions, and we can use that fact to write a function to take a finite approximation of a stream. *)
 
-Fixpoint approx A (s : stream A) (n : nat) {struct n} : list A :=
+Fixpoint approx A (s : stream A) (n : nat) : list A :=
   match n with
     | O => nil
     | S n' =>
@@ -75,44 +74,39 @@
   end.
 
 Eval simpl in approx zeroes 10.
-(** [[
-
+(** %\vspace{-.15in}% [[
      = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil
      : list nat
      ]] *)
+
 Eval simpl in approx trues 10.
-(** [[
-
+(** %\vspace{-.15in}% [[
      = true
        :: false
           :: true
              :: false
                 :: true :: false :: true :: false :: true :: false :: nil
      : list bool
-     ]] *)
+ 
+     ]]
 
-(** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks.  However, there are important restrictions that are dual to the restrictions on the use of inductive types.  Fixpoints %\textit{%#<i>#consume#</i>#%}% values of inductive types, with restrictions on which %\textit{%#<i>#arguments#</i>#%}% may be passed in recursive calls.  Dually, co-fixpoints %\textit{%#<i>#produce#</i>#%}% values of co-inductive types, with restrictions on what may be done with the %\textit{%#<i>#results#</i>#%}% of co-recursive calls.
+     So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks.  However, there are important restrictions that are dual to the restrictions on the use of inductive types.  Fixpoints %\textit{%#<i>#consume#</i>#%}% values of inductive types, with restrictions on which %\textit{%#<i>#arguments#</i>#%}% may be passed in recursive calls.  Dually, co-fixpoints %\textit{%#<i>#produce#</i>#%}% values of co-inductive types, with restrictions on what may be done with the %\textit{%#<i>#results#</i>#%}% of co-recursive calls.
 
 The restriction for co-inductive types shows up as the %\textit{%#<i>#guardedness condition#</i>#%}%, and it can be broken into two parts.  First, consider this stream definition, which would be legal in Haskell.
 
 [[
 CoFixpoint looper : stream nat := looper.
 
-]]
-
-[[
 Error:
 Recursive definition of looper is ill-formed.
 In environment
 looper : stream nat
 
 unguarded recursive call in "looper"
+ 
 ]]
 
-*)
-
-
-(** The rule we have run afoul of here is that %\textit{%#<i>#every co-recursive call must be guarded by a constructor#</i>#%}%; that is, every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating.  It is a good thing that this rule is enforced.  If the definition of [looper] were accepted, our [approx] function would run forever when passed [looper], and we would have fallen into inconsistency.
+The rule we have run afoul of here is that %\textit{%#<i>#every co-recursive call must be guarded by a constructor#</i>#%}%; that is, every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating.  It is a good thing that this rule is enforced.  If the definition of [looper] were accepted, our [approx] function would run forever when passed [looper], and we would have fallen into inconsistency.
 
 The second rule of guardedness is easiest to see by first introducing a more complicated, but legal, co-fixpoint. *)
 
@@ -128,7 +122,7 @@
 
 (** This code is a literal copy of that for the list [map] function, with the [Nil] case removed and [Fixpoint] changed to [CoFixpoint].  Many other standard functions on lazy data structures can be implemented just as easily.  Some, like [filter], cannot be implemented.  Since the predicate passed to [filter] may reject every element of the stream, we cannot satisfy even the first guardedness condition.
 
-   The second condition is subtler.  To illustrate it, we start off with another co-recursive function definition that %\textit{%#<i>#is#</i>#%}% legal.  The function [interleaves] takes two streams and produces a new stream that alternates between their elements. *)
+   The second condition is subtler.  To illustrate it, we start off with another co-recursive function definition that %\textit{%#<i>#is#</i>#%}% legal.  The function [interleave] takes two streams and produces a new stream that alternates between their elements. *)
 
 Section interleave.
   Variable A : Set.
@@ -144,22 +138,20 @@
 Section map'.
   Variables A B : Set.
   Variable f : A -> B.
-
 (* begin thide *)
   (** [[
-
   CoFixpoint map' (s : stream A) : stream B :=
     match s with
       | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s))
     end.
-
+ 
     ]]
-   *)
-
-  (** We get another error message about an unguarded recursive call.  This is because we are violating the second guardedness condition, which says that, not only must co-recursive calls be arguments to constructors, there must also %\textit{%#<i>#not be anything but [match]es and calls to constructors of the same co-inductive type#</i>#%}% wrapped around these immediate uses of co-recursive calls.  The actual implemented rule for guardedness is a little more lenient than what we have just stated, but you can count on the illegality of any exception that would enhance the expressive power of co-recursion.
+    
+    We get another error message about an unguarded recursive call.  This is because we are violating the second guardedness condition, which says that, not only must co-recursive calls be arguments to constructors, there must also %\textit{%#<i>#not be anything but [match]es and calls to constructors of the same co-inductive type#</i>#%}% wrapped around these immediate uses of co-recursive calls.  The actual implemented rule for guardedness is a little more lenient than what we have just stated, but you can count on the illegality of any exception that would enhance the expressive power of co-recursion.
 
      Why enforce a rule like this?  Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams.  Perhaps this other function might be defined mutually with [map'].  It might deconstruct its first argument, retrieving [map' s] from within [Cons (f h) (map' s)].  Next it might try a [match] on this retrieved value, which amounts to deconstructing [map' s].  To figure out how this [match] turns out, we need to know the top-level structure of [map' s], but this is exactly what we started out trying to determine!  We run into a loop in the evaluation process, and we have reached a witness of inconsistency if we are evaluating [approx (map' s) 1] for any [s]. *)
 (* end thide *)
+
 End map'.
 
 
@@ -176,6 +168,7 @@
 
   (** However, faced with the initial subgoal, it is not at all clear how this theorem can be proved.  In fact, it is unprovable.  The [eq] predicate that we use is fundamentally limited to equalities that can be demonstrated by finite, syntactic arguments.  To prove this equivalence, we will need to introduce a new relation. *)
 (* begin thide *)
+
 Abort.
 
 (** Co-inductive datatypes make sense by analogy from Haskell.  What we need now is a %\textit{%#<i>#co-inductive proposition#</i>#%}%.  That is, we want to define a proposition whose proofs may be infinite, subject to the guardedness condition.  The idea of infinite proofs does not show up in usual mathematics, but it can be very useful (unsurprisingly) for reasoning about infinite data structures.  Besides examples from Haskell, infinite data and proofs will also turn out to be useful for modelling inherently infinite mathematical objects, like program executions.
@@ -197,26 +190,26 @@
 
 Theorem ones_eq : stream_eq ones ones'.
   (** Coq does not support tactical co-inductive proofs as well as it supports tactical inductive proofs.  The usual starting point is the [cofix] tactic, which asks to structure this proof as a co-fixpoint. *)
+
   cofix.
   (** [[
-
   ones_eq : stream_eq ones ones'
   ============================
    stream_eq ones ones'
-   ]] *)
+ 
+   ]]
 
-  (** It looks like this proof might be easier than we expected! *)
+   It looks like this proof might be easier than we expected! *)
 
   assumption.
   (** [[
+Proof completed.
+ 
+]]
 
-Proof completed.
+  Unfortunately, we are due for some disappointment in our victory lap.
 
-]] *)
-
-  (** Unfortunately, we are due for some disappointment in our victory lap. *)
-
-  (** [[
+  [[
 Qed.
 
 Error:
@@ -226,12 +219,12 @@
 ones_eq : stream_eq ones ones'
 
 unguarded recursive call in "ones_eq"
+ 
+]]
 
-]] *)
+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!
 
-  (** 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!
-
-     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 first part of 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.
+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 first part of 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.
 
      [[
 Guarded.
@@ -245,13 +238,14 @@
   Undo.
   simpl.
   (** [[
-
   ones_eq : stream_eq ones ones'
   ============================
    stream_eq ones ones'
-   ]] *)
+ 
+   ]]
 
-  (** It turns out that we are best served by proving an auxiliary lemma. *)
+   It turns out that we are best served by proving an auxiliary lemma. *)
+
 Abort.
 
 (** First, we need to define a function that seems pointless on first glance. *)
@@ -273,20 +267,20 @@
   cofix.
 
   (** We can use the theorem to rewrite the two streams. *)
+
   rewrite (frob_eq ones).
   rewrite (frob_eq ones').
   (** [[
-
   ones_eq : stream_eq ones ones'
   ============================
    stream_eq (frob ones) (frob ones')
-   ]] *)
+ 
+   ]]
 
-  (** Now [simpl] is able to reduce the streams. *)
+   Now [simpl] is able to reduce the streams. *)
 
   simpl.
   (** [[
-
   ones_eq : stream_eq ones ones'
   ============================
    stream_eq (Cons 1 ones)
@@ -295,13 +289,13 @@
             match s with
             | Cons h t => Cons (S h) (map t)
             end) zeroes))
-            ]] *)
+ 
+            ]]
 
-  (** Since we have exposed the [Cons] structure of each stream, we can apply the constructor of [stream_eq]. *)
+  Since we have exposed the [Cons] structure of each stream, we can apply the constructor of [stream_eq]. *)
 
   constructor.
   (** [[
-
   ones_eq : stream_eq ones ones'
   ============================
    stream_eq ones
@@ -309,9 +303,11 @@
          match s with
          | Cons h t => Cons (S h) (map t)
          end) zeroes)
-         ]] *)
+ 
+         ]]
 
-  (** Now, modulo unfolding of the definition of [map], we have matched our assumption. *)
+  Now, modulo unfolding of the definition of [map], we have matched our assumption. *)
+
   assumption.
 Qed.
 
@@ -326,153 +322,84 @@
 Theorem ones_eq' : stream_eq ones ones'.
   cofix; crush.
   (** [[
-
   Guarded.
 
   ]] *)
 Abort.
 (* end thide *)
 
-(** 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. *)
+(** 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. *)
 
 
 (** * 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 types of registers, program labels, and 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 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.
 
-Inductive reg : Set := R1 | R2.
+   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. *)
+
+Definition reg := nat.
 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.
+(** 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. *)
 
-(** [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.
+Inductive instr : Set :=
+| Imm : reg -> nat -> instr
+| Copy : reg -> reg -> instr
+| Jmp : label -> instr
+| Jnz : reg -> label -> instr.
 
-We can define a program as a list of lists of instructions, where labels will be interpreted as indexing into such a list. *)
+(** 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 [eq_nat_dec] for comparing natural numbers. *)
 
-Definition program := list instrs.
+Definition regs := reg -> nat.
+Require Import Arith.
+Definition set (rs : regs) (r : reg) (v : nat) : regs :=
+  fun r' => if eq_nat_dec r r' then v else rs r'.
 
-(** We define a polymorphic map type for register keys, with its associated operations. *)
-Section regmap.
-  Variable A : Set.
+(** An inductive [exec] judgment captures the effect of an instruction on the program counter and register bank. *)
 
-  Record regmap : Set := Regmap {
-    VR1 : A;
-    VR2 : A
-  }.
+Inductive exec : label -> regs -> instr -> label -> regs -> Prop :=
+| E_Imm : forall pc rs r n, exec pc rs (Imm r n) (S pc) (set rs r n)
+| E_Copy : forall pc rs r1 r2, exec pc rs (Copy r1 r2) (S pc) (set rs r1 (rs r2))
+| E_Jmp : forall pc rs pc', exec pc rs (Jmp pc') pc' rs
+| E_JnzF : forall pc rs r pc', rs r = 0 -> exec pc rs (Jnz r pc') (S pc) rs
+| E_JnzT : forall pc rs r pc' n, rs r = S n -> exec pc rs (Jnz r pc') pc' rs.
 
-  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.
-  Definition set (rm : regmap) (r : reg) (v : A) : regmap :=
-    match r with
-      | R1 => Regmap v (VR2 rm)
-      | R2 => Regmap (VR1 rm) v
-    end.
-End regmap.
+(** 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. *)
 
-(** 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.  An application [run rm is v] means that, when we run the instructions [is] starting with register map [rm], either execution terminates with result [v] or execution runs safely forever.  (That is, the choice of [v] is immaterial for non-terminating executions.) *)
+Lemma exec_total : forall pc rs i,
+  exists pc', exists rs', exec pc rs i pc' rs'.
+  Hint Constructors exec.
 
-Section run.
-  Variable prog : program.
-
-  CoInductive run : regmap nat -> instrs -> nat -> Prop :=
-  | RConst : forall rm r n is v,
-    run (set rm r n) is v
-    -> run rm (Const r n is) v
-  | RAdd : forall rm r r1 r2 is v,
-    run (set rm r (get rm r1 + get rm r2)) is v
-    -> run rm (Add r r1 r2 is) v
-  | RHalt : forall rm r,
-    run rm (Halt r) (get rm r)
-  | RJeq_eq : forall rm r1 r2 l is is' v,
-    get rm r1 = get rm r2
-    -> nth_error prog l = Some is'
-    -> run rm is' v
-    -> run rm (Jeq r1 r2 l is) v
-  | RJeq_neq : forall rm r1 r2 l is v,
-    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)
-        | _, _ => 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
-    | [ H : _ |- match get _ ?R with Some _ => _ | None => _ end ] => generalize (H R); destruct R; crush
-  end.
-
-Lemma regmapCompat_set_None : forall rm rm' r n,
-  regmapCompat rm rm'
-  -> regmapCompat (set rm r n) (set rm' r None).
-  destruct r; compat.
+  destruct i; crush; eauto;
+    match goal with
+      | [ |- context[Jnz ?r _] ] => case_eq (rs r)
+    end; eauto.
 Qed.
 
-Lemma regmapCompat_set_Some : forall rm rm' r n,
-  regmapCompat rm rm'
-  -> regmapCompat (set rm r n) (set rm' r (Some n)).
-  destruct r; compat.
-Qed.
+(** 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. *)
 
-(** Finally, we can prove the main theorem. *)
+Section safe.
+  Variable prog : label -> instr.
 
-Section constFold_ok.
-  Variable prog : program.
+  CoInductive safe : label -> regs -> Prop :=
+  | Step : forall pc r pc' r',
+    exec pc r (prog pc) pc' r'
+    -> safe pc' r'
+    -> safe pc r.
 
-  Theorem constFold_ok : forall rm is v,
-    run prog rm is v
-    -> forall rm', regmapCompat rm rm'
-      -> run prog rm (constFold rm' is) v.
-    Hint Resolve regmapCompat_set_None regmapCompat_set_Some.
-    Hint Constructors run.
-
-    cofix;
-      destruct 1; crush; eauto;
-        repeat match goal with
-                 | [ H : regmapCompat _ _
-                   |- run _ _ (match get ?RM ?R with
-                                 | Some _ => _
-                                 | None => _
-                               end) _ ] =>
-                   generalize (H R); destruct (get RM R); crush
-               end.
+  (** 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. *)
+  
+  Theorem always_safe : forall pc rs,
+    safe pc rs.
+    cofix; intros;
+      destruct (exec_total pc rs (prog pc)) as [? [? ?]];
+        econstructor; eauto.
   Qed.
-End constFold_ok.
+End safe.
 
 (** 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.
+Print always_safe.
 
 
 (** * Exercises *)