Lambda Calculus
Subject Reduction for the simply typed lambda-calculus
Parts of this example were completed as part of Daniel Luick's honors thesis [1].
Generalized
ty : type.
top : ty.
arr : {Z1:ty} {Z2:ty} ty.
tm : type.
app : {Y1:tm} {Y2:tm} tm.
lam : {Z:ty} {Y:{x:tm}tm} tm.
of : tm -> ty -> type.
of_app : {M:tm}{N:tm}{T:ty}{U:ty}
{a1:of M (arr U T)} {a2:of N U} of (app M N) T.
of_lam : {R : {x:tm} tm}{T:ty}{U:ty}
{a1:({x:tm}{z:of x T} of (R x) U)}
of (lam T ([x] R x)) (arr T U).
step : tm -> tm -> type.
step-app1 : {M1:tm} {M2:tm} {N:tm} {D : step M1 M2}
step (app M1 N) (app M2 N).
step-app2 : {M:tm} {N1:tm} {N2:tm} {D : step N1 N2}
step (app M N1) (app M N2).
step-beta : {T:ty} {R:{x:tm}tm} {N:tm}
step (app (lam T ([x] R x)) N) (R N).
step-lam : {T:ty} {R1:{x:tm}tm} {R2:{x:tm}tm}
{D : {x:tm} {d:of x T} step (R1 x) (R2 x)}
step (lam T ([x] R1 x)) (lam T ([x] R2 x)).Specification "generalized.lf".
Schema c :=
{T}(x:tm,y:of x T).
Theorem subject_reduction : ctx Gamma:c, forall M1 M2 T D1 D2,
{Gamma |- D1 : step M1 M2} => {Gamma |- D2 : of M1 T} => exists D3,
{Gamma |- D3 : of M2 T}.
induction on 1. intros. case H1.
% step-lam case
case H2.
apply IH to H6 H10 with (Gamma = Gamma, n1:tm, n:of n1 T1).
prune H11.
exists of_lam ([x] R2 x) T1 T2 ([x] [x1] D1 x x1).
search.
% step-beta case
case H2.
case H10.
inst H15 with n2 = N.
inst H16 with n3 = D5.
exists D6 N D5.
search.
% step-app2 case
case H2.
apply IH to H6 H12.
exists of_app M N2 T U a1 D3.
search.
% step-app1 case
case H2.
apply IH to H6 H11.
exists of_app M4 N T U D3 a2.
search.Large & Small Step
ty : type.
arr : ty -> ty -> ty.
tm : type.
app : tm -> tm -> tm.
lam : ty -> (tm -> tm) -> tm.
of : tm -> ty -> type.
of_app : {M:tm}{N:tm}{T:ty}{U:ty}
{a1:of M (arr U T)} {a2:of N U} of (app M N) T.
of_lam : {R : {x:tm} tm}{T:ty}{U:ty}
{a1:({x:tm}{z:of x T} of (R x) U)}
of (lam T ([x] R x)) (arr T U).
eq : ty -> ty -> type.
refl : {T:ty} eq T T.
% weak small step call by value reduction
sscbv : tm -> tm -> type.
sscbv_app1 : {M1:tm} {M2:tm} {N:tm} {D1 : sscbv M1 M2}
sscbv (app M1 N) (app M2 N).
sscbv_app2 : {R:{x:tm}tm}{T:ty}{M1:tm}{M2:tm}{D1 : sscbv M1 M2}
sscbv (app (lam T ([x] R x)) M1) (app (lam T ([x] R x)) M2).
sscbv_beta : {R1 : {x:tm} tm}{R2 : {x:tm} tm}{T1:ty}{T2:ty}
sscbv (app (lam T1 ([x] R1 x)) (lam T2 ([x] R2 x))) (R1 (lam T2 ([x] R2 x))).
% weak large step call by name reduction
lscbn : tm -> tm -> type.
lscbn_abs : {R:{x:tm} tm} {T:ty} lscbn (lam T ([x] R x)) (lam T ([x] R x)).
lscbn_beta : {M:tm} {N:tm} {V:tm} {R:{x:tm}tm} {T:ty}
{D1 : lscbn M (lam T ([x] R x))}
{D2 : lscbn (R N) V}
lscbn (app M N) V.Specification "reduce.lf".
Schema c :=
{T}(x:tm,y:of x T).
% Subject reduction for weak large step call by name reduction.
Theorem subject_reduction_lscbn : ctx Gamma:c, forall M1 M2 T D1 D2,
{Gamma |- D1 : of M1 T} => {D2 : lscbn M1 M2} =>
exists D3, {Gamma |- D3 : of M2 T}.
induction on 2. intros. case H2.
% beta reduction case.
case H1.
apply IH to H14 H8.
case H16.
inst H20 with n2 = N.
inst H21 with n3 = D7.
apply IH to H22 H9.
exists (D1 n3 n2 n1 n).
search.
% abs reduction case.
exists D1.
search.Specification "reduce.lf".
Schema c :=
{T}(x:tm,y:of x T).
% Subject reduction for weak small step call by value reduction.
Theorem subject_reduction_wsscbv : ctx Gamma:c, forall M1 M2 T D1 D2,
{Gamma |- D1 : of M1 T} => {D2 : sscbv M1 M2} =>
exists D3, {Gamma |- D3 : of M2 T}.
induction on 2. intros. case H2.
% beta case.
case H1.
case H11.
inst H16 with n3 = (lam T2 ([x] R2 x)).
inst H17 with n4 = D5.
exists D6 (lam T2 ([x] R2 x)) D5.
search.
% app2 case.
case H1.
apply IH to H13 H7.
prune H14.
exists of_app (lam T1 ([x] R x)) M4 T D4 D5 (D1 n).
assert {Gamma |- M4 : tm}. search.
% app1 case.
case H1.
apply IH to H11 H6.
exists of_app M4 N T U D1 a2.
assert {Gamma |- M4 : tm}. search.References
- [1] Luick, D.: Using the Adelfa Proof Assistant to Construct Proofs of Programming Language Properties, https://hdl.handle.net/11299/220294, (2021).