Refinement Proof

The M-machine can definitely do this:

Plus (Num v1) (Num v2) |->M Num (v1 + v2)



We want to show that steps like this can also be performed in context.

In particular, we need to do it in the kind of context that is created
by applying our abstraction function:

A (s ≻ Plus (Num v1) (Num v2) |->M A (s ≻ Num (v1 + v2))


We need to generalise this to:

∀e1 e2. e1 |-> e2 ==> A (s ≻ e1) |->M A (s ≻ e2)


To do the proof formally, we need to induct on the value
s, which we are treating as a list. Alternatively, we could
induct on the inference rules that construct the judgements
Stack and Frame in the slides.

Base case: s is empty, of the form ○.

This case is uninteresting, A (○ ≻ e) is just e, and
therefore what we have to show is exactly what we assumed.

Inductive case:

s is of the form f ▷ s'.

Assume the IH:
∀e1 e2. e1 |->M e2 ==> A (s' ≻ e1) |->M A (s' ≻ e2)

Show that 
∀e1 e2. e1 |->M e2 ==> A (f ▷ s' ≻ e1) |->M A (f ▷ s' ≻ e2)

So, fix e1 an e2 and assume e1 |->M e2.

Case split on f, on the different kinds of frame.

For instance:

f is of the form Plus □ e3.

Our goal was:
A (f ▷ s' ≻ e1) |->M A (f ▷ s' ≻ e2)
  = A (Plus □ e3 ▷ s' ≻ e1) |->M A (Plus □ e3 ▷ s' ≻ e2) 
  ≡ A (s' ≻ Plus e1 e3) |->M A s' ≻ Plus e2 e3)     (by definition of A)

To this goal, we apply our IH, and must show:

Plus e1 e3 |->M Plus e2 e3

This follows from the contextual rule for |->M,
and from our assumption e1 |->M e2.

Likewise for all the other cases for f.