Tutorial

Proofs about the simply-typed lambda-calculus

1. Type uniqueness

2. Reasoning about paths in lambda-terms

3. Subject reduction

4. Equality reasoning

To illustrate some issues when combining lemmas, we choose equality reasoning. To simplify matters this example will concentrate on untyped lambda-terms. They are defined as before but lambda-abstractions do not carry type annotations. The example is a quite simple, but it has the advantage that it is easily understood and helps the novice understand the issues arising when formalizing a given formal system together with proofs.

If you'd like to run this example using Beluga, please download equal-proof.bel, which contains all the data-type definitions and the implementation of all the proofs as recursive functions.

We first define a declarative definition of equality which we call equal and then give an algorithmic equality definition, called eq where general reflexivity and transitivity rules can be proven to be admissible. Then we prove the equivalence between both definitions of equality.

First, we define the declarative equality using equal. In particular, it has a generic reflexivity rule, called e_r, and a generic transitivity rule, called e_t. 

datatype equal : exp → exp → type =
| e_l : ({x:exp} equal x x → equal (T x) (T' x)) 
        → equal (lam (\x. T x)) (lam (\x. T' x))
| e_a : equal T2 S2  → equal T1 S1 → equal (app T1 T2) (app S1 S2)
| e_r : equal T T
| e_t : equal T' S → equal T T' → equal T S
;

For each variable we add the fact that equal x x. Next, we define the algorithmic equality using eq. 

datatype eq: exp → exp → type =   
| eq_app : eq M1 N1 → eq M2 N2 → eq (app M1 M2) (app N1 N2)
| eq_lam :  ({x : exp} eq x x → eq (M x) (N x))
         → eq (lam (\x. M x)) (lam (\x. N x))
;

For algorithmic equality, we can prove reflexivity to be admissible. Before we state the reflexivity and transitivity theorems we will carefully define the context used when reasoning about the equality of terms.

Ψ ::= . | Ψ, eq x x

We define the shape of contexts in Beluga using context schema as follows: 

schema eqCtx = block x: exp . eq x x ;

Theorem (Reflexivity): For all M, Ψ ⊢ eq M M.

The reflexivity theorem is represented as a computation-level type in Beluga and its proof corresponds to a recursive program of this type. The reflexivity theorem can then be implemented as a recursive function called ref which will have the following type: {g:eqCtx} {M:[g. exp]} [g. eq (M ..) (M ..)].

Quantification over the context variable g is written using curly brackets in {g:(eqctx)*}. The context schema name is annotated with * to mark that we pass the context explicitely. {M:[g. exp]} is concrete syntax for universal quantification over the meta-variable M. The contextual type exp[g] describes an expression M which may refer to declarations in the context g. When we use M we associate it with the substitution .. which denotes the identity substitution from the context g to itself. Intuitively, it says that M may refer to all variables declared in the context g. 

rec ref : {g:eqCtx} {M:[g. exp]} [g. eq (M ..) (M ..)] =
mlam g ⇒ mlam M ⇒ case [g. M ..] of
| [g. #p.1 ..] ⇒ [g. #p.2 ..]              

| [g. lam \x. N .. x] ⇒
  let [g,b:block y:exp. eq y y. E .. b] =  
    ref [g, b:block q:exp. eq q q] [g, b. N .. b.1] in
    [g. eq_lam \x. \w. (E .. x, w)]

| [g. app (M1 ..) (M2 ..)]  ⇒
  let [g. E1 ..] = ref [g] [g . M1 ..] in
  let [g. E2 ..] = ref [g] [g . M2 ..] in
    [g. eq_app (E1 ..) (E2 ..)]
;

Theorem (Transitivity): If Ψ ⊢ eq M K and Ψ ⊢ eq K N then Ψ ⊢ eq M N.

The transitivity theorem is represented as a computation-level type in Beluga and its proof corresponds to a recursive program of this type. 

rec trans: (g:eqCtx)[g. eq (M ..) (K ..)]  → [g. eq (K ..) (N ..)]    
        → [g. eq (M ..) (N ..)]  =
fn e1 ⇒ fn e2 ⇒ case e1 of
| [g. #p.2 ..] ⇒ e2

| [g. eq_lam \x.\u. D1 .. x u] ⇒
  let [g. eq_lam \x.\u. D2 .. x u] =  e2  in	
  let [g, b:block x:exp. eq x x. E .. b] = 
    trans [g, b:block x':exp. eq x' x'. D1 .. b.1 b.2]
          [g, b. D2 .. b.1 b.2]
  in
    [g. eq_lam \x. \u. E .. x, u]
       
| [g. eq_app (D1 ..) (D2 ..)] ⇒
  let [g. eq_app (F1 ..) (F2 ..)] = e2 in 
  let [g. E1 ..] = trans [g. D1 ..]  [g. F1 ..] in
  let [g. E2 ..] = trans [g. D2 ..]  [g. F2 ..] in
    [g. eq_app  (E1 ..)  (E2 ..)]
;

Finally, we will show the proof for completeness, i.e., every proof using declarative equality can be translated in a proof using algorithmic equality.

schema equalCtx = some [] block x: exp, u:eq x x . equal x x ;

rec ceq: (g:equalCtx) [g. equal (T ..) (S ..)] → [g. eq (T ..) (S ..)]  =
fn e ⇒ case e of 
| [g. #p.3] .. ⇒ [g. #p.2 ..]

| [g. e_r] ⇒ ref [g] [g. _]

| [g. e_t (D2 ..) (D1 ..)] ⇒ 
  let [g. F2 ..] = ceq [g. D2 ..] in 
  let [g. F1 ..] = ceq [g. D1 ..] in 
    trans [g] [g. F1 ..]  [g. F2 ..]           

| [g. e_l (\x.(\u. (D .. x u))] ⇒ 
  let [g,b:block x:exp,u:eq x x . equal x x. F .. b.1 b.2] = 
        ceq ([g, b:block x:exp, u:eq x x . equal x x. D .. b.1 b.3]
  in
     [g. eq_lam (\x.\v. F .. x v)]

| [g. e_a (D2 ..) (D1 ..)] ⇒ 
  let [g. F1 ..] = ceq [g. D1 ..] in 
  let [g] F2 .. = ceq  [g. D2 ..] in 
      [g. eq_app (F1 ..) (F2 ..)]

;


rec ceq_main: [ . equal T S] → [ . eq T S] =  fn e ⇒  ceq e ;

The most interesting part about this proof is the fact that we need context subsumption. For example, in the case where we have applied as a last rule to equal (T ..) (S ..) the rule e_r, we refer to the reflexivity lemma by calling the previously defined function ref. However, the function ref expects a contxt eqCtx. Since the context schema eqCtx is a prefix of the schema equalCtx, we can always weaken any object originally defined in a context of schema eqCtx to obtain an object defined in a context of schema equalCtx.

More explanation regarding this example can be found in "Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison" by Amy Felty and Brigitte Pientka.

5. Reasoning about smaller relation on lambda-terms