POPL Tutorial/Big step, small step: Solution

From The Twelf Project

This is the solution to this exercise.

Contents 1 Big-step implies multi-step 1.1 Compatibility lemmas 1.1.1 TASK 1: Fill in the cases of the unfinished compatibility proof 1.2 Main theorem 1.2.1 TASK 2: Fill in the missing cases of the theorem 2 Multi-step implies big step 2.1 Expansion lemma 2.1.1 TASK 3: Prove the three missing cases of the expansion lemma 2.2 Main theorem 2.2.1 TASK 4: Prove main theorem in the forward direction 2.2.2 TASK 5: Complete proof by composing previous lemmas

Big-step implies multi-step

Compatibility lemmas

TASK 1: Fill in the cases of the unfinished compatibility proof

step*/app/arg : step* E2 E2' -> value V1 -> step* (app V1 E2) (app V1 E2')
                 -> type.
%mode step*/app/arg +D2 +DvalV1 -Dapp.

- : step*/app/arg (step*/step (D2 : step E2 E2'))
                  (DvalV1 : value V1)
                  (step*/step (step/app/arg D2 DvalV1)).
- : step*/app/arg step*/refl _ step*/refl.
- : step*/app/arg (step*/trans D* D*')
                  (DvalV1 : value V1)
                  (step*/trans D*app D*'app)
     <- step*/app/arg D* DvalV1 D*app
     <- step*/app/arg D*' DvalV1 D*'app.

%worlds () (step*/app/arg _ _ _).
%total D (step*/app/arg D _ _).

Main theorem

TASK 2: Fill in the missing cases of the theorem

eval-multi : eval E V -> step* E V -> type.
%mode eval-multi +D -D*.

...snip...

- : eval-multi 
     eval/fn 
     step*/refl.

- : eval-multi 
     (eval/app (Dsub : eval (E V2) V)
        (D2 : eval E2 V2)
        (D1 : eval E1 (fn T1 ([x] E x))))
        (Dfun* @ Darg* @ step*/step (step/app/beta DvalV2) @ Dsub*)
     <- eval-multi D1 (D1* : step* E1 (fn T1 ([x] E x)))
     <- eval-multi D2 (D2* : step* E2 V2)
     <- eval-multi Dsub (Dsub* : step* (E V2) V)
     <- step*/app/fn D1* (Dfun* : step* (app E1 E2)
                                         (app (fn T1 ([x] E x)) E2))
     <- step*/app/arg D2* value/fn
                          (Darg* : step* (app (fn T1 ([x] E x)) E2)
                                         (app (fn T1 ([x] E x)) V2))
     <- eval-val D2 DvalV2.

%worlds () (eval-multi _ _). 
%total D (eval-multi D _).

Multi-step implies big step

Expansion lemma

TASK 3: Prove the three missing cases of the expansion lemma

expansion : eval E' V -> step E E' -> eval E V -> type.
%mode expansion +D1 +D2 -D3.

...snip...

- : expansion
     (eval/ifz/s (D1 : eval (E1 V) V1) (Ds' : eval E' (s V))
        : eval (ifz E' E0 [x] E1 x) V1)
     (step/ifz/arg (Dstep : step E E')
        : step (ifz E E0 [x] E1 x) (ifz E' E0 [x] E1 x))
     (eval/ifz/s D1 Ds
        : eval (ifz E E0 [x] E1 x) V1)
     <- expansion Ds' Dstep (Ds : eval E (s V)).

...snip...

- : expansion 
     (eval/app (Dsub : eval (E V2) V)
        (D2' : eval E2' V2)
        (D1 : eval V1 (fn T1 ([x] E x)))
        : eval (app V1 E2') V)
     (step/app/arg (Dstep2 : step E2 E2') (Dval1 : value V1)
        : step (app V1 E2) (app V1 E2'))
     (eval/app Dsub D2 D1)
     <- expansion D2' Dstep2 (D2 : eval E2 V2).

- : expansion 
     (Deval' : eval (E V2) V)
     (step/app/beta (Dval2 : value V2)
        : step (app (fn T1 ([x] E x)) V2) (E V2))
     (eval/app Deval' DevalV2 eval/fn)
     <- val-eval Dval2 (DevalV2 : eval V2 V2).

%worlds () (expansion _ _ _).
%total D (expansion _ D _).

Main theorem

TASK 4: Prove main theorem in the forward direction

multi**-eval : step** E V -> value V -> eval E V -> type.
%mode multi**-eval +D1 +D2 -D3.

- : multi**-eval step**/refl (Dval : value V) Deval
     <- val-eval Dval (Deval : eval V V).

- : multi**-eval (step**/cons (Dstep : step E E') (Dstep** : step** E' V))
                 (Dval : value V)
                 Deval
     <- multi**-eval Dstep** Dval (Deval' : eval E' V)
     <- expansion Deval' Dstep (Deval : eval E V).

%worlds () (multi**-eval _ _ _).
%total D (multi**-eval D _ _).

TASK 5: Complete proof by composing previous lemmas

multi-eval : step* E V -> value V -> eval E V -> type.
%mode multi-eval +D1 +D2 -D3.

- : multi-eval (D* : step* E V) (Dval : value V) Dev
     <- multi-step** D* (D** : step** E V)
     <- multi**-eval D** Dval (Dev : eval E V).

%worlds () (multi-eval _ _ _).
%total {} (multi-eval _ _ _).