Tutorial

1. Type uniqueness

2. Reasoning about paths in lambda-terms

3. Subject reduction

4. Equality reasoning

5. Reasoning about a "smaller" relation on lambda-terms

This simple example illustrates the expressive power of Beluga. It is simpler than the example where we reason about paths in a lambda term. To simplify matters even further, this example uses untyped lambda-terms. They are defined as before, except that lambda-abstractions do not have type annotations.

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

We begin by defining when a lambda-term is a subterm of another lambda-term. The type family lt defines when a term is strictly smaller than another term, and eq defines when two terms are equal. le succeeds if a term is strictly smaller or equal to another term. 

datatype eq : exp → exp → type =
| e_ref: eq T T
;

datatype lt : exp → exp → type =
| lt_lam: ({x:exp}le N (M x)) → lt N (lam M)
| lt_appl: le N M1 → lt N (app M1 M2)
| lt_appr: le N M1 → lt N (app M1 M2)
and le : exp → exp → type =
| le_= : eq M N → le M N
| le_< : lt M N → le M N
;

We want to prove the following theorem:

Theorem: If, for all M, ⊢ le M N implies ⊢ le M K, then ⊢ le N K.

This is a simple example to illustrate the expressive power of Beluga. Because the statements require nested quantification and implication, it is not possible to state this theorem directly in some systems such as the Twelf system.

We will state here a more general version which allows the context to be non-empty.

Lemma: If, for all M, Γ ⊢ le M N implies Γ ⊢ lt M K, then Γ ⊢ le N K.

The context Γ contains assumptions x:exp. 

schema ctx = exp ;

On paper proof:

To prove the above theorem, we proceed as follows: Assume that "for all M, Γ ⊢ le M N implies Γ ⊢ lt M K". Use N to instantiate this assumption and eliminate the universal quantifier. Hence, we obtain: Γ ⊢ le N N implies Γ ⊢ le N K. By reflexivity of equality, using rule e_ref, we know that eq N N. By the rule le_=, we conclude le N N. Hence, we can now use implication elimination and conclude that le N K, which is what we needed to prove.

The proof for the stated lemma can be implemented as a function which has the following type: 

{g:ctx}({M:[g. exp]} [g. le (M ..) (N ..)] → [g. le (M ..) (K ..)])
      → [g. le (N ..) (K ..)]

The type corresponds directly to the specified lemma where {g:ctx} introduces quantification over the context variable g which has schema ctx. Meta-variables written with curly braces such as {M:[g. exp]} correspond to universal quantification over the variables M.

The proof can be implemented as a function in Beluga following closely the more informal development given earlier. We treat computation-level expressions that correspond to quantifier introduction and elimination the same as the expressions corresponding to implication introduction and elimination. To introduce a universally quantified meta-variable M, we write mlam M ⇒ .... To eliminate a universal quantifier, we write e [g.M] where e has type {M:[g. A]}.tau and g.M describes the data-level object used to instantiate the universal quantifier and has type A in the context g. For implication introduction, we write fn x ⇒ .... 


rec lemma : {g:ctx}({M:[g. exp]} [g. le (M ..) (N ..)] → [g. le (M ..) (K ..)])
      → [g. le (N ..) (K ..)]  
 = 
mlam g ⇒ fn f ⇒ f [g. _ ] [g. le_= e_ref] ;

In the code we write _ and let type reconstruction fill in the correct instantiation.