POPL Tutorial/Big step, small step: Solution

This is the solution to this exercise. |hidden = true

%% Syntax %%
%sort tp %.
%name tp %.
%term nat tp %.
%term arr %pi tp %-> tp %-> tp %.
%sort exp %.
%name exp %.
%term fn %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%term z exp %.
%term s %pi exp %-> exp %.
%term ifz %pi exp %-> exp %-> (%pi exp %-> exp) %-> exp %.
%% Small-step dynamic semantics %%
%sort value {_ exp} %.
%name value %.
%mode value %in %.
%term value/z value z %.
%term value/s %pi (value (s E)) %<- (value E) %.
%term value/fn value (fn _ _) %.
%sort step {_ exp} {_ exp} %.
%name step %.
%mode step %in %out %.
%term step/app/fn %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step/app/arg %pi (step (app E1 E2) (app E1 E2')) %<- (value E1) %<- (step E2 E2') %.
%term step/app/beta %pi (step (app (fn _ ([x] E x)) E2) (E E2)) %<- (value E2) %.
%term step/s %pi (step (s E) (s E')) %<- (step E E') %.
%term step/ifz/arg %pi (step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))) %<- (step E E') %.
%term step/ifz/z step (ifz z E1 ([x] E2 x)) E1 %.
%term step/ifz/s %pi (step (ifz (s E) E1 ([x] E2 x)) (E2 E)) %<- (value E) %.
%%% Multi-step %%%
%sort step* {_ exp} {_ exp} %.
%name step* %.
%term step*/step %pi (step* E E') %<- (step E E') %.
%term step*/refl step* E E %.
%term step*/trans %pi (step* E E'') %<- (step* E' E'') %<- (step* E E') %.
%inline @ (%pi (step* E E') %-> (step* E' E'') %-> (step* E E'')) [d1] [d2] step*/trans d1 d2 %.
%prec %right 10 @ %.
%% Big-step dynamic semantics %%
%sort eval {_ exp} {_ exp} %.
%name eval %.
%term eval/z eval z z %.
%term eval/s %pi (eval (s E) (s V)) %<- (eval E V) %.
%term eval/ifz/z %pi (eval (ifz E E0 ([x] E1 x)) V0) %<- (eval E z) %<- (eval E0 V0) %.
%term eval/ifz/s %pi (eval (ifz E E0 ([x] E1 x)) V1) %<- (eval E (s V)) %<- (eval (E1 V) V1) %.
%term eval/fn eval (fn T1 ([x] E x)) (fn T1 ([x] E x)) %.
%term eval/app
  %pi (eval (app E1 E2) V)
  %<- (eval E1 (fn T1 ([x] E x)))
  %<- (eval E2 V2)
  %<- (eval (E V2) V) %.
%%% Lemmas about big-step dynamic semantics and values %%%
%sort eval-val {_ eval E V} {_ value V} %.
%mode eval-val %in %out %.
%term _ eval-val eval/z value/z %.
%term _ %pi (eval-val (eval/s D) (value/s Dval)) %<- (eval-val D Dval) %.
%term _
  %pi (eval-val (eval/ifz/z (%the (eval E0 V0) D0) (%the (eval E z) Dz)) Dval0)
  %<- (eval-val D0 (%the (value V0) Dval0)) %.
%term _
  %pi (eval-val (%the (eval (ifz E E0 ([x] E1 x)) V1) (eval/ifz/s (%the (eval (E1 V) V1) D1) (%the (eval E (s V)) Ds))) Dval1)
  %<- (eval-val D1 (%the (value V1) Dval1)) %.
%term _ eval-val eval/fn value/fn %.
%term _
  %pi (eval-val (eval/app (%the (eval (E V2) V) Dsub) (%the (eval E2 V2) D2) (%the (eval E1 (fn T1 ([x] E x))) D1)) DvalV)
  %<- (eval-val Dsub (%the (value V) DvalV)) %.
%worlds () (eval-val _ _) %.
%total D (eval-val D _) %.
%sort val-eval {_ value V} {_ eval V V} %.
%mode val-eval %in %out %.
%term _ val-eval value/z eval/z %.
%term _ %pi (val-eval (value/s Dval) (eval/s Dev)) %<- (val-eval Dval Dev) %.
%term _ val-eval value/fn eval/fn %.
%worlds () (val-eval _ _) %.
%total D (val-eval D _) %.

Big-step implies multi-step

Compatibility lemmas ===

%sort step*/s {_ step* E E'} {_ step* (s E) (s E')} %.
%mode step*/s %in %out %.
%term _ step*/s (step*/step (%the (step E E') D)) (step*/step (step/s D)) %.
%term _ step*/s (%the (step* E E) step*/refl) (%the (step* (s E) (s E)) step*/refl) %.
%term _
  %pi (step*/s (step*/trans (%the (step* E E') D*) (%the (step* E' E'') D*')) (step*/trans D*s D*'s))
  %<- (step*/s D* (%the (step* (s E) (s E')) D*s))
  %<- (step*/s D*' (%the (step* (s E') (s E'')) D*'s)) %.
%worlds () (step*/s _ _) %.
%total D (step*/s D _) %.
%sort step*/ifz/arg {_ step* E E'} {_ step* (ifz E E0 ([x] E1 x)) (ifz E' E0 ([x] E1 x))} %.
%mode {%in E exp} {%in E' exp} {%in E0 exp} {%in E1 %pi exp %-> exp} {%in D step* E E'} {%out Difz step* (ifz E E0 ([x exp] E1 x)) (ifz E' E0 ([x exp] E1 x))} step*/ifz/arg D Difz %.
%term _ step*/ifz/arg (step*/step (%the (step E E') D)) (step*/step (step/ifz/arg D)) %.
%term _ step*/ifz/arg step*/refl step*/refl %.
%term _
  %pi (step*/ifz/arg (step*/trans D* D*') (step*/trans D*ifz D*'ifz))
  %<- (step*/ifz/arg D* D*ifz)
  %<- (step*/ifz/arg D*' D*'ifz) %.
%worlds () (step*/ifz/arg _ _) %.
%total D (step*/ifz/arg D _) %.
%sort step*/app/fn {_ step* E1 E1'} {_ step* (app E1 E2) (app E1' E2)} %.
%mode {%in E1 exp} {%in E1' exp} {%in E2 exp} {%in D1 step* E1 E1'} {%out Dapp step* (app E1 E2) (app E1' E2)} step*/app/fn D1 Dapp %.
%term _ step*/app/fn (step*/step (%the (step E1 E1') D1)) (step*/step (step/app/fn D1)) %.
%term _ step*/app/fn step*/refl step*/refl %.
%term _
  %pi (step*/app/fn (step*/trans D* D*') (step*/trans D*app D*'app))
  %<- (step*/app/fn D* D*app)
  %<- (step*/app/fn D*' D*'app) %.
%worlds () (step*/app/fn _ _) %.
%total D (step*/app/fn D _) %.

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

%sort step*/app/arg {_ step* E2 E2'} {_ value V1} {_ step* (app V1 E2) (app V1 E2')} %.
%mode step*/app/arg %in %in %out %.
%term _ step*/app/arg (step*/step (%the (step E2 E2') D2)) (%the (value V1) DvalV1) (step*/step (step/app/arg D2 DvalV1)) %.
%term _ step*/app/arg step*/refl _ step*/refl %.
%term _
  %pi (step*/app/arg (step*/trans D* D*') (%the (value V1) DvalV1) (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

%sort eval-multi {_ eval E V} {_ step* E V} %.
%mode eval-multi %in %out %.
%term _ eval-multi (%the (eval z z) eval/z) step*/refl %.
%term _
  %pi (eval-multi (%the (eval (s E) (s V)) (eval/s D)) D*s)
  %<- (eval-multi D (%the (step* E V) D*))
  %<- (step*/s D* (%the (step* (s E) (s V)) D*s)) %.
%term _
  %pi (eval-multi (eval/ifz/z (%the (eval E0 V0) D0) (%the (eval E z) Dz)) (Difz* @ step*/step step/ifz/z @ D0*))
  %<- (eval-multi Dz (%the (step* E z) Dz*))
  %<- (eval-multi D0 (%the (step* E0 V0) D0*))
  %<- (step*/ifz/arg Dz* (%the (step* (ifz E E0 ([x] E1 x)) (ifz z E0 ([x] E1 x))) Difz*)) %.
%term _
  %pi (eval-multi (eval/ifz/s (%the (eval (E1 V) V1) D1) (%the (eval E (s V)) Ds)) (Difz* @ step*/step (step/ifz/s DvalV) @ D1*))
  %<- (eval-multi Ds (%the (step* E (s V)) Ds*))
  %<- (eval-multi D1 (%the (step* (E1 V) V1) D1*))
  %<- (step*/ifz/arg Ds* (%the (step* (ifz E E0 ([x] E1 x)) (ifz (s V) E0 ([x] E1 x))) Difz*))
  %<- (eval-val Ds (value/s (%the (value V) DvalV))) %.

…snip…

%term _ eval-multi eval/fn step*/refl %.
%term _
  %pi (eval-multi (eval/app (%the (eval (E V2) V) Dsub) (%the (eval E2 V2) D2) (%the (eval E1 (fn T1 ([x] E x))) D1)) (Dfun* @ Darg* @ step*/step (step/app/beta DvalV2) @ Dsub*))
  %<- (eval-multi D1 (%the (step* E1 (fn T1 ([x] E x))) D1*))
  %<- (eval-multi D2 (%the (step* E2 V2) D2*))
  %<- (eval-multi Dsub (%the (step* (E V2) V) Dsub*))
  %<- (step*/app/fn D1* (%the (step* (app E1 E2) (app (fn T1 ([x] E x)) E2)) Dfun*))
  %<- (step*/app/arg D2* value/fn (%the (step* (app (fn T1 ([x] E x)) E2) (app (fn T1 ([x] E x)) V2)) Darg*))
  %<- (eval-val D2 DvalV2) %.
%worlds () (eval-multi _ _) %.
%total D (eval-multi D _) %.

Multi-step implies big step ==

%sort step** {_ exp} {_ exp} %.
%name step** %.
%term step**/refl step** E E %.
%term step**/cons %pi (step** E E'') %<- (step** E' E'') %<- (step E E') %.
%sort step**/trans {_ step** E E'} {_ step** E' E''} {_ step** E E''} %.
%mode step**/trans %in %in %out %.
%term _ step**/trans step**/refl (%the (step** E E'') Dstep**) Dstep** %.
%term _
  %pi (step**/trans (step**/cons (%the (step E E1) Dstep1) (%the (step** E1 E') Dstep**1)) (%the (step** E' E'') Dstep**2) (step**/cons Dstep1 Dstep**))
  %<- (step**/trans Dstep**1 Dstep**2 (%the (step** E1 E'') Dstep**)) %.
%worlds () (step**/trans _ _ _) %.
%total D (step**/trans D _ _) %.
%sort multi-step** {_ step* E E'} {_ step** E E'} %.
%mode multi-step** %in %out %.
%term _ multi-step** (step*/step Dstep) (step**/cons Dstep step**/refl) %.
%term _ multi-step** step*/refl step**/refl %.
%term _
  %pi (multi-step** (step*/trans (%the (step* E E') D1) (%the (step* E' E'') D2)) D**)
  %<- (multi-step** D1 (%the (step** E E') D1**))
  %<- (multi-step** D2 (%the (step** E' E'') D2**))
  %<- (step**/trans D1** D2** (%the (step** E E'') D**)) %.
%worlds () (multi-step** _ _) %.
%total D (multi-step** D _) %.

Expansion lemma

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

%sort expansion {_ eval E' V} {_ step E E'} {_ eval E V} %.
%mode expansion %in %in %out %.
%term _
  %pi (expansion (%the (eval (s E') (s V)) (eval/s (%the (eval E' V) Deval'))) (%the (step (s E) (s E')) (step/s (%the (step E E') Dstep))) (%the (eval (s E) (s V)) (eval/s (%the (eval E V) Deval))))
  %<- (expansion Deval' Dstep (%the (eval E V) Deval)) %.
%term _
  %pi (expansion (%the (eval (ifz E' E0 ([x] E1 x)) V0) (eval/ifz/z (%the (eval E0 V0) D0) (%the (eval E' z) Dz'))) (%the (step (ifz E E0 ([x] E1 x)) (ifz E' E0 ([x] E1 x))) (step/ifz/arg (%the (step E E') Dstep))) (%the (eval (ifz E E0 ([x] E1 x)) V0) (eval/ifz/z D0 Dz)))
  %<- (expansion Dz' Dstep (%the (eval E z) Dz)) %.

…snip…

%term _
  %pi (expansion (%the (eval (ifz E' E0 ([x] E1 x)) V1) (eval/ifz/s (%the (eval (E1 V) V1) D1) (%the (eval E' (s V)) Ds'))) (%the (step (ifz E E0 ([x] E1 x)) (ifz E' E0 ([x] E1 x))) (step/ifz/arg (%the (step E E') Dstep))) (%the (eval (ifz E E0 ([x] E1 x)) V1) (eval/ifz/s D1 Ds)))
  %<- (expansion Ds' Dstep (%the (eval E (s V)) Ds)) %.
%term _ expansion (%the (eval E0 V0) Deval') (%the (step (ifz z E0 ([x] E1 x)) E0) step/ifz/z) (eval/ifz/z Deval' eval/z) %.
%term _
  %pi (expansion (%the (eval (E1 V) V1) Deval') (%the (step (ifz (s V) E0 ([x] E1 x)) (E1 V)) (step/ifz/s (%the (value V) Dval))) (eval/ifz/s Deval' (eval/s DevalV)))
  %<- (val-eval Dval (%the (eval V V) DevalV)) %.
%term _
  %pi (expansion (%the (eval (E1 V) V1) Deval') (%the (step (ifz (s V) E0 ([x] E1 x)) (E1 V)) (step/ifz/s (%the (value V) Dval))) (eval/ifz/s Deval' (eval/s DevalV)))
  %<- (val-eval Dval (%the (eval V V) DevalV)) %.
%term _
  %pi (expansion (%the (eval (app E1' E2) V) (eval/app (%the (eval (E V2) V) Dsub) (%the (eval E2 V2) D2) (%the (eval E1' (fn T1 ([x] E x))) D1'))) (%the (step (app E1 E2) (app E1' E2)) (step/app/fn (%the (step E1 E1') Dstep1))) (eval/app Dsub D2 D1))
  %<- (expansion D1' Dstep1 (%the (eval E1 (fn T1 ([x] E x))) D1)) %.

…snip…

%term _
  %pi (expansion (%the (eval (app V1 E2') V) (eval/app (%the (eval (E V2) V) Dsub) (%the (eval E2' V2) D2') (%the (eval V1 (fn T1 ([x] E x))) D1))) (%the (step (app V1 E2) (app V1 E2')) (step/app/arg (%the (step E2 E2') Dstep2) (%the (value V1) Dval1))) (eval/app Dsub D2 D1))
  %<- (expansion D2' Dstep2 (%the (eval E2 V2) D2)) %.
%term _
  %pi (expansion (%the (eval (E V2) V) Deval') (%the (step (app (fn T1 ([x] E x)) V2) (E V2)) (step/app/beta (%the (value V2) Dval2))) (eval/app Deval' DevalV2 eval/fn))
  %<- (val-eval Dval2 (%the (eval V2 V2) DevalV2)) %.
%worlds () (expansion _ _ _) %.
%total D (expansion _ D _) %.

Main theorem

TASK 4: Prove main theorem in the forward direction

%sort multi**-eval {_ step** E V} {_ value V} {_ eval E V} %.
%mode multi**-eval %in %in %out %.
%term _
  %pi (multi**-eval step**/refl (%the (value V) Dval) Deval)
  %<- (val-eval Dval (%the (eval V V) Deval)) %.
%term _
  %pi (multi**-eval (step**/cons (%the (step E E') Dstep) (%the (step** E' V) Dstep**)) (%the (value V) Dval) Deval)
  %<- (multi**-eval Dstep** Dval (%the (eval E' V) Deval'))
  %<- (expansion Deval' Dstep (%the (eval E V) Deval)) %.
%worlds () (multi**-eval _ _ _) %.
%total D (multi**-eval D _ _) %.

TASK 5: Complete proof by composing previous lemmas

%sort multi-eval {_ step* E V} {_ value V} {_ eval E V} %.
%mode multi-eval %in %in %out %.
%term _
  %pi (multi-eval (%the (step* E V) D*) (%the (value V) Dval) Dev)
  %<- (multi-step** D* (%the (step** E V) D**))
  %<- (multi**-eval D** Dval (%the (eval E V) Dev)) %.
%worlds () (multi-eval _ _ _) %.
%total {} (multi-eval _ _ _) %.