Proof that small-step and big-step semantics for conditionals coincide.


Syntax

  t ::= true | false | if t0 then t1 else t2
  v ::= true | false


Small step, t --> t'

  if true then t1 else t2  -->  t1  (E-IfTrue)

  if false then t1 else t2  -->  t2  (E-IfFalse)

  t0 --> t0'
  ------------------------------------------------ (E-If)
  if t0 then t1 else t2 --> if t0' then t1 else t2


Big step, t => v

  v => v  (B-Value)

  t0 => true   t1 => v
  --------------------------  (B-IfTrue)
  if t0 then t1 else t2 => v 

  t0 => false   t2 => v
  --------------------------  (B-IfFalse)
  if t0 then t1 else t2 => v 


------------------------------------------------------------------------
PROPOSITION (Equivalence of big and small step).
We have t -->* v if and only if t => v.

As usual, we break this into proofs in the backward and forward directions.
The backward proof is straightforward, but the forward proof is not.
(Induction on the length of the reduction sequence gives us
t0 --> t0' and if t0' then t1 else t2 => v, but it is not easy to put
these two together.)  So we prove the backward direction, and first
prove a destructuring lemma for small-step reductions (which is an
easy induction on the length of the reduction sequence), and then prove
the forward direction.

------------------------------------------------------------------------
PROPOSITION (backward implication).  If  t => v  then  t -->* v.

PROOF.  By induction on the height of t => v and case analsys on the
last rule in the derivation.

* Case:

  v => v.

Immediate.

* Case:

  t0 => true   t1 => v
  --------------------------  (B-IfTrue)
  if t0 then t1 else t2 => v 

By induction hypothesis, we have:

  t0 -->* true   t1 -->* v

whence:

  if t0 then t1 else t2 -->* if true then t1 else t2 --> t1 -->* v

* Case:

  t0 => false   t2 => v
  --------------------------  (B-IfFalse)
  if t0 then t1 else t2 => v 

Similar to the previous case.  QED.


------------------------------------------------------------------------
PROPOSITION (destructuring lemma).  If

  if t0 then t1 else t2 -->* v

then either

  t0 -->* true and t1 -->* v  or else  t0 -->* false and t2 -->* v,

and each of these sequences is shorter than the original sequence.

PROOF.  By induction on the length of  if t0 then t1 else t2 -->* v,
and case analysis on the first reduction in the sequence.  The sequence
cannot be empty, since the initial term is not a value.

* Case

  t0 --> t0'
  ------------------------------------------------ (E-If)
  if t0 then t1 else t2 --> if t0' then t1 else t2

By the induction hypothesis we know

  t0' -->* true and t1 -->* v  or else  t0' -->* false and t2 -->* v

Say the first of these holds, then we form

  t0 --> t0' -->* true and t1 -->* v

and similarly in the other case.  Note that the new sequences are
still strictly shorter than the original.

* Case

  if true then t1 else t2 --> t1 (T-IfTrue)

Then by the hypothesis, the rest of the sequence is t1 -->* v,
and we are done.

* Case

  if false then t1 else t2 --> t2 (T-IfFalse)

is similar.  QED.


------------------------------------------------------------------------
PROPOSITION (forward implication).  If  t -->* v  then  t => v.

PROOF.  By induction on the length of t -->* v and case analysis on t.

* Case t is a value.  Then v -->* v and v => v, trivially.

* Case t is (if t0 then t1 else t2).  Then by the destructuring lemma
we know

  t0 -->* true and t1 -->* v  or else  t0 -->* false and t2 -->* v

where the new reduction sequences are strictly shorter, so the
induction hypothesis applies.  Hence we have

  t0 => true  t1 => v                  t0 => false  t2 => v               
  --------------------------  or else  --------------------------	    
  if t0 then t1 else t2 => v	       if t0 then t1 else t2 => v

as required. QED.