Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

ImpCEvalFun: An Evaluation Function for Imp

We saw in the Imp chapter how a naive approach to defining a function representing evaluation for Imp runs into difficulties. There, we adopted the solution of changing from a functional to a relational definition of evaluation. In this optional chapter, we consider strategies for getting the functional approach to work.

(* ################################################################# *)

A Broken Evaluator

From Coq Require Import omega.Omega.
From Coq Require Import Arith.Arith.
From LF Require Import Imp Maps.

Here was our first try at an evaluation function for commands, omitting WHILE.

Open Scope imp_scope.
Fixpoint ceval_step1 (st : state) (c : com) : state :=
  match c with
    | SKIP =>
        st
    | l ::= a1 =>
        (l !-> aeval st a1 ; st)
    | c1 ;; c2 =>
        let st' := ceval_step1 st c1 in
        ceval_step1 st' c2
    | TEST b THEN c1 ELSE c2 FI =>
        if (beval st b)
          then ceval_step1 st c1
          else ceval_step1 st c2
    | WHILE b1 DO c1 END =>
        st  (* bogus *)
  end.
Close Scope imp_scope.

As we remarked in chapter Imp, in a traditional functional programming language like ML or Haskell we could write the WHILE case as follows:

| WHILE b1 DO c1 END => if (beval st b1) then ceval_step1 st (c1;; WHILE b1 DO c1 END) else st

Coq doesn't accept such a definition (Error: Cannot guess decreasing argument of fix) because the function we want to define is not guaranteed to terminate. Indeed, the changed ceval_step1 function applied to the loop program from Imp.v would never terminate. Since Coq is not just a functional programming language, but also a consistent logic, any potentially non-terminating function needs to be rejected. Here is an invalid(!) Coq program showing what would go wrong if Coq allowed non-terminating recursive functions:

Fixpoint loop_false (n : nat) : False := loop_false n.

That is, propositions like False would become provable (e.g., loop_false 0 would be a proof of False), which would be a disaster for Coq's logical consistency.

Thus, because it doesn't terminate on all inputs, the full version of ceval_step1 cannot be written in Coq -- at least not without one additional trick...

(* ################################################################# *)

A Step-Indexed Evaluator

The trick we need is to pass an additional parameter to the evaluation function that tells it how long to run. Informally, we start the evaluator with a certain amount of "gas" in its tank, and we allow it to run until either it terminates in the usual way or it runs out of gas, at which point we simply stop evaluating and say that the final result is the empty memory. (We could also say that the result is the current state at the point where the evaluator runs out of gas -- it doesn't really matter because the result is going to be wrong in either case!)

Open Scope imp_scope.
Fixpoint ceval_step2 (st : state) (c : com) (i : nat) : state :=
  match i with
  | O => empty_st
  | S i' =>
    match c with
      | SKIP =>
          st
      | l ::= a1 =>
          (l !-> aeval st a1 ; st)
      | c1 ;; c2 =>
          let st' := ceval_step2 st c1 i' in
          ceval_step2 st' c2 i'
      | TEST b THEN c1 ELSE c2 FI =>
          if (beval st b)
            then ceval_step2 st c1 i'
            else ceval_step2 st c2 i'
      | WHILE b1 DO c1 END =>
          if (beval st b1)
          then let st' := ceval_step2 st c1 i' in
               ceval_step2 st' c i'
          else st
    end
  end.
Close Scope imp_scope.

Note: It is tempting to think that the index i here is counting the "number of steps of evaluation." But if you look closely you'll see that this is not the case: for example, in the rule for sequencing, the same i is passed to both recursive calls. Understanding the exact way that i is treated will be important in the proof of ceval__ceval_step, which is given as an exercise below.

One thing that is not so nice about this evaluator is that we can't tell, from its result, whether it stopped because the program terminated normally or because it ran out of gas. Our next version returns an option state instead of just a state, so that we can distinguish between normal and abnormal termination.

Open Scope imp_scope.
Fixpoint ceval_step3 (st : state) (c : com) (i : nat)
                    : option state :=
  match i with
  | O => None
  | S i' =>
    match c with
      | SKIP =>
          Some st
      | l ::= a1 =>
          Some (l !-> aeval st a1 ; st)
      | c1 ;; c2 =>
          match (ceval_step3 st c1 i') with
          | Some st' => ceval_step3 st' c2 i'
          | None => None
          end
      | TEST b THEN c1 ELSE c2 FI =>
          if (beval st b)
            then ceval_step3 st c1 i'
            else ceval_step3 st c2 i'
      | WHILE b1 DO c1 END =>
          if (beval st b1)
          then match (ceval_step3 st c1 i') with
               | Some st' => ceval_step3 st' c i'
               | None => None
               end
          else Some st
    end
  end.
Close Scope imp_scope.

We can improve the readability of this version by introducing a bit of auxiliary notation to hide the plumbing involved in repeatedly matching against optional states.

Notation "'LETOPT' x <== e1 'IN' e2"
   := (match e1 with
         | Some x => e2
         | None => None
       end)
   (right associativity, at level 60).

Open Scope imp_scope.
Fixpoint ceval_step (st : state) (c : com) (i : nat)
                    : option state :=
  match i with
  | O => None
  | S i' =>
    match c with
      | SKIP =>
          Some st
      | l ::= a1 =>
          Some (l !-> aeval st a1 ; st)
      | c1 ;; c2 =>
          LETOPT st' <== ceval_step st c1 i' IN
          ceval_step st' c2 i'
      | TEST b THEN c1 ELSE c2 FI =>
          if (beval st b)
            then ceval_step st c1 i'
            else ceval_step st c2 i'
      | WHILE b1 DO c1 END =>
          if (beval st b1)
          then LETOPT st' <== ceval_step st c1 i' IN
               ceval_step st' c i'
          else Some st
    end
  end.
Close Scope imp_scope.

Definition test_ceval (st:state) (c:com) :=
  match ceval_step st c 500 with
  | None    => None
  | Some st => Some (st X, st Y, st Z)
  end.

(* Compute
     (test_ceval empty_st
         (X ::= 2;;
          TEST (X <= 1)
            THEN Y ::= 3
            ELSE Z ::= 4
          FI)).
   ====>
      Some (2, 0, 4)   *)

Exercise: 2 stars, standard, recommended (pup_to_n)

Write an Imp program that sums the numbers from 1 to X (inclusive: 1 + 2 + ... + X) in the variable Y. Make sure your solution satisfies the test that follows.

Definition pup_to_n : com
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *).com Admitted.

(* 

Example pup_to_n_1 :
  test_ceval (X !-> 5) pup_to_n
  = Some (0, 15, 0).
Proof. reflexivity. Qed.

    [] *)

Exercise: 2 stars, standard, optional (peven)

Write an Imp program that sets Z to 0 if X is even and sets Z to 1 otherwise. Use test_ceval to test your program.

(* FILL IN HERE 

    [] *)

(* ################################################################# *)

Relational vs. Step-Indexed Evaluation

As for arithmetic and boolean expressions, we'd hope that the two alternative definitions of evaluation would actually amount to the same thing in the end. This section shows that this is the case.

Theorem ceval_step__ceval: forall c st st',
      (exists i, ceval_step st c i = Some st') ->
      st =[ c ]=> st'.forall (c : com) (st st' : state),
(exists i : nat, ceval_step st c i = Some st') ->
st =[ c ]=> st'
Proof.forall (c : com) (st st' : state),
(exists i : nat, ceval_step st c i = Some st') ->
st =[ c ]=> st'
  intros c st st' H.c:com
st, st':state
H:exists i : nat, ceval_step st c i = Some st'
st =[ c ]=> st'
  inversion H as [i E].c:com
st, st':state
H:exists i0 : nat, ceval_step st c i0 = Some st'
i:nat
E:ceval_step st c i = Some st'
st =[ c ]=> st'
  clear H.c:com
st, st':state
i:nat
E:ceval_step st c i = Some st'
st =[ c ]=> st'
  generalize dependent st'.c:com
st:state
i:nat
forall st' : state,
ceval_step st c i = Some st' -> st =[ c ]=> st'
  generalize dependent st.c:com
i:nat
forall st st' : state,
ceval_step st c i = Some st' -> st =[ c ]=> st'
  generalize dependent c.i:nat
forall (c : com) (st st' : state),
ceval_step st c i = Some st' -> st =[ c ]=> st'
  induction i as [| i' ].forall (c : com) (st st' : state),
ceval_step st c 0 = Some st' -> st =[ c ]=> st'
i':nat
IHi':forall (c : com) (st st' : state),
ceval_step st c i' = Some st' ->
st =[ c ]=> st'
forall (c : com) (st st' : state),
ceval_step st c (S i') = Some st' -> st =[ c ]=> st'

  - (* i = 0 -- contradictory *)forall (c : com) (st st' : state),
ceval_step st c 0 = Some st' -> st =[ c ]=> st'
    intros c st st' H.c:com
st, st':state
H:ceval_step st c 0 = Some st'
st =[ c ]=> st' discriminate H.

  - (* i = S i' *)i':nat
IHi':forall (c : com) (st st' : state),
ceval_step st c i' = Some st' ->
st =[ c ]=> st'
forall (c : com) (st st' : state),
ceval_step st c (S i') = Some st' -> st =[ c ]=> st'
    intros c st st' H.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
c:com
st, st':state
H:ceval_step st c (S i') = Some st'
st =[ c ]=> st'
    destruct c;
           simpl in H; inversion H; subst; clear H.i':nat
IHi':forall (c : com) (st st'0 : state),
ceval_step st c i' = Some st'0 ->
st =[ c ]=> st'0
st':state
st' =[ SKIP ]=> st'
i':nat
IHi':forall (c : com) (st0 st' : state),
ceval_step st0 c i' = Some st' ->
st0 =[ c ]=> st'
x:string
a:aexp
st:state
st =[ x ::= a ]=> (x !-> aeval st a; st)
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st':state
H1:LETOPT st'0 <== ceval_step st c1 i'
IN ceval_step st'0 c2 i' = 
Some st'
st =[ c1;; c2 ]=> st'
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
H1:(if beval st b
 then ceval_step st c1 i'
 else ceval_step st c2 i') = 
Some st'
st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
H1:(if beval st b
 then
  LETOPT st'0 <== ceval_step st c i'
  IN ceval_step st'0 (WHILE b DO c END) i'
 else Some st) = Some st'
st =[ WHILE b DO c END ]=> st'
      + (* SKIP *)i':nat
IHi':forall (c : com) (st st'0 : state),
ceval_step st c i' = Some st'0 ->
st =[ c ]=> st'0
st':state
st' =[ SKIP ]=> st' apply E_Skip.
      + (* ::= *)i':nat
IHi':forall (c : com) (st0 st' : state),
ceval_step st0 c i' = Some st' ->
st0 =[ c ]=> st'
x:string
a:aexp
st:state
st =[ x ::= a ]=> (x !-> aeval st a; st) apply E_Ass.i':nat
IHi':forall (c : com) (st0 st' : state),
ceval_step st0 c i' = Some st' ->
st0 =[ c ]=> st'
x:string
a:aexp
st:state
aeval st a = aeval st a reflexivity.

      + (* ;; *)i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st':state
H1:LETOPT st'0 <== ceval_step st c1 i'
IN ceval_step st'0 c2 i' = 
Some st'
st =[ c1;; c2 ]=> st'
        destruct (ceval_step st c1 i') eqn:Heqr1.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
st =[ c1;; c2 ]=> st'
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st':state
Heqr1:ceval_step st c1 i' = None
H1:None = Some st'
st =[ c1;; c2 ]=> st'
        * (* Evaluation of r1 terminates normally *)i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
st =[ c1;; c2 ]=> st'
          apply E_Seq with s.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
st =[ c1 ]=> s
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
s =[ c2 ]=> st'
            apply IHi'.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
ceval_step st c1 i' = Some s
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
s =[ c2 ]=> st' rewrite Heqr1.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
Some s = Some s
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
s =[ c2 ]=> st' reflexivity.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
s =[ c2 ]=> st'
            apply IHi'.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
ceval_step s c2 i' = Some st' simpl in H1.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st', s:state
Heqr1:ceval_step st c1 i' = Some s
H1:ceval_step s c2 i' = Some st'
ceval_step s c2 i' = Some st' assumption.
        * (* Otherwise -- contradiction *)i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
c1, c2:com
st, st':state
Heqr1:ceval_step st c1 i' = None
H1:None = Some st'
st =[ c1;; c2 ]=> st'
          discriminate H1.

      + (* TEST *)i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
H1:(if beval st b
 then ceval_step st c1 i'
 else ceval_step st c2 i') = 
Some st'
st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
        destruct (beval st b) eqn:Heqr.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = true
H1:ceval_step st c1 i' = Some st'
st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = false
H1:ceval_step st c2 i' = Some st'
st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
        * (* r = true *)i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = true
H1:ceval_step st c1 i' = Some st'
st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
          apply E_IfTrue.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = true
H1:ceval_step st c1 i' = Some st'
beval st b = true
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = true
H1:ceval_step st c1 i' = Some st'
st =[ c1 ]=> st' rewrite Heqr.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = true
H1:ceval_step st c1 i' = Some st'
true = true
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = true
H1:ceval_step st c1 i' = Some st'
st =[ c1 ]=> st' reflexivity.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = true
H1:ceval_step st c1 i' = Some st'
st =[ c1 ]=> st'
          apply IHi'.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = true
H1:ceval_step st c1 i' = Some st'
ceval_step st c1 i' = Some st' assumption.
        * (* r = false *)i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = false
H1:ceval_step st c2 i' = Some st'
st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
          apply E_IfFalse.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = false
H1:ceval_step st c2 i' = Some st'
beval st b = false
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = false
H1:ceval_step st c2 i' = Some st'
st =[ c2 ]=> st' rewrite Heqr.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = false
H1:ceval_step st c2 i' = Some st'
false = false
i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = false
H1:ceval_step st c2 i' = Some st'
st =[ c2 ]=> st' reflexivity.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = false
H1:ceval_step st c2 i' = Some st'
st =[ c2 ]=> st'
          apply IHi'.i':nat
IHi':forall (c : com) (st0 st'0 : state),
ceval_step st0 c i' = Some st'0 ->
st0 =[ c ]=> st'0
b:bexp
c1, c2:com
st, st':state
Heqr:beval st b = false
H1:ceval_step st c2 i' = Some st'
ceval_step st c2 i' = Some st' assumption.

      + (* WHILE *)i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
H1:(if beval st b
 then
  LETOPT st'0 <== ceval_step st c i'
  IN ceval_step st'0 (WHILE b DO c END) i'
 else Some st) = Some st'
st =[ WHILE b DO c END ]=> st' destruct (beval st b) eqn :Heqr.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
H1:LETOPT st'0 <== ceval_step st c i'
IN ceval_step st'0 (WHILE b DO c END) i' =
Some st'
st =[ WHILE b DO c END ]=> st'
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = false
H1:Some st = Some st'
st =[ WHILE b DO c END ]=> st'
        * (* r = true *)i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
H1:LETOPT st'0 <== ceval_step st c i'
IN ceval_step st'0 (WHILE b DO c END) i' =
Some st'
st =[ WHILE b DO c END ]=> st'
         destruct (ceval_step st c i') eqn:Heqr1.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
st =[ WHILE b DO c END ]=> st'
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
Heqr1:ceval_step st c i' = None
H1:None = Some st'
st =[ WHILE b DO c END ]=> st'
         { (* r1 = Some s *)i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
st =[ WHILE b DO c END ]=> st'
           apply E_WhileTrue with s.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
beval st b = true
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
st =[ c ]=> s
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
s =[ WHILE b DO c END ]=> st' rewrite Heqr.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
true = true
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
st =[ c ]=> s
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
s =[ WHILE b DO c END ]=> st'
           reflexivity.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
st =[ c ]=> s
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
s =[ WHILE b DO c END ]=> st'
           apply IHi'.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
ceval_step st c i' = Some s
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
s =[ WHILE b DO c END ]=> st' rewrite Heqr1.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
Some s = Some s
i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
s =[ WHILE b DO c END ]=> st' reflexivity.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
s =[ WHILE b DO c END ]=> st'
           apply IHi'.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
ceval_step s (WHILE b DO c END) i' = Some st' simpl in H1.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
s:state
Heqr1:ceval_step st c i' = Some s
H1:ceval_step s (WHILE b DO c END) i' = Some st'
ceval_step s (WHILE b DO c END) i' = Some st' assumption. }i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
Heqr1:ceval_step st c i' = None
H1:None = Some st'
st =[ WHILE b DO c END ]=> st'
         { (* r1 = None *)i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = true
Heqr1:ceval_step st c i' = None
H1:None = Some st'
st =[ WHILE b DO c END ]=> st' discriminate H1. }
        * (* r = false *)i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = false
H1:Some st = Some st'
st =[ WHILE b DO c END ]=> st'
          injection H1.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = false
H1:Some st = Some st'
st = st' -> st =[ WHILE b DO c END ]=> st' intros H2.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = false
H1:Some st = Some st'
H2:st = st'
st =[ WHILE b DO c END ]=> st' rewrite <- H2.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = false
H1:Some st = Some st'
H2:st = st'
st =[ WHILE b DO c END ]=> st
          apply E_WhileFalse.i':nat
IHi':forall (c0 : com) (st0 st'0 : state),
ceval_step st0 c0 i' = Some st'0 ->
st0 =[ c0 ]=> st'0
b:bexp
c:com
st, st':state
Heqr:beval st b = false
H1:Some st = Some st'
H2:st = st'
beval st b = false apply Heqr. Qed.

Exercise: 4 stars, standard (ceval_step__ceval_inf)

Write an informal proof of ceval_step__ceval, following the usual template. (The template for case analysis on an inductively defined value should look the same as for induction, except that there is no induction hypothesis.) Make your proof communicate the main ideas to a human reader; do not simply transcribe the steps of the formal proof.

(* FILL IN HERE *)

(* Do not modify the following line: *)
Definition manual_grade_for_ceval_step__ceval_inf : option (nat*string) := None.

☐

Theorem ceval_step_more: forall i1 i2 st st' c,
  i1 <= i2 ->
  ceval_step st c i1 = Some st' ->
  ceval_step st c i2 = Some st'.forall (i1 i2 : nat) (st st' : state) (c : com),
i1 <= i2 ->
ceval_step st c i1 = Some st' ->
ceval_step st c i2 = Some st'
Proof.forall (i1 i2 : nat) (st st' : state) (c : com),
i1 <= i2 ->
ceval_step st c i1 = Some st' ->
ceval_step st c i2 = Some st'
induction i1 as [|i1']; intros i2 st st' c Hle Hceval.i2:nat
st, st':state
c:com
Hle:0 <= i2
Hceval:ceval_step st c 0 = Some st'
ceval_step st c i2 = Some st'
i1':nat
IHi1':forall (i0 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i0 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i0 = Some st'0
i2:nat
st, st':state
c:com
Hle:S i1' <= i2
Hceval:ceval_step st c (S i1') = Some st'
ceval_step st c i2 = Some st'
  - (* i1 = 0 *)i2:nat
st, st':state
c:com
Hle:0 <= i2
Hceval:ceval_step st c 0 = Some st'
ceval_step st c i2 = Some st'
    simpl in Hceval.i2:nat
st, st':state
c:com
Hle:0 <= i2
Hceval:None = Some st'
ceval_step st c i2 = Some st' discriminate Hceval.
  - (* i1 = S i1' *)i1':nat
IHi1':forall (i0 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i0 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i0 = Some st'0
i2:nat
st, st':state
c:com
Hle:S i1' <= i2
Hceval:ceval_step st c (S i1') = Some st'
ceval_step st c i2 = Some st'
    destruct i2 as [|i2'].i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
st, st':state
c:com
Hle:S i1' <= 0
Hceval:ceval_step st c (S i1') = Some st'
ceval_step st c 0 = Some st'
i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
c:com
Hle:S i1' <= S i2'
Hceval:ceval_step st c (S i1') = Some st'
ceval_step st c (S i2') = Some st' inversion Hle.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
c:com
Hle:S i1' <= S i2'
Hceval:ceval_step st c (S i1') = Some st'
ceval_step st c (S i2') = Some st'
    assert (Hle': i1' <= i2') by omega.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
c:com
Hle:S i1' <= S i2'
Hceval:ceval_step st c (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st c (S i2') = Some st'
    destruct c.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
Hle:S i1' <= S i2'
Hceval:ceval_step st SKIP (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st SKIP (S i2') = Some st'
i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
x:string
a:aexp
Hle:S i1' <= S i2'
Hceval:ceval_step st (x ::= a) (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st (x ::= a) (S i2') = Some st'
i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
Hceval:ceval_step st (c1;; c2) (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st (c1;; c2) (S i2') = Some st'
i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
b:bexp
c1, c2:com
Hle:S i1' <= S i2'
Hceval:ceval_step st (TEST b THEN c1 ELSE c2 FI)
  (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st (TEST b THEN c1 ELSE c2 FI) (S i2') =
Some st'
i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
Hceval:ceval_step st (WHILE b DO c END) (S i1') =
Some st'
Hle':i1' <= i2'
ceval_step st (WHILE b DO c END) (S i2') = Some st'
    + (* SKIP *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
Hle:S i1' <= S i2'
Hceval:ceval_step st SKIP (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st SKIP (S i2') = Some st'
      simpl in Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
Hle:S i1' <= S i2'
Hceval:Some st = Some st'
Hle':i1' <= i2'
ceval_step st SKIP (S i2') = Some st' inversion Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
Hle:S i1' <= S i2'
Hceval:Some st = Some st'
Hle':i1' <= i2'
H0:st = st'
ceval_step st' SKIP (S i2') = Some st'
      reflexivity.
    + (* ::= *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
x:string
a:aexp
Hle:S i1' <= S i2'
Hceval:ceval_step st (x ::= a) (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st (x ::= a) (S i2') = Some st'
      simpl in Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
x:string
a:aexp
Hle:S i1' <= S i2'
Hceval:Some (x !-> aeval st a; st) = Some st'
Hle':i1' <= i2'
ceval_step st (x ::= a) (S i2') = Some st' inversion Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
x:string
a:aexp
Hle:S i1' <= S i2'
Hceval:Some (x !-> aeval st a; st) = Some st'
Hle':i1' <= i2'
H0:(x !-> aeval st a; st) = st'
ceval_step st (x ::= a) (S i2') =
Some (x !-> aeval st a; st)
      reflexivity.
    + (* ;; *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
Hceval:ceval_step st (c1;; c2) (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st (c1;; c2) (S i2') = Some st'
      simpl in Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
Hceval:LETOPT st'0 <== ceval_step st c1 i1'
IN ceval_step st'0 c2 i1' = 
Some st'
Hle':i1' <= i2'
ceval_step st (c1;; c2) (S i2') = Some st' simpl.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
Hceval:LETOPT st'0 <== ceval_step st c1 i1'
IN ceval_step st'0 c2 i1' = 
Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c1 i2'
IN ceval_step st'0 c2 i2' = 
Some st'
      destruct (ceval_step st c1 i1') eqn:Heqst1'o.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c1 i1' = Some s
Hceval:ceval_step s c2 i1' = Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c1 i2'
IN ceval_step st'0 c2 i2' = 
Some st'
i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
Heqst1'o:ceval_step st c1 i1' = None
Hceval:None = Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c1 i2'
IN ceval_step st'0 c2 i2' = 
Some st'
      * (* st1'o = Some *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c1 i1' = Some s
Hceval:ceval_step s c2 i1' = Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c1 i2'
IN ceval_step st'0 c2 i2' = 
Some st'
        apply (IHi1' i2') in Heqst1'o; try assumption.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c1 i2' = Some s
Hceval:ceval_step s c2 i1' = Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c1 i2'
IN ceval_step st'0 c2 i2' = 
Some st'
        rewrite Heqst1'o.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c1 i2' = Some s
Hceval:ceval_step s c2 i1' = Some st'
Hle':i1' <= i2'
ceval_step s c2 i2' = Some st' simpl.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c1 i2' = Some s
Hceval:ceval_step s c2 i1' = Some st'
Hle':i1' <= i2'
ceval_step s c2 i2' = Some st' simpl in Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c1 i2' = Some s
Hceval:ceval_step s c2 i1' = Some st'
Hle':i1' <= i2'
ceval_step s c2 i2' = Some st'
        apply (IHi1' i2') in Hceval; try assumption.
      * (* st1'o = None *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
c1, c2:com
Hle:S i1' <= S i2'
Heqst1'o:ceval_step st c1 i1' = None
Hceval:None = Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c1 i2'
IN ceval_step st'0 c2 i2' = 
Some st'
        discriminate Hceval.

    + (* TEST *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
b:bexp
c1, c2:com
Hle:S i1' <= S i2'
Hceval:ceval_step st (TEST b THEN c1 ELSE c2 FI)
  (S i1') = Some st'
Hle':i1' <= i2'
ceval_step st (TEST b THEN c1 ELSE c2 FI) (S i2') =
Some st'
      simpl in Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
b:bexp
c1, c2:com
Hle:S i1' <= S i2'
Hceval:(if beval st b
 then ceval_step st c1 i1'
 else ceval_step st c2 i1') = 
Some st'
Hle':i1' <= i2'
ceval_step st (TEST b THEN c1 ELSE c2 FI) (S i2') =
Some st' simpl.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state) (c : com),
i1' <= i2 ->
ceval_step st0 c i1' = Some st'0 ->
ceval_step st0 c i2 = Some st'0
i2':nat
st, st':state
b:bexp
c1, c2:com
Hle:S i1' <= S i2'
Hceval:(if beval st b
 then ceval_step st c1 i1'
 else ceval_step st c2 i1') = 
Some st'
Hle':i1' <= i2'
(if beval st b
 then ceval_step st c1 i2'
 else ceval_step st c2 i2') = 
Some st'
      destruct (beval st b); apply (IHi1' i2') in Hceval;
        assumption.

    + (* WHILE *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
Hceval:ceval_step st (WHILE b DO c END) (S i1') =
Some st'
Hle':i1' <= i2'
ceval_step st (WHILE b DO c END) (S i2') = Some st'
      simpl in Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
Hceval:(if beval st b
 then
  LETOPT st'0 <== ceval_step st c i1'
  IN ceval_step st'0 (WHILE b DO c END) i1'
 else Some st) = Some st'
Hle':i1' <= i2'
ceval_step st (WHILE b DO c END) (S i2') = Some st' simpl.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
Hceval:(if beval st b
 then
  LETOPT st'0 <== ceval_step st c i1'
  IN ceval_step st'0 (WHILE b DO c END) i1'
 else Some st) = Some st'
Hle':i1' <= i2'
(if beval st b
 then
  LETOPT st'0 <== ceval_step st c i2'
  IN ceval_step st'0 (WHILE b DO c END) i2'
 else Some st) = Some st'
      destruct (beval st b); try assumption.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
Hceval:LETOPT st'0 <== ceval_step st c i1'
IN ceval_step st'0 (WHILE b DO c END) i1' =
Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c i2'
IN ceval_step st'0 (WHILE b DO c END) i2' = 
Some st'
      destruct (ceval_step st c i1') eqn: Heqst1'o.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c i1' = Some s
Hceval:ceval_step s (WHILE b DO c END) i1' =
Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c i2'
IN ceval_step st'0 (WHILE b DO c END) i2' = 
Some st'
i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
Heqst1'o:ceval_step st c i1' = None
Hceval:None = Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c i2'
IN ceval_step st'0 (WHILE b DO c END) i2' = 
Some st'
      * (* st1'o = Some *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c i1' = Some s
Hceval:ceval_step s (WHILE b DO c END) i1' =
Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c i2'
IN ceval_step st'0 (WHILE b DO c END) i2' = 
Some st'
        apply (IHi1' i2') in Heqst1'o; try assumption.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c i2' = Some s
Hceval:ceval_step s (WHILE b DO c END) i1' =
Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c i2'
IN ceval_step st'0 (WHILE b DO c END) i2' = 
Some st'
        rewrite -> Heqst1'o.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c i2' = Some s
Hceval:ceval_step s (WHILE b DO c END) i1' =
Some st'
Hle':i1' <= i2'
ceval_step s (WHILE b DO c END) i2' = Some st' simpl.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c i2' = Some s
Hceval:ceval_step s (WHILE b DO c END) i1' =
Some st'
Hle':i1' <= i2'
ceval_step s (WHILE b DO c END) i2' = Some st' simpl in Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
s:state
Heqst1'o:ceval_step st c i2' = Some s
Hceval:ceval_step s (WHILE b DO c END) i1' =
Some st'
Hle':i1' <= i2'
ceval_step s (WHILE b DO c END) i2' = Some st'
        apply (IHi1' i2') in Hceval; try assumption.
      * (* i1'o = None *)i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
Heqst1'o:ceval_step st c i1' = None
Hceval:None = Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c i2'
IN ceval_step st'0 (WHILE b DO c END) i2' = 
Some st'
        simpl in Hceval.i1':nat
IHi1':forall (i2 : nat) (st0 st'0 : state)
  (c0 : com),
i1' <= i2 ->
ceval_step st0 c0 i1' = Some st'0 ->
ceval_step st0 c0 i2 = Some st'0
i2':nat
st, st':state
b:bexp
c:com
Hle:S i1' <= S i2'
Heqst1'o:ceval_step st c i1' = None
Hceval:None = Some st'
Hle':i1' <= i2'
LETOPT st'0 <== ceval_step st c i2'
IN ceval_step st'0 (WHILE b DO c END) i2' = 
Some st' discriminate Hceval.  Qed.

Exercise: 3 stars, standard, recommended (ceval__ceval_step)

Finish the following proof. You'll need ceval_step_more in a few places, as well as some basic facts about ≤ and plus.

Theorem ceval__ceval_step: forall c st st',
      st =[ c ]=> st' ->
      exists i, ceval_step st c i = Some st'.forall (c : com) (st st' : state),
st =[ c ]=> st' ->
exists i : nat, ceval_step st c i = Some st'
Proof.forall (c : com) (st st' : state),
st =[ c ]=> st' ->
exists i : nat, ceval_step st c i = Some st'
  intros c st st' Hce.c:com
st, st':state
Hce:st =[ c ]=> st'
exists i : nat, ceval_step st c i = Some st'
  induction Hce.st:state
exists i : nat, ceval_step st SKIP i = Some st
st:state
a1:aexp
n:nat
x:string
H:aeval st a1 = n
exists i : nat,
  ceval_step st (x ::= a1) i = Some (x !-> n; st)
c1, c2:com
st, st', st'':state
Hce1:st =[ c1 ]=> st'
Hce2:st' =[ c2 ]=> st''
IHHce1:exists i : nat, ceval_step st c1 i = Some st'
IHHce2:exists i : nat,
  ceval_step st' c2 i = Some st''
exists i : nat, ceval_step st (c1;; c2) i = Some st''
st, st':state
b:bexp
c1, c2:com
H:beval st b = true
Hce:st =[ c1 ]=> st'
IHHce:exists i : nat, ceval_step st c1 i = Some st'
exists i : nat,
  ceval_step st (TEST b THEN c1 ELSE c2 FI) i =
  Some st'
st, st':state
b:bexp
c1, c2:com
H:beval st b = false
Hce:st =[ c2 ]=> st'
IHHce:exists i : nat, ceval_step st c2 i = Some st'
exists i : nat,
  ceval_step st (TEST b THEN c1 ELSE c2 FI) i =
  Some st'
b:bexp
st:state
c:com
H:beval st b = false
exists i : nat,
  ceval_step st (WHILE b DO c END) i = Some st
st, st', st'':state
b:bexp
c:com
H:beval st b = true
Hce1:st =[ c ]=> st'
Hce2:st' =[ WHILE b DO c END ]=> st''
IHHce1:exists i : nat, ceval_step st c i = Some st'
IHHce2:exists i : nat,
  ceval_step st' (WHILE b DO c END) i =
  Some st''
exists i : nat,
  ceval_step st (WHILE b DO c END) i = Some st''
  (* FILL IN HERE *) Admitted.

☐

Theorem ceval_and_ceval_step_coincide: forall c st st',
      st =[ c ]=> st'
  <-> exists i, ceval_step st c i = Some st'.forall (c : com) (st st' : state),
st =[ c ]=> st' <->
(exists i : nat, ceval_step st c i = Some st')
Proof.forall (c : com) (st st' : state),
st =[ c ]=> st' <->
(exists i : nat, ceval_step st c i = Some st')
  intros c st st'.c:com
st, st':state
st =[ c ]=> st' <->
(exists i : nat, ceval_step st c i = Some st')
  split.c:com
st, st':state
st =[ c ]=> st' ->
exists i : nat, ceval_step st c i = Some st'
c:com
st, st':state
(exists i : nat, ceval_step st c i = Some st') ->
st =[ c ]=> st' apply ceval__ceval_step.c:com
st, st':state
(exists i : nat, ceval_step st c i = Some st') ->
st =[ c ]=> st' apply ceval_step__ceval.
Qed.

(* ################################################################# *)

Determinism of Evaluation Again

Using the fact that the relational and step-indexed definition of evaluation are the same, we can give a slicker proof that the evaluation relation is deterministic.

Theorem ceval_deterministic' : forall c st st1 st2,
     st =[ c ]=> st1 ->
     st =[ c ]=> st2 ->
     st1 = st2.forall (c : com) (st st1 st2 : state),
st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2
Proof.forall (c : com) (st st1 st2 : state),
st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2
  intros c st st1 st2 He1 He2.c:com
st, st1, st2:state
He1:st =[ c ]=> st1
He2:st =[ c ]=> st2
st1 = st2
  apply ceval__ceval_step in He1.c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:st =[ c ]=> st2
st1 = st2
  apply ceval__ceval_step in He2.c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
st1 = st2
  inversion He1 as [i1 E1].c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1:nat
E1:ceval_step st c i1 = Some st1
st1 = st2
  inversion He2 as [i2 E2].c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1:nat
E1:ceval_step st c i1 = Some st1
i2:nat
E2:ceval_step st c i2 = Some st2
st1 = st2
  apply ceval_step_more with (i2 := i1 + i2) in E1.c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1, i2:nat
E1:ceval_step st c (i1 + i2) = Some st1
E2:ceval_step st c i2 = Some st2
st1 = st2
c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1:nat
E1:ceval_step st c i1 = Some st1
i2:nat
E2:ceval_step st c i2 = Some st2
i1 <= i1 + i2
  apply ceval_step_more with (i2 := i1 + i2) in E2.c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1, i2:nat
E1:ceval_step st c (i1 + i2) = Some st1
E2:ceval_step st c (i1 + i2) = Some st2
st1 = st2
c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1, i2:nat
E1:ceval_step st c (i1 + i2) = Some st1
E2:ceval_step st c i2 = Some st2
i2 <= i1 + i2
c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1:nat
E1:ceval_step st c i1 = Some st1
i2:nat
E2:ceval_step st c i2 = Some st2
i1 <= i1 + i2
  rewrite E1 in E2.c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1, i2:nat
E1:ceval_step st c (i1 + i2) = Some st1
E2:Some st1 = Some st2
st1 = st2
c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1, i2:nat
E1:ceval_step st c (i1 + i2) = Some st1
E2:ceval_step st c i2 = Some st2
i2 <= i1 + i2
c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1:nat
E1:ceval_step st c i1 = Some st1
i2:nat
E2:ceval_step st c i2 = Some st2
i1 <= i1 + i2 inversion E2.c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1, i2:nat
E1:ceval_step st c (i1 + i2) = Some st1
E2:Some st1 = Some st2
H0:st1 = st2
st2 = st2
c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1, i2:nat
E1:ceval_step st c (i1 + i2) = Some st1
E2:ceval_step st c i2 = Some st2
i2 <= i1 + i2
c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1:nat
E1:ceval_step st c i1 = Some st1
i2:nat
E2:ceval_step st c i2 = Some st2
i1 <= i1 + i2 reflexivity.c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1, i2:nat
E1:ceval_step st c (i1 + i2) = Some st1
E2:ceval_step st c i2 = Some st2
i2 <= i1 + i2
c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1:nat
E1:ceval_step st c i1 = Some st1
i2:nat
E2:ceval_step st c i2 = Some st2
i1 <= i1 + i2
  omega.c:com
st, st1, st2:state
He1:exists i : nat, ceval_step st c i = Some st1
He2:exists i : nat, ceval_step st c i = Some st2
i1:nat
E1:ceval_step st c i1 = Some st1
i2:nat
E2:ceval_step st c i2 = Some st2
i1 <= i1 + i2 omega.  Qed.

(* Wed Jan 9 12:02:46 EST 2019 *)