Proof of Equivalence

Prove e ↓ v ==> e |->* Num v.


We proceed by rule induction on the definition of the big-step judgement.
We pick P(e, v) ≡ e |->* Num v, and prove by induction e ↓ v ==> P(e, v).

There is one case for each of the 4 inference rules that characterise the
big-step semantics.


Base case: associated with (Num n) ↓ n.
We must show P(Num n, n) ≡ Num n |->* Num n.

This follows, it is just the base case (reflexivity) of the
reflexive-transitive closure.


Inductive case 1: associated with the Plus rule:

  e1 ↓ v1         e2 ↓ v2
---------------------------  <- this rule
  (Plus e1 e2) ↓ (v1 + v2)


We assume IHs:
IH1: P(e1, v1) ≡ e1 |->* Num v1.
IH2: P(e2, v2) ≡ e2 |->* Num v2.

We must show:
P(Plus e1 e2, v1 + v2) ≡ Plus e1 e2 |->* Num (v1 + v2).


We need to use a contextual lemma, Lemma 1:

        e1 |->* e1_2
----------------------------
Plus e1 e2 |->* Plus e1_2 e2

We will not prove this in detail. It can be shown by rule induction on the
recursive-transitive-closure assumption. The interesting case then uses the
contextual rule for the small-step relation.


We are trying to show:
Plus e1 e2 |->* Num (v1 + v2).


Plus e1 e2
    |->* Plus (Num v1) e2          -- by contextual rule and IH1
    |->* Plus (Num v1) (Num v2)    -- by (right) contextual rule and IH2
    |->* Num (v1 + v2).            -- from the small-step rules

This is a sketch proof. To put the whole thing together,
we'd need to prove *both* the contextual rules, and transitivity
of the recursive transitive relation.


Inductive case 2: The Times case is exactly analagous to Plus.



Inductive case 3: The Let case.

This case is associated with the Let rule of the big-step judgement:

  e1 ↓ v1         e2[x := Num v1] ↓ v2
----------------------------------------  <- this rule
        (Let x e1 e2) ↓ v2


We assume IHs:
IH1: P(e1, v1) ≡ e1 |->* Num v1.
IH2: P(e2[x := Num v1], v2) ≡ e2[x := Num v1] |->* Num v2.


We need to prove P(Let x e1 e2, v2) ≡ Let x e1 e2 |->* Num v2.


Again, we need a contextual rule that establishes that any chain of small-steps
that rewrite e1 into e1' implies a chain from Let x e1 e2 to Let x e1' e2.


Let x e1 e2
  |->* Let x (Num v1) e2     -- from IH1 and the contextual rule
  |->* e2[x := Num v1]       -- using the Let single-step rule
  |->* Num v2.               -- exactly IH2

Gluing these together with transitivity gives the required result.


This completes the (sketch) proof that the big-step judgement implies a
matching small-step evaluation.

Prove e |->* Num v ==> e ↓ v.


We prove this by rule induction on the definition of the recursive-transitive
closure, using Q(e1, e2) ≡ (∀n. e2 = Num n ==> e1 ↓ n).


Base case (associated with reflexivity rule):


Show Q(e, e) ≡ (∀n. e = Num n ==> e ↓ n).


OK, we fix n, assume A: e = Num n, and must show e ↓ n.


 -----------    -- defining big-step rule
  Num n ↓ n
-------------   -- rewriting using A
    e ↓ n


Inductive case (associated with the step rule of the rec-trans-closure):

Assume premise P1: e1 |-> e2.
Assume IH: Q(e2, e3) ≡ (∀n. e3 = Num n ==> e2 ↓ n).

We must show Q(e1, e3) ≡ (∀n. e3 = Num n ==> e1 ↓ n).


OK, so we fix n, and assume A: e3 = Num n.

A and IH together give us A2: e2 ↓ n.

We need to show e1 ↓ n.


This case requires another induction, so we phrase our case as Lemma 2:


  e |-> e2    e2 ↓ n
----------------------
       e ↓ n


Once we have proven Lemma 1, we can use it with P1 and A2 to prove our goal.
That completes a proof by induction of Q, that is:
∀e1 e2. e1 |->* e2 ==> (∀n. e2 = Num n ==> e1 ↓ n).


This fact can then be used to prove e1 |->* Num n ==> e1 ↓ n as required.


So, we need to prove Lemma 2. However, we will first prove Lemma 3, determinism
of big-step semantics, which will simplify the proof of Lemma 2.


Lemma 3:


  e ↓ v1    e ↓ v2
--------------------
     v1 = v2


Studying the big-step semantics, this may be "obvious". There is only ever one
rule that can apply for a given left-hand-side expression, and the
right-hand-side value it results in is fixed. Anyway.


We prove this by rule induction on the definition of the big-step relation,
proving R(e, v1) ≡ (∀v2. e ↓ v2 ==> v1 = v2).



Base case: associated with the numeral rule of the big-step semantics:


R(Num n, n) ≡ (∀v2. Num n ↓ v2 ==> n = v2).


So, we fix v2 and assume that A: Num n ↓ v2.


We need to make use of the big-step relation in A again. We could do this by
proving a lemma by induction, which would look like this:
∀e v. e ↓ v ==> (∀n. e = Num n ==> v = n).


This induction would be "silly", with every case being straightforward (most
of them are contradictory, e.g. requiring Plus e1 e2 = Num n) and none of the
induction hypotheses being used.


Instead, let us use a new proof technique. We will case split on A: Num n ↓ v2.
We are assuming that this judgement is true, i.e. that it has a proof using the
rules of the big-step relation. We will case split on the final step in that
proof. This is essentially the same thing as doing an induction and dropping
the induction hypotheses.


So, we case split on A: Num n ↓ v2. Three of the big-step rules create
contradictory cases, only one rule is compatible with the left-hand-side being
Num n, and it requires the right hand side to be n. This establishes that
n = v2, which was our goal.


The other cases of Lemma 3 are similar. This skips having to do the case-splits
in the proof of Lemma 2.


Finally, we turn our attention to Lemma 2:


  e |-> e2    e2 ↓ n
----------------------
       e ↓ n


We prove this by rule induction on the definition of the small-step relation,
proving S(e, e2) ≡ (∀n. e2 ↓ n ==> e ↓ n).


Base case 1: associated with the plus-numeral case:


We must show S(Plus (Num n) (Num m), Num (n + m)) ≡
(∀n2. Num (n + m) ↓ n2 ==> Plus (Num n) (Num m) ↓ n2).


OK, so we fix n2 and assume A: Num (n + m) ↓ n2. We can prove n2 = n + m:


  -------------------- A   -----------------------  Big-step rules
    Num (n + m) ↓ n2         Num (n + m) ↓ n + m
  ------------------------------------------------   Lemma 3
                 n2 = n + m


Thus we can rewrite our goal to Plus (Num n) (Num m) ↓ n + m.

This we can prove from the big-step rules:


  -------------       -------------
    Num n ↓ n           Num m ↓ m
  ---------------------------------
     Plus (Num n) (Num m) ↓ n + m


That completes this case.



Let us examine one of the inductive cases, the case associated with the Let
contextual rule:

                 e1 |-> e1_2
-------------------------------------------  <- this rule
        (Let x e1 e2) |-> (Let x e1_2 e2)


We assume an inductive hypothesis:
IH: 
S(e1, e1_2) ≡ (∀n. e1 ↓ n ==> e1_2 ↓ n).


We must show S(Let x e1 e2, Let x e1_2 e2) ≡
(∀n. Let x e1 e2 ↓ n ==> Let x e1_2 e2 ↓ n).


OK, so we fix n, and can assume the local assumption A: Let x e1 e2 ↓ n.


Unfortunately we can't just use Lemma 3 here, as we don't know anything about
the evaluation of e2. We need to case-split on the proof of A. The only
big-step rule that can establish this judgement is the Let big-step rule. It
requires that e1 ↓ v (for some v), and that e2[x := Num v] ↓ n. So, we can
fix a new v, and assume A2: e1 ↓ v and A3: e2[x := Num v] ↓ n.


Now we can prove what we need:



    ------ A2
    e1 ↓ v
  -------- IH   ------------------ A3
  e1_2 ↓ v      e2[x := Num v] ↓ n
------------------------------------ Let big-step rule
         Let x e1_2 e2 ↓ n


The remaining "contextual" small-step cases have similar proofs. In each case
we have e |-> e', that some syntax S containing e evaluates (↓) to v, and want
to show that S' (S with e replaced by e') also evaluates to v. We also know
that e and e' evaluate to the same thing. What we need to do is case-split on the
derivation of S ↓ v, one part of which will be e ↓ v2, and use our IH to establish
e' ↓ v2, then put the parts of the big-step judgement back together to get S' ↓ v.