Walkthrough

Introduction

Adelfa is a proof assistant that reasons about LF specifications. Proof developments are parameterized by an LF signature which often encodes the object system to be reasoned about. LF is a popular choice for encoding systems, as it can more easily represent objects with binding operations via higher-order abstract syntax.

In this example, we will reason about the $\lambda$ -calculus with big step (sometimes referred to as “call-by name”) evaluation semantics. We denote this as a relation between two terms $e_1 \Downarrow e_2$ . The “input” term is on the left of the $\Downarrow$ and the result of the evaluation is the term on the right.

{{}\over{}(\lambda x. e) \Downarrow (\lambda x. e)}{\mathtt{eval\textrm{-}abs}} \qquad\qquad {{ e_1 \Downarrow (\lambda x. e') \qquad \{e_2/x\}e' \Downarrow e } \over{}{(e_1\ e_2) \Downarrow e}}{\mathtt{eval\textrm{-}app}}

$\mathtt{eval\textrm{-}abs}$ states that an abstraction is already evaluated, i.e., it evaluates to itself.
$\mathtt{eval\textrm{-}app}$ evaluates the first term of the application, which result in an abstraction to permit the application. Then the second term is substituted for the variable bound in said abstraction.

In addition to an evaluation semantics, we encode typing of the lambda calculus.

{ {\Gamma \vdash e_1 {:} (\tau \to \sigma) \qquad \Gamma \vdash e_2 {:} \tau} \over {\Gamma \vdash (e_1\ e_2) {:} \sigma} }\mathtt{of\textrm{-}app} \qquad\quad { {\Gamma, x{:}\tau \vdash e{:}\sigma} \over {\Gamma \vdash (\lambda x. e){:}(\tau \to \sigma)} }{\mathtt{of\textrm{-}abs} \atop {x \not\in \Gamma}} \qquad\quad { {x{:}\tau \in \Gamma} \over {\Gamma \vdash x {:} \tau} }\mathtt{of\textrm{-}var}

$\mathrm{of\textrm{-}app}$ rule ensures that the first term is an abstraction, which would permit the substitution of $e_2$ for the variable.
$\mathrm{of\textrm{-}abs}$ says that the abstraction is typed under extended context with $x{:}\tau$ present. The additional proviso ensures that $x$ does not already appear in $\Gamma$ and shadow its entry.
$\mathrm{of\textrm{-}var}$ ensures that when we encounter a variable, its must have an entry in the context which assigns it that type.

We now discuss showing that evaluation of terms does not change the type, called subject reduction or type preservation. The informal proof is phrased as:

For any $\lambda$ -calculus terms $e$ and $e'$ such that $e \Downarrow e'$ and $\Gamma \vdash e{:}\tau$ hold, then $\Gamma \vdash e'{:}\tau$ must hold.

We will now work through how we can specify these rules in LF, then use Adelfa to reason about this specification. You can follow along using the specification file stlc.lf and theorem development stlc.ath.

Canonical LF Specification

Firstly, the syntactic categories of our system are encoded as LF types. Formations of these syntactic categories are encoded as term constructors of the relevant type.

stlc.lf


ty : type.
arr : {T:ty}{U:ty} ty.
 
tm : type.
app : {E1:tm}{E2:tm} tm.
abs : {R:{x:tm}tm} tm.

Now we will encode the evaluation and typing judgements for the system. This is done by creating an LF type indexed by the relevant types for each judgement. For example, the evaluation rules relate two terms. Therefore, it we introduce a new type eval which is indexed by two tms.

Typing in our specification slightly differs from typing in our informal rules. Although this relation had to maintain an explicit context to support the $\mathtt{of\textrm{-}abs}$ and $\mathtt{of\textrm{-}var}$ rules, we will encode the typing rules using the higher-order abstract syntax approach. The of_abs rule is indexed by a judgement {a1:({x:tm}{z:of x T}) of (R x) U}. This judgement analyzes the type of R when x is of type T. The type of a1 is informed by the informal rule for typing.

stlc.lf


of : {E:tm}{T: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_abs : {R : {x:tm} tm}{T:ty}{U:ty}
         {a1:({x:tm}{z:of x T} of (R x) U)}
         of (abs ([x] R x)) (arr T U).
 
eval : {E1:tm}{E2:tm}type.
eval_abs : {R: {x:tm} tm}
           eval (abs ([x] R x)) (abs ([x] R x)).
eval_app : {M:tm}{N:tm}{V:tm}{R:{x:tm} tm}
           {a1:eval M (abs ([x] R x))}{a2:eval (R N) V}
           eval (app M N) V.

We have finished our encoding of the object system, and can now being to reason about it using Adelfa.

Saving the above signature in a file stlc.lf we load it into Adelfa using the following command.

Reasoning

We will step through the proof of subject reduction using the Adelfa CLI. You may choose to follow along in this way or use tools such as Proof General to help maintain a proof file. If you choose to do the latter, you may want to copy the entire development from here then follow along in the editor of your choice.

We begin by loading the LF signature we defined into the proof development.


>> Specification "stlc.lf".

We can state subject reduction in Adelfa with:


>> Theorem sr_eval : forall E V T D1 D2,
  {D1 : eval E V} => {D2 : of E T} => exists D, {D : of V T}.
 
Subgoal sr_eval:
 
==================================
forall E, forall V, forall T, forall D1, forall D2,
  {D1 : eval E V} => {D2 : of E T} => exists D, {D : of V T}

The formula states that whenever there exist inhabitants D1 and D2 of types eval E V and of E T respectively, then there must exist an inhabitant, D, exhibiting that V is also of type T.

We will prove this theorem by induction on the height of the derivation that E evaluates to V.


sr_eval >> induction on 1.
 
Subgoal sr_eval:
 
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
 
==================================
forall E, forall V, forall T, forall D1, forall D2,
  {D1 : eval E V}@ => {D2 : of E T} => exists D, {D : of V T}

The next step is to introduce eigenvariables and context variables for any quantifiers and introduce the implications in the goal as hypotheses.


sr_eval >> intros.
 
Subgoal sr_eval:
 
Vars: D2:o, D1:o, T:o, V:o, E:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H1:{D1 : eval E V}@
H2:{D2 : of E T}
 
==================================
exists D, {D : of V T}

Now we perform case analysis on {D1 : eval E V}@ using the case tactic. This will split the proof into two branches based on the two possible ways in which E can evaluate to V. Each of the different proof branches is called a subgoal. In general, only the first subgoal will be displayed in full; the other subgoals will be shown without their hypotheses. When the first subgoal is completed, the prover will move to the next subgoal.


sr_eval >> case H1.
 
Subgoal sr_eval.1:
 
Vars: R:(o) -> o, T1:o, a1:o, a2:o, M:o, N:o, D2:o, T:o, V:o
Nominals: n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H2:{D2 : of (app M N) T}
H3:{M : tm}*
H4:{N : tm}*
H5:{V : tm}*
H6:{n:tm |- R n : tm}*
H7:{T1 : ty}*
H8:{a1 : eval M (abs T1 ([x]R x))}*
H9:{a2 : eval (R N) V}*
 
==================================
exists D, {D : of V T}
 
Subgoal sr_eval.2 is:
 exists D, {D : of (abs T1 ([x]R x)) T}

We now perform case analysis on the second hypothesis, {D2 : of (app M N) T}, to obtain derivations for the typing of both subterms M and N.


sr_eval.1>> case H2.
 
Subgoal sr_eval.1:
 
Vars: D3:o, D4:o, D5:o, R:(o) -> o, T1:o, a1:o, a2:o, M:o, N:o, T:o, V:o
Nominals: n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H3:{M : tm}*
H4:{N : tm}*
H5:{V : tm}*
H6:{n:tm |- R n : tm}*
H7:{T1 : ty}*
H8:{a1 : eval M (abs T1 ([x]R x))}*
H9:{a2 : eval (R N) V}*
H10:{M : tm}
H11:{N : tm}
H12:{T : ty}
H13:{D3 : ty}
H14:{D4 : of M (arr D3 T)}
H15:{D5 : of N D3}
 
==================================
exists D, {D : of V T}
 
Subgoal sr_eval.2 is:
 exists D, {D : of (abs T1 ([x]R x)) T}

We are now able to apply the inductive hypothesis with the assumptions H8 and H14.


sr_eval.1>> apply IH to H8 H14.
 
Subgoal sr_eval.1:
 
Vars: D:(o) -> o, D3:o, D4:o, D5:o, R:(o) -> o, T1:o, a1:o, a2:o, M:o, N:o, T
        :o, V:o
Nominals: n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H3:{M : tm}*
H4:{N : tm}*
H5:{V : tm}*
H6:{n:tm |- R n : tm}*
H7:{T1 : ty}*
H8:{a1 : eval M (abs T1 ([x]R x))}*
H9:{a2 : eval (R N) V}*
H10:{M : tm}
H11:{N : tm}
H12:{T : ty}
H13:{D3 : ty}
H14:{D4 : of M (arr D3 T)}
H15:{D5 : of N D3}
H16:{D n : of (abs T1 ([x]R x)) (arr D3 T)}
 
==================================
exists D, {D : of V T}
 
Subgoal sr_eval.2 is:
 exists D, {D : of (abs T1 ([x]R x)) T}

We can now analyze the new assumption to obtain a typing judgement for R.


sr_eval.1>> case H16.
 
Subgoal sr_eval.1:
 
Vars: a3:(o) -> (o) -> (o) -> o, D3:o, D4:o, D5:o, R:(o) -> o, a1:o, a2:o, M:
        o, N:o, T:o, V:o
Nominals: n3:o, n2:o, n1:o, n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H3:{M : tm}*
H4:{N : tm}*
H5:{V : tm}*
H6:{n:tm |- R n : tm}*
H7:{D3 : ty}*
H8:{a1 : eval M (abs D3 ([x]R x))}*
H9:{a2 : eval (R N) V}*
H10:{M : tm}
H11:{N : tm}
H12:{T : ty}
H13:{D3 : ty}
H14:{D4 : of M (arr D3 T)}
H15:{D5 : of N D3}
H17:{n1:tm |- R n1 : tm}
H18:{D3 : ty}
H19:{T : ty}
H20:{n2:tm, n3:of n2 D3 |- a3 n n2 n3 : of (R n2) T}
 
==================================
exists D, {D : of V T}
 
Subgoal sr_eval.2 is:
 exists D, {D : of (abs T1 ([x]R x)) T}

The nominal constants in the hypothesis H20 are placeholders, and so can be instantiated by any particular terms of the appropriate type. In this instance, we want to replace n2 with N and n3 with D5.


sr_eval.1>> inst H20 with n2 = N.
 
Subgoal sr_eval.1:
 
Vars: a3:(o) -> (o) -> (o) -> o, D3:o, D4:o, D5:o, R:(o) -> o, a1:o, a2:o, M:
        o, N:o, T:o, V:o
Nominals: n3:o, n2:o, n1:o, n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H3:{M : tm}*
H4:{N : tm}*
H5:{V : tm}*
H6:{n:tm |- R n : tm}*
H7:{D3 : ty}*
H8:{a1 : eval M (abs D3 ([x]R x))}*
H9:{a2 : eval (R N) V}*
H10:{M : tm}
H11:{N : tm}
H12:{T : ty}
H13:{D3 : ty}
H14:{D4 : of M (arr D3 T)}
H15:{D5 : of N D3}
H17:{n1:tm |- R n1 : tm}
H18:{D3 : ty}
H19:{T : ty}
H20:{n2:tm, n3:of n2 D3 |- a3 n n2 n3 : of (R n2) T}
H21:{n3:of N D3 |- a3 n N n3 : of (R N) T}
 
==================================
exists D, {D : of V T}
 
Subgoal sr_eval.2 is:
 exists D, {D : of (abs T1 ([x]R x)) T}


sr_eval.1>> inst H21 with n3 = D5.
 
Subgoal sr_eval.1:
 
Vars: a3:(o) -> (o) -> (o) -> o, D3:o, D4:o, D5:o, R:(o) -> o, a1:o, a2:o, M:
        o, N:o, T:o, V:o
Nominals: n3:o, n2:o, n1:o, n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H3:{M : tm}*
H4:{N : tm}*
H5:{V : tm}*
H6:{n:tm |- R n : tm}*
H7:{D3 : ty}*
H8:{a1 : eval M (abs D3 ([x]R x))}*
H9:{a2 : eval (R N) V}*
H10:{M : tm}
H11:{N : tm}
H12:{T : ty}
H13:{D3 : ty}
H14:{D4 : of M (arr D3 T)}
H15:{D5 : of N D3}
H17:{n1:tm |- R n1 : tm}
H18:{D3 : ty}
H19:{T : ty}
H20:{n2:tm, n3:of n2 D3 |- a3 n n2 n3 : of (R n2) T}
H21:{n3:of N D3 |- a3 n N n3 : of (R N) T}
H22:{a3 n N D5 : of (R N) T}
 
==================================
exists D, {D : of V T}
 
Subgoal sr_eval.2 is:
 exists D, {D : of (abs T1 ([x]R x)) T}

We are now able to apply the inductive hypothesis with (R N) to obtain a typing derivation for V.


sr_eval.1>> apply IH to H9 H22.
 
Subgoal sr_eval.1:
 
Vars: a3:(o) -> (o) -> (o) -> o, D:(o) -> (o) -> (o) -> (o) -> o, D3:o, D4:o,
        D5:o, R:(o) -> o, a1:o, a2:o, M:o, N:o, T:o, V:o
Nominals: n3:o, n2:o, n1:o, n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H3:{M : tm}*
H4:{N : tm}*
H5:{V : tm}*
H6:{n:tm |- R n : tm}*
H7:{D3 : ty}*
H8:{a1 : eval M (abs D3 ([x]R x))}*
H9:{a2 : eval (R N) V}*
H10:{M : tm}
H11:{N : tm}
H12:{T : ty}
H13:{D3 : ty}
H14:{D4 : of M (arr D3 T)}
H15:{D5 : of N D3}
H17:{n1:tm |- R n1 : tm}
H18:{D3 : ty}
H19:{T : ty}
H20:{n2:tm, n3:of n2 D3 |- a3 n n2 n3 : of (R n2) T}
H21:{n3:of N D3 |- a3 n N n3 : of (R N) T}
H22:{a3 n N D5 : of (R N) T}
H23:{D n3 n2 n1 n : of V T}
 
==================================
exists D, {D : of V T}
 
Subgoal sr_eval.2 is:
 exists D, {D : of (abs T1 ([x]R x)) T}

We now instantiate D in the goal formula with the term (D n3 n2 n1 n) for which we now have an appropriate typing derivation in the premises.


sr_eval.1>> exists (D n3 n2 n1 n).
 
Subgoal sr_eval.1:
 
Vars: a3:(o) -> (o) -> (o) -> o, D:(o) -> (o) -> (o) -> (o) -> o, D3:o, D4:o,
        D5:o, R:(o) -> o, a1:o, a2:o, M:o, N:o, T:o, V:o
Nominals: n3:o, n2:o, n1:o, n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H3:{M : tm}*
H4:{N : tm}*
H5:{V : tm}*
H6:{n:tm |- R n : tm}*
H7:{D3 : ty}*
H8:{a1 : eval M (abs D3 ([x]R x))}*
H9:{a2 : eval (R N) V}*
H10:{M : tm}
H11:{N : tm}
H12:{T : ty}
H13:{D3 : ty}
H14:{D4 : of M (arr D3 T)}
H15:{D5 : of N D3}
H17:{n1:tm |- R n1 : tm}
H18:{D3 : ty}
H19:{T : ty}
H20:{n2:tm, n3:of n2 D3 |- a3 n n2 n3 : of (R n2) T}
H21:{n3:of N D3 |- a3 n N n3 : of (R N) T}
H22:{a3 n N D5 : of (R N) T}
H23:{D n3 n2 n1 n : of V T}
 
==================================
{D n3 n2 n1 n : of V T}
 
Subgoal sr_eval.2 is:
 exists D, {D : of (abs T1 ([x]R x)) T}

Adelfa is now able to complete the proof by identifying the goal formula with the identical assumption formula H23. This completes the subgoal, and Adelfa moves to the next subgoal.


sr_eval.1>> search.
 
Subgoal sr_eval.2:
 
Vars: T1:o, R:(o) -> o, D2:o, T:o
Nominals: n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H2:{D2 : of (abs T1 ([x]R x)) T}
H3:{n:tm |- R n : tm}*
H4:{T1 : ty}*
 
==================================
exists D, {D : of (abs T1 ([x]R x)) T}

This subgoal corresponds to when the term E is an abstraction and so evaluates to itself. The proof in this case will simply instantiate the D in the goal formula with D2 which we know is typeable at the indicated type by the second assumption formula. An application of the search tactic will complete the proof.


sr_eval.2>> exists D2.
 
Subgoal sr_eval.2:
 
Vars: T1:o, R:(o) -> o, D2:o, T:o
Nominals: n:o
IH:
    forall E, forall V, forall T, forall D1, forall D2,
      {D1 : eval E V}* => {D2 : of E T} => exists D, {D : of V T}
H2:{D2 : of (abs T1 ([x]R x)) T}
H3:{n:tm |- R n : tm}*
H4:{T1 : ty}*
 
==================================
{D2 : of (abs T1 ([x]R x)) T}


sr_eval.2>> search.
Proof Completed!

Summary

The full output for the proof development is included here. In these code blocks, tactics can be hovered over in order to see what the resulting proof state is.

Full development

stlc.ath


Specification "stlc.lf".
 
%subject reduction for stlc
Theorem sr_eval : forall E V T D1 D2,
  {D1 : eval E V} => {D2 : of E T} => exists D, {D : of V T}
induction on 1 intros case H1
  %case 1: application; D1 = eval-app M N V R T1 a1 a2, E = app M N
    case H2 %D2 = of_app M N T D3 D4 D5
    apply IH to H7 H13
    case H15
    inst H19 with n2 = N inst H20 with n3 = D5
    apply IH to H8 H21
    exists (D n3 n2 n1 n)
    search
  %case 2: abstraction; D1 = eval-abs R T1, E = abs T1 ([x]R x)
    exists D2
    search

Exercise

As an exercise, try to prove a follow up theorem that evaluation is deterministic. In other words, multiple evaluations of the same term always results in equivalent results.

For all terms $e$ , $t$ , and $v$ , if $e \Downarrow t$ and $e \Downarrow v$ then $t = v$

You will have to encode the equality of terms in LF before stating the theorem in Adelfa.

Hints & Solution

If you are stuck developing a specification for term equality or want to check your work before moving on to the proof, we go over the encoding here.

Encoding

Developing a specification for equality can be done here with just reflexivity.


tm_eq : tm -> tm -> type.
tm_eq_refl : {E: tm} tm_eq E E.

Proof


Theorem sr_det : forall E V T D1 D2,
  {D1 : eval E V} => {D2 : eval E T} =>
    exists D, {D: tm_eq V T}
induction on 1 intros
case H1
  case H2 apply IH to H7 H13 case H15
  apply IH to H8 H14 exists D n1 n search
 
  case H2 exists tm_eq_refl (abs ([x] R x)) search