Exercises: Big-step / Small-step Equivalence

Author

Aurèle Barrière, Adam Chlipala, Benjamin C. Pierce

License

No redistribution allowed (usage by permission in CS-428).

From Stdlib Require Import String List Arith Lia.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.
Set Implicit Arguments.

Definitions and notations

Here are the definitions and notations from the small-step semantics lecture.

Notation var := string.

Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Minus (e1 e2 : arith)
| Times (e1 e2 : arith).

Coercion Const : nat >-> arith.Const is now a coercion
Coercion Var : var >-> arith.Var is now a coercion
Declare Scope arith_scope.
Infix "+" := Plus : arith_scope.
Infix "-" := Minus : arith_scope.
Infix "*" := Times : arith_scope.
Delimit Scope arith_scope with arith.

Definition valuation := var -> option nat.

Definition empty : valuation := fun _ => None.
Notation "$0" := (empty).

Definition get (x:var) (v:valuation) : option nat := v x.
Notation "v $? x" := (get x v) (at level 50, left associativity).

Definition set (x:var) (n:nat) (v:valuation) : valuation :=
  fun y =>
    match string_dec x y with
        | left H => Some n
        | right H' => get y v
    end.
Notation "v $+ ( x , k )" :=
  (set x k v) (at level 50, left associativity).

Fixpoint interp (e : arith) (v : valuation) : nat :=
  match e with
  | Const n => n
  | Var x =>
    match get x v with
    | None => 0
    | Some n => n
    end
  | Plus e1 e2 => interp e1 v + interp e2 v
  | Minus e1 e2 => interp e1 v - interp e2 v
  | Times e1 e2 => interp e1 v * interp e2 v
  end.

Inductive cmd :=
| Skip
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| If (e : arith) (then_ else_ : cmd)
| While (e : arith) (body : cmd).

Notation "x <- e" := (Assign x e%arith) (at level 75).
Infix ";;" := Sequence (at level 76).
Notation "'when' e 'then' then_ 'else' else_ 'done'" :=
  (If e%arith then_ else_) (at level 75, e at level 0).
Notation "'while' e 'loop' body 'done'" :=
  (While e%arith body) (at level 75).

Inductive eval : valuation -> cmd -> valuation -> Prop :=
| EvalSkip : forall v,
    eval v Skip v
| EvalAssign : forall v x e,
    eval v (Assign x e) (v $+ (x, interp e v))
| EvalSeq : forall v c1 v1 c2 v2,
    eval v c1 v1
    -> eval v1 c2 v2
    -> eval v (Sequence c1 c2) v2
| EvalIfTrue : forall v e then_ else_ v',
    interp e v <> 0
    -> eval v then_ v'
    -> eval v (If e then_ else_) v'
| EvalIfFalse : forall v e then_ else_ v',
    interp e v = 0
    -> eval v else_ v'
    -> eval v (If e then_ else_) v'
| EvalWhileTrue : forall v e body v' v'',
    interp e v <> 0
    -> eval v body v'
    -> eval v' (While e body) v''
    -> eval v (While e body) v''
| EvalWhileFalse : forall v e body,
    interp e v = 0
    -> eval v (While e body) v.

Inductive step : valuation * cmd -> valuation * cmd -> Prop :=
| StepAssign : forall v x e,
    step (v, Assign x e) (v $+ (x, interp e v), Skip)
| StepSeq1 : forall v c1 c2 v' c1',
    step (v, c1) (v', c1')
    -> step (v, Sequence c1 c2) (v', Sequence c1' c2)
| StepSeq2 : forall v c2,
    step (v, Sequence Skip c2) (v, c2)
| StepIfTrue : forall v e then_ else_,
    interp e v <> 0
    -> step (v, If e then_ else_) (v, then_)
| StepIfFalse : forall v e then_ else_,
    interp e v = 0
    -> step (v, If e then_ else_) (v, else_)
| StepWhileTrue : forall v e body,
    interp e v <> 0
    -> step (v, While e body) (v, Sequence body (While e body))
| StepWhileFalse : forall v e body,
    interp e v = 0
    -> step (v, While e body) (v, Skip).

Inductive trc {A:Type} {R:A -> A -> Prop}: A -> A -> Prop :=
| TrcRefl : forall x, trc x x
| TrcFront : forall x y z
               (STEP: R x y)
               (STAR: trc y z),
    trc x z.

Notation "R ^*" := (@trc _ R) (at level 0).

We have seen two styles of defining semantics for the same language. Each has their own advantages. It also turns out that these two semantics styles are equivalent. Let's prove it.

First, we need some intermediate lemmas.

  Lemma multi_step_trans:
    forall v1 c1 v2 c2 v3 c3
      (STAR1: step^* (v1,c1) (v2,c2))
      (STAR2: step^* (v2,c2) (v3,c3)),
      step^* (v1,c1) (v3,c3).forall (v1 : valuation) (c1 : cmd) (v2 : valuation)
  (c2 : cmd) (v3 : valuation) (c3 : cmd),
(step) ^* (v1, c1) (v2, c2) ->
(step) ^* (v2, c2) (v3, c3) ->
(step) ^* (v1, c1) (v3, c3)

Solution

  Proof.forall (v1 : valuation) (c1 : cmd) (v2 : valuation)
  (c2 : cmd) (v3 : valuation) (c3 : cmd),
(step) ^* (v1, c1) (v2, c2) ->
(step) ^* (v2, c2) (v3, c3) ->
(step) ^* (v1, c1) (v3, c3)
    intros v1 c1 v2 c2 v3 c3 STAR1 STAR2.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
STAR1: (step) ^* (v1, c1) (v2, c2)
STAR2: (step) ^* (v2, c2) (v3, c3)
(step) ^* (v1, c1) (v3, c3) induction STAR1; auto.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: valuation * cmd
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
(step) ^* x (v3, c3)
    econstructor.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: valuation * cmd
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
step x ?y
v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: valuation * cmd
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
(step) ^* ?y (v3, c3) apply STEP.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: valuation * cmd
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
(step) ^* y (v3, c3)
    apply IHSTAR1.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: valuation * cmd
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
(step) ^* z (v3, c3) assumption.
  Qed.

  Lemma step_star_Seq1 :
    forall s1 s2 c,
    step^* s1 s2 ->
    step^* (fst s1, Sequence (snd s1) c) (fst s2, Sequence (snd s2) c).forall (s1 s2 : valuation * cmd) (c : cmd),
(step) ^* s1 s2 ->
(step) ^* (fst s1, snd s1;; c) (fst s2, snd s2;; c)

Solution

  Proof.forall (s1 s2 : valuation * cmd) (c : cmd),
(step) ^* s1 s2 ->
(step) ^* (fst s1, snd s1;; c) (fst s2, snd s2;; c)
    intros s1 s2 c H.s1, s2: valuation * cmd
c: cmd
H: (step) ^* s1 s2
(step) ^* (fst s1, snd s1;; c) (fst s2, snd s2;; c)
    induction H.c: cmd
x: valuation * cmd
(step) ^* (fst x, snd x;; c) (fst x, snd x;; c)
c: cmd
x, y, z: valuation * cmd
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c) (fst z, snd z;; c)
(step) ^* (fst x, snd x;; c) (fst z, snd z;; c)
    -c: cmd
x: valuation * cmd
(step) ^* (fst x, snd x;; c) (fst x, snd x;; c) constructor.
    -c: cmd
x, y, z: valuation * cmd
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c) (fst z, snd z;; c)
(step) ^* (fst x, snd x;; c) (fst z, snd z;; c) destruct y.c: cmd
x: valuation * cmd
v: valuation
c0: cmd
z: valuation * cmd
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
(step) ^* (fst x, snd x;; c) (fst z, snd z;; c) econstructor.c: cmd
x: valuation * cmd
v: valuation
c0: cmd
z: valuation * cmd
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (fst x, snd x;; c) ?y
c: cmd
x: valuation * cmd
v: valuation
c0: cmd
z: valuation * cmd
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
(step) ^* ?y (fst z, snd z;; c)
      2: {c: cmd
x: valuation * cmd
v: valuation
c0: cmd
z: valuation * cmd
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
(step) ^* ?y (fst z, snd z;; c) eapply IHtrc. }c: cmd
x: valuation * cmd
v: valuation
c0: cmd
z: valuation * cmd
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (fst x, snd x;; c) (fst (v, c0), snd (v, c0);; c)
      constructor.c: cmd
x: valuation * cmd
v: valuation
c0: cmd
z: valuation * cmd
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (fst x, snd x) (fst (v, c0), snd (v, c0)) destruct x.c: cmd
v0: valuation
c1: cmd
v: valuation
c0: cmd
z: valuation * cmd
STEP: step (v0, c1) (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (fst (v0, c1), snd (v0, c1))
  (fst (v, c0), snd (v, c0)) simpl.c: cmd
v0: valuation
c1: cmd
v: valuation
c0: cmd
z: valuation * cmd
STEP: step (v0, c1) (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (v0, c1) (v, c0) assumption.
  Qed.

This works well, but why did we state the theorem using fst and snd instead of giving a name to each element of each state? That would have been a more straightforward statement.

This is once again because induction is going to forget about some much needed equalities. We will look at three possible solutions:

State the theorems on pairs and use fst and snd as shown above.
Use the remember tactic as we saw two weeks ago.
Use the dependent induction tactic which generalizes as much as possible. See the reference manual for more details and examples.

  Lemma step_star_Seq_remember : forall v c1 c2 v' c1',
      step^* (v, c1) (v', c1')
      -> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).forall (v : valuation) (c1 c2 : cmd) 
  (v' : valuation) (c1' : cmd),
(step) ^* (v, c1) (v', c1') ->
(step) ^* (v, c1;; c2) (v', c1';; c2)

Solution

  Proof.forall (v : valuation) (c1 c2 : cmd) 
  (v' : valuation) (c1' : cmd),
(step) ^* (v, c1) (v', c1') ->
(step) ^* (v, c1;; c2) (v', c1';; c2)
    intros v c1 c2 v' c1' H.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: (step) ^* (v, c1) (v', c1')
(step) ^* (v, c1;; c2) (v', c1';; c2)
    remember (v, c1) as x.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: valuation * cmd
Heqx: x = (v, c1)
H: (step) ^* x (v', c1')
(step) ^* (v, c1;; c2) (v', c1';; c2)
    remember (v', c1') as y.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: valuation * cmd
Heqx: x = (v, c1)
y: valuation * cmd
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (v, c1;; c2) (v', c1';; c2)
    replace v with (fst x) by (subst;auto).v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: valuation * cmd
Heqx: x = (v, c1)
y: valuation * cmd
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (fst x, c1;; c2) (v', c1';; c2)
    replace v' with (fst y) by (subst;auto).v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: valuation * cmd
Heqx: x = (v, c1)
y: valuation * cmd
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (fst x, c1;; c2) (fst y, c1';; c2)
    replace c1 with (snd x) by (subst;auto).v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: valuation * cmd
Heqx: x = (v, c1)
y: valuation * cmd
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (fst x, snd x;; c2) (fst y, c1';; c2)
    replace c1' with (snd y) by (subst;auto).v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: valuation * cmd
Heqx: x = (v, c1)
y: valuation * cmd
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (fst x, snd x;; c2) (fst y, snd y;; c2)
    (* if we don't clear we don't get the right induction! *)
    clear v v' c1 c1' Heqx Heqy.c2: cmd
x, y: valuation * cmd
H: (step) ^* x y
(step) ^* (fst x, snd x;; c2) (fst y, snd y;; c2)
    induction H; subst.c2: cmd
x: valuation * cmd
(step) ^* (fst x, snd x;; c2) (fst x, snd x;; c2)
c2: cmd
x, y, z: valuation * cmd
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2) (fst z, snd z;; c2)
(step) ^* (fst x, snd x;; c2) (fst z, snd z;; c2)
    -c2: cmd
x: valuation * cmd
(step) ^* (fst x, snd x;; c2) (fst x, snd x;; c2) constructor.
    -c2: cmd
x, y, z: valuation * cmd
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2) (fst z, snd z;; c2)
(step) ^* (fst x, snd x;; c2) (fst z, snd z;; c2) econstructor.c2: cmd
x, y, z: valuation * cmd
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2) (fst z, snd z;; c2)
step (fst x, snd x;; c2) ?y
c2: cmd
x, y, z: valuation * cmd
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2) (fst z, snd z;; c2)
(step) ^* ?y (fst z, snd z;; c2)
      2: apply IHtrc.c2: cmd
x, y, z: valuation * cmd
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2) (fst z, snd z;; c2)
step (fst x, snd x;; c2) (fst y, snd y;; c2)
      constructor.c2: cmd
x, y, z: valuation * cmd
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2) (fst z, snd z;; c2)
step (fst x, snd x) (fst y, snd y) destruct x, y.c2: cmd
v: valuation
c: cmd
v0: valuation
c0: cmd
z: valuation * cmd
STEP: step (v, c) (v0, c0)
H: (step) ^* (v0, c0) z
IHtrc: (step) ^* (fst (v0, c0), snd (v0, c0);; c2)
  (fst z, snd z;; c2)
step (fst (v, c), snd (v, c))
  (fst (v0, c0), snd (v0, c0)) assumption.
  Qed.

Not very convenient. Let's look at the dependent induction tactic.

  #[warnings="-require-in-module"]
  From Stdlib Require Import Program.Equality.

  Lemma step_star_Seq : forall v c1 c2 v' c1',
    step^* (v, c1) (v', c1')
    -> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).forall (v : valuation) (c1 c2 : cmd) 
  (v' : valuation) (c1' : cmd),
(step) ^* (v, c1) (v', c1') ->
(step) ^* (v, c1;; c2) (v', c1';; c2)

Solution

  Proof.forall (v : valuation) (c1 c2 : cmd) 
  (v' : valuation) (c1' : cmd),
(step) ^* (v, c1) (v', c1') ->
(step) ^* (v, c1;; c2) (v', c1';; c2)
    intros.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: (step) ^* (v, c1) (v', c1')
(step) ^* (v, c1;; c2) (v', c1';; c2)
    dependent induction H.c2: cmd
v': valuation
c1': cmd
(step) ^* (v', c1';; c2) (v', c1';; c2)
c2: cmd
v: valuation
c1: cmd
y: valuation * cmd
v': valuation
c1': cmd
STEP: step (v, c1) y
H: (step) ^* y (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd) (v'0 : valuation)
  (c1'0 : cmd),
y = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* (v, c1;; c2) (v', c1';; c2)
    -c2: cmd
v': valuation
c1': cmd
(step) ^* (v', c1';; c2) (v', c1';; c2) constructor.
    -c2: cmd
v: valuation
c1: cmd
y: valuation * cmd
v': valuation
c1': cmd
STEP: step (v, c1) y
H: (step) ^* y (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd) (v'0 : valuation)
  (c1'0 : cmd),
y = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* (v, c1;; c2) (v', c1';; c2) destruct y.c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd) (v'0 : valuation)
  (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* (v, c1;; c2) (v', c1';; c2) econstructor.c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd) (v'0 : valuation)
  (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
step (v, c1;; c2) ?y
c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd) (v'0 : valuation)
  (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* ?y (v', c1';; c2)
      2: {c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd) (v'0 : valuation)
  (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* ?y (v', c1';; c2) eapply IHtrc; reflexivity. }c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd) (v'0 : valuation)
  (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
step (v, c1;; c2) (v0, c;; c2)
      constructor.c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd) (v'0 : valuation)
  (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
step (v, c1) (v0, c)  assumption.
  Qed.

We can now resume our proof. First, let's show that a big-step reduction implies a multi-step small-step reduction to a final state.

  Theorem big_small :
    forall v c v',
      eval v c v' ->
      step^* (v, c) (v', Skip).forall (v : valuation) (c : cmd) (v' : valuation),
eval v c v' -> (step) ^* (v, c) (v', Skip)

Solution

  Proof.forall (v : valuation) (c : cmd) (v' : valuation),
eval v c v' -> (step) ^* (v, c) (v', Skip)
    intros v c v' H.v: valuation
c: cmd
v': valuation
H: eval v c v'
(step) ^* (v, c) (v', Skip) induction H.v: valuation
(step) ^* (v, Skip) (v, Skip)
v: valuation
x: var
e: arith
(step) ^* (v, x <- e) (v $+ (x, interp e v), Skip)
v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1) (v1, Skip)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v, c1;; c2) (v2, Skip)
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
(step) ^* (v, when e then then_ else else_ done)
  (v', Skip)
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
(step) ^* (v, when e then then_ else else_ done)
  (v', Skip)
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v, while e loop body done) (v'', Skip)
v: valuation
e: arith
body: cmd
H: interp e v = 0
(step) ^* (v, while e loop body done) (v, Skip)
    -v: valuation
(step) ^* (v, Skip) (v, Skip) constructor.
    -v: valuation
x: var
e: arith
(step) ^* (v, x <- e) (v $+ (x, interp e v), Skip) econstructor; constructor.
    -v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1) (v1, Skip)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v, c1;; c2) (v2, Skip) apply step_star_Seq with (c2:=c2) in IHeval1.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v, c1;; c2) (v2, Skip)
      eapply multi_step_trans.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v, c1;; c2) (?v2, ?c2)
v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (?v2, ?c2) (v2, Skip) apply IHeval1.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v1, Skip;; c2) (v2, Skip)
      econstructor.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
step (v1, Skip;; c2) ?y
v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* ?y (v2, Skip) apply StepSeq2.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v1, c2) (v2, Skip) assumption.
    -v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
(step) ^* (v, when e then then_ else else_ done)
  (v', Skip) econstructor.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
step (v, when e then then_ else else_ done) ?y
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
(step) ^* ?y (v', Skip)
      {v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
step (v, when e then then_ else else_ done) ?y apply StepIfTrue.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
interp e v <> 0 assumption. }v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
(step) ^* (v, then_) (v', Skip)
      assumption.
    -v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
(step) ^* (v, when e then then_ else else_ done)
  (v', Skip) econstructor.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
step (v, when e then then_ else else_ done) ?y
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
(step) ^* ?y (v', Skip)
      {v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
step (v, when e then then_ else else_ done) ?y apply StepIfFalse.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
interp e v = 0 assumption. }v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
(step) ^* (v, else_) (v', Skip)
      assumption.
    -v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v, while e loop body done) (v'', Skip) econstructor.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
step (v, while e loop body done) ?y
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* ?y (v'', Skip)
      {v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
step (v, while e loop body done) ?y apply StepWhileTrue.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
interp e v <> 0 assumption. }v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (v'', Skip)
      eapply multi_step_trans.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (?v2, ?c2)
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (?v2, ?c2) (v'', Skip)
      2: {v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (?v2, ?c2) (v'', Skip) apply IHeval2. }v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (v', while e loop body done)
      eapply multi_step_trans.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (?v2, ?c2)
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (?v2, ?c2) (v', while e loop body done)
      {v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (?v2, ?c2) apply step_star_Seq.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v, body) (?v2, ?c1') apply IHeval1. }v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v', Skip;; while e loop body done)
  (v', while e loop body done)
      econstructor.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
step (v', Skip;; while e loop body done) ?y
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* ?y (v', while e loop body done) apply StepSeq2.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done) (v'', Skip)
(step) ^* (v', while e loop body done)
  (v', while e loop body done) constructor.
    -v: valuation
e: arith
body: cmd
H: interp e v = 0
(step) ^* (v, while e loop body done) (v, Skip) econstructor.v: valuation
e: arith
body: cmd
H: interp e v = 0
step (v, while e loop body done) ?y
v: valuation
e: arith
body: cmd
H: interp e v = 0
(step) ^* ?y (v, Skip)
      {v: valuation
e: arith
body: cmd
H: interp e v = 0
step (v, while e loop body done) ?y apply StepWhileFalse.v: valuation
e: arith
body: cmd
H: interp e v = 0
interp e v = 0 assumption. }v: valuation
e: arith
body: cmd
H: interp e v = 0
(step) ^* (v, Skip) (v, Skip)
      constructor.
  Qed.

Now for the other direction, we start at the level of the fine-grain step then work our way to the multi-step relation.

  Lemma small_big_fs: forall x y,
      step x y ->
      forall v', eval (fst y) (snd y) v' ->
            eval (fst x) (snd x) v'.forall x y : valuation * cmd,
step x y ->
forall v' : valuation,
eval (fst y) (snd y) v' -> eval (fst x) (snd x) v'

Solution

  Proof.forall x y : valuation * cmd,
step x y ->
forall v' : valuation,
eval (fst y) (snd y) v' -> eval (fst x) (snd x) v'
    intros x y H.x, y: valuation * cmd
H: step x y
forall v' : valuation,
eval (fst y) (snd y) v' -> eval (fst x) (snd x) v' induction H; intros; simpl in *.v: valuation
x: var
e: arith
v': valuation
H: eval (v $+ (x, interp e v)) Skip v'
eval v (x <- e) v'
v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
eval v (c1;; c2) v'0
v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval v (Skip;; c2) v'
v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
v': valuation
H0: eval v then_ v'
eval v (when e then then_ else else_ done) v'
v: valuation
e: arith
then_, else_: cmd
H: interp e v = 0
v': valuation
H0: eval v else_ v'
eval v (when e then then_ else else_ done) v'
v: valuation
e: arith
body: cmd
H: interp e v <> 0
v': valuation
H0: eval v (body;; while e loop body done) v'
eval v (while e loop body done) v'
v: valuation
e: arith
body: cmd
H: interp e v = 0
v': valuation
H0: eval v Skip v'
eval v (while e loop body done) v'
    -v: valuation
x: var
e: arith
v': valuation
H: eval (v $+ (x, interp e v)) Skip v'
eval v (x <- e) v' inversion H.v: valuation
x: var
e: arith
v': valuation
H: eval (v $+ (x, interp e v)) Skip v'
v0: valuation
H0: v0 = v $+ (x, interp e v)
H2: v $+ (x, interp e v) = v'
eval v (x <- e) (v $+ (x, interp e v)) subst.v: valuation
x: var
e: arith
H: eval (v $+ (x, interp e v)) Skip
  (v $+ (x, interp e v))
eval v (x <- e) (v $+ (x, interp e v)) constructor.
    -v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
eval v (c1;; c2) v'0 inversion H0.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v0: valuation
c0: cmd
v1: valuation
c3: cmd
v2: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
H3: v0 = v'
H1: c0 = c1'
H2: c3 = c2
H5: v2 = v'0
eval v (c1;; c2) v'0 subst.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v (c1;; c2) v'0 econstructor.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v c1 ?v1
v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval ?v1 c2 v'0
      +v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v c1 ?v1 apply IHstep.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v' c1' ?v1 eassumption.
      +v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v1 c2 v'0 assumption.
    -v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval v (Skip;; c2) v' econstructor.v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval v Skip ?v1
v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval ?v1 c2 v' constructor.v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval v c2 v' assumption.
    -v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
v': valuation
H0: eval v then_ v'
eval v (when e then then_ else else_ done) v' constructor; assumption.
    -v: valuation
e: arith
then_, else_: cmd
H: interp e v = 0
v': valuation
H0: eval v else_ v'
eval v (when e then then_ else else_ done) v' apply EvalIfFalse; assumption.
    -v: valuation
e: arith
body: cmd
H: interp e v <> 0
v': valuation
H0: eval v (body;; while e loop body done) v'
eval v (while e loop body done) v' inversion H0.v: valuation
e: arith
body: cmd
H: interp e v <> 0
v': valuation
H0: eval v (body;; while e loop body done) v'
v0: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H4: eval v body v1
H6: eval v1 (while e loop body done) v'
H3: v0 = v
H1: c1 = body
H2: c2 = (while e loop body done)
H5: v2 = v'
eval v (while e loop body done) v' subst.v: valuation
e: arith
body: cmd
H: interp e v <> 0
v': valuation
H0: eval v (body;; while e loop body done) v'
v1: valuation
H4: eval v body v1
H6: eval v1 (while e loop body done) v'
eval v (while e loop body done) v' econstructor; eassumption.
    -v: valuation
e: arith
body: cmd
H: interp e v = 0
v': valuation
H0: eval v Skip v'
eval v (while e loop body done) v' inversion H0.v: valuation
e: arith
body: cmd
H: interp e v = 0
v': valuation
H0: eval v Skip v'
v0: valuation
H1: v0 = v
H3: v = v'
eval v' (while e loop body done) v' subst.e: arith
body: cmd
v': valuation
H0: eval v' Skip v'
H: interp e v' = 0
eval v' (while e loop body done) v' apply EvalWhileFalse.e: arith
body: cmd
v': valuation
H0: eval v' Skip v'
H: interp e v' = 0
interp e v' = 0 assumption.
  Qed.

  Lemma small_big'' : forall v c v' c',
      step (v, c) (v', c') ->
      forall v'', eval v' c' v'' ->
             eval v c v''.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
step (v, c) (v', c') ->
forall v'' : valuation, eval v' c' v'' -> eval v c v''

Solution

  Proof.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
step (v, c) (v', c') ->
forall v'' : valuation, eval v' c' v'' -> eval v c v''
    intros v c v' c' H v'' H0.v: valuation
c: cmd
v': valuation
c': cmd
H: step (v, c) (v', c')
v'': valuation
H0: eval v' c' v''
eval v c v''
    eapply small_big_fs in H; simpl.v: valuation
c: cmd
v': valuation
c': cmd
v'': valuation
H0: eval v' c' v''
H: eval (fst (v, c)) (snd (v, c)) ?v'
eval v c v''
v: valuation
c: cmd
v': valuation
c': cmd
H: step (v, c) (v', c')
v'': valuation
H0: eval v' c' v''
eval v' c' ?v' 2: eassumption.v: valuation
c: cmd
v': valuation
c': cmd
v'': valuation
H0: eval v' c' v''
H: eval (fst (v, c)) (snd (v, c)) v''
eval v c v''
    simpl in H.v: valuation
c: cmd
v': valuation
c': cmd
v'': valuation
H0: eval v' c' v''
H: eval v c v''
eval v c v'' assumption.
  Qed.

  Lemma small_big' :
    forall v c v' c',
      step^* (v, c) (v', c') ->
      forall v'', eval v' c' v'' ->
             eval v c v''.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
(step) ^* (v, c) (v', c') ->
forall v'' : valuation, eval v' c' v'' -> eval v c v''

Solution

  Proof.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
(step) ^* (v, c) (v', c') ->
forall v'' : valuation, eval v' c' v'' -> eval v c v''
    intros v c v' c' H.v: valuation
c: cmd
v': valuation
c': cmd
H: (step) ^* (v, c) (v', c')
forall v'' : valuation, eval v' c' v'' -> eval v c v''
    dependent induction H; intros; try assumption.v: valuation
c: cmd
y: valuation * cmd
v': valuation
c': cmd
STEP: step (v, c) y
H: (step) ^* y (v', c')
IHtrc: forall (v : valuation) (c : cmd) (v'0 : valuation)
  (c'0 : cmd),
y = (v, c) ->
(v', c') = (v'0, c'0) ->
forall v'' : valuation,
eval v'0 c'0 v'' -> eval v c v''
v'': valuation
H0: eval v' c' v''
eval v c v''
    destruct y.v: valuation
c: cmd
v0: valuation
c0: cmd
v': valuation
c': cmd
STEP: step (v, c) (v0, c0)
H: (step) ^* (v0, c0) (v', c')
IHtrc: forall (v : valuation) (c : cmd) (v'0 : valuation)
  (c'0 : cmd),
(v0, c0) = (v, c) ->
(v', c') = (v'0, c'0) ->
forall v'' : valuation,
eval v'0 c'0 v'' -> eval v c v''
v'': valuation
H0: eval v' c' v''
eval v c v'' eapply IHtrc in H0; auto.v: valuation
c: cmd
v0: valuation
c0: cmd
v': valuation
c': cmd
STEP: step (v, c) (v0, c0)
H: (step) ^* (v0, c0) (v', c')
IHtrc: forall (v : valuation) (c : cmd) (v'0 : valuation)
  (c'0 : cmd),
(v0, c0) = (v, c) ->
(v', c') = (v'0, c'0) ->
forall v'' : valuation,
eval v'0 c'0 v'' -> eval v c v''
v'': valuation
H0: eval v0 c0 v''
eval v c v''
    eapply small_big''; eauto.
  Qed.

  Theorem small_big :
    forall v c v',
       step^* (v, c) (v', Skip) ->
       eval v c v'.forall (v : valuation) (c : cmd) (v' : valuation),
(step) ^* (v, c) (v', Skip) -> eval v c v'
  Proof.forall (v : valuation) (c : cmd) (v' : valuation),
(step) ^* (v, c) (v', Skip) -> eval v c v'
    intros v c v' H.v: valuation
c: cmd
v': valuation
H: (step) ^* (v, c) (v', Skip)
eval v c v' eapply small_big'; eauto.v: valuation
c: cmd
v': valuation
H: (step) ^* (v, c) (v', Skip)
eval v' Skip v' constructor.
  Qed.