The mechanization highlights several aspects: - Induction on universally quantified objects - Stating and proving properties in a generalized context - Reasoning using context subsumption }}% %{{ ## Syntax We first define lambda-terms in the logical framework LF using Beluga-style syntax. }}% LF tm: type = | app: tm -> tm -> tm | lam: (tm -> tm) -> tm ; %{{ The type for

`lam`

reflects that binders are represented in the object language using binders in the HOAS meta-language.
## Judgements and Rules We describe algorithmic and declarative equality for the untyped lambda-calculus using axioms and inference rules. The Beluga code is a straightforward HOAS encoding of the associated rules.}}% % --------------------------------------------------------------------------- %{{ ### Algorithmic Equality For algorithmic equality, we have the predicate

`aeq`

of type `tm -> tm -> type`

, and inference rules for term applications `ae_a`

and lambda-abstractions `ae_l`

}}%
LF aeq: tm -> tm -> type =
| ae_a : aeq M1 N1 -> aeq M2 N2 -> aeq (app M1 M2) (app N1 N2)
| ae_l : ({x : tm} aeq x x -> aeq (M x) (N x))
-> aeq (lam (\x. M x)) (lam (\x. N x))
;
% ---------------------------------------------------------------------------
%{{
### Declarative Equality
Next we define declarative equality in order to establish its equivalence with algorithmic equality and prove completeness. Note that the only difference between the two judgements is that declarative equality explicitly includes inference rules for reflexivity `de_r`

, transitivity `de_t`

, and symmetry `de_s`

: properties which we will prove to be intrinsic to algorithmic equality in the untyped lambda-calculus.}}%
LF deq: tm -> tm -> type =
| de_l: ({x:tm} deq x x -> deq (M x) (M' x))
-> deq (lam (\x. M x)) (lam (\x. M' x))
| de_a: deq M1 N1 -> deq M2 N2
-> deq (app M1 M2) (app N1 N2)
| de_r: deq M M
| de_t: deq M L -> deq L N
-> deq M N
| de_s: deq T S -> deq S T
;
% ---------------------------------------------------------------------------
%{{ ## Context schemas
Just as types classify expressions, contexts are classified by context schemas.}}%
schema xaG = block x:tm, ae_v:aeq x x;
schema daG = block (x: tm, ae_v:aeq x x, de_v:deq x x) ;
%{{
## Proof of Reflexivity
We first prove admissibility of reflexivity. The proof is implemented as a recursive function called `reflG`

of type `{g:xaG}{M:[gamma |- tm ]}[gamma |- aeq M M]`

: for all contexts `g`

that have schema `xaG`

, for all terms `M`

, we have a proof that `[gamma |- aeq M M]`

. Quantification over contexts and contextual objects in computation-level types is denoted by curly braces; the corresponding abstraction on the level of expressions is written as `mlam g => mlam M => e`

.}}%
rec reflG: {gamma:xaG} {M:[gamma |- tm]} [gamma |- aeq M M] =
mlam gamma => mlam M => case [gamma |- M] of
| [gamma |- #p.1] => [gamma |- #p.2]
| [gamma |- lam \x. M] =>
let [gamma,b:block y:tm, ae_v:aeq y y |- D[..,b.1,b.2]] =
reflG [gamma, b:block y:tm, ae_v:aeq y y] [gamma, b |- M[..,b.1]]
in
[gamma |- ae_l \x. \w. D] % : eq L L
| [gamma |- app M1 M2] =>
let [gamma |- D1] = reflG [gamma] [gamma |- M1 ] in
let [gamma |- D2] = reflG [gamma] [gamma |- M2 ] in
[gamma |- ae_a D1 D2]
;
%{{In the proof for `reflG`

we begin by introducing and `M`

followed by a case analysis on `[gamma |- M]`

using pattern matching. There are three possible cases for `M`

:
**Variable case.**If`M`

is a variable from`g`

, we write`[gamma |- #p.1]`

where`#p`

denotes a parameter variable declared in the context`g`

. Operationally,`#p`

can be instantiated with any bound variable from the context`g`

. Since the context`g`

has schema`xaG`

, it contains blocks`x:tm , ae_v:aeq x x.`

The first projection allows us to extract the term component, while the second projection denotes the proof of`aeq x x`

.**Lambda case.**If`M`

is a lambda-term, then we extend the context and appeal to the induction hypothesis by making a recursive call. Beluga supports weakening which allows us to use M that has type`[g, x:tm |- tm ]`

in the extended context`[g, b:block y:tm , ae_v: aeq y y]`

. We simply construct a weakening substitution`.. b.1`

with domain`g,y:tm`

and range`g, b:block y:tm , ae_v:aeq y y.`

that essentially renames`y`

to`b.1`

in`M`

. The recursive call returns`[g,b:block y:tm ,ae_v:aeq y y |- D[.., b.1, b.2]]`

. Using it together with rule`ae_l`

we build the final derivation.**Application case.**If`M`

is an application, we appeal twice to the induction hypothesis and build a proof for`[gamma |- aeq (app M1 M2) (app M1 M2)]`

.

`[gamma |- aeq M L]`

to arrive at the second `[gamma |- aeq L N]`

. The recursive function `transG`

handles the three cases for variables, lambda-terms, and applications in a similar fashion to `reflG`

}. The context `g:xaG`

is surrounded by parentheses `( )`

to indicate that it is implicit in the actual proof and need to be reconstructed. }}%
rec transG: (gamma:xaG)
[gamma |- aeq M L] -> [gamma |- aeq L N]
-> [gamma |- aeq M N] =
fn d1 => fn d2 => case d1 of
| [gamma |- #p.2] => d2
| [gamma |- ae_l \x.\u. D1] =>
let [gamma |- ae_l \x.\u. D2] = d2 in
let [gamma, b:block x:tm, ae_v:aeq x x |- E[..,b.1,b.2]] =
transG [gamma, b:block x':tm, ae_v:aeq x' x' |- D1[..,b.1,b.2]]
[gamma, b |- D2[..,b.1,b.2]]
in
[gamma |- ae_l \x. \u. E]
| [gamma |- ae_a D1 D2] =>
let [gamma |- ae_a F1 F2] = d2 in
let [gamma |- E1] = transG [gamma |- D1] [gamma |- F1] in
let [gamma |- E2] = transG [gamma |- D2] [gamma |- F2] in
[gamma |- ae_a E1 E2]
;
%{{Here, the variable case exploits that if `aeq M N`

is an element of the context `g`

, then `M = N`

. Note that the recursive calls do not take the context `g`

as an explicit argument.}}%
% ---------------------------------------------------------------------------
% General symmetry is admissible
%{{
## Proof of Symmetry
Again, we encode the proof of symmetry as a recursive function `symG`

. As in `transG`

, the context `g`

is implicit. Furthermore, we handle the variable case using the same property in both functions.
}}%
rec symG: (gamma:xaG)
[gamma |- aeq M L] -> [gamma |- aeq L M] =
fn d => case d of
| [gamma |- #p.2] => d
| [gamma |- ae_l \x.\u. D1] =>
let [gamma, b:block x:tm, ae_v:aeq x x |- E[..,b.1,b.2]] =
symG [gamma, b:block x':tm, ae_v:aeq x' x' |- D1[..,b.1,b.2]]
in
[gamma |- ae_l \x. \u. E]
| [gamma |- ae_a D1 D2] =>
let [gamma |- E1] = symG [gamma |- D1] in
let [gamma |- E2] = symG [gamma |- D2] in
[gamma |- ae_a E1 E2]
;
% ---------------------------------------------------------------------------
%{{
## Proof of Completeness
Finally, we implement the completeness proof as as a recursive function `ceqG`

.
}}%
rec ceq: (gamma:daG) [gamma |- deq M N] -> [gamma |- aeq M N] =
fn e => case e of
| [gamma |- #p.3] => [gamma |- #p.2]
| [gamma |- de_r] => reflG [gamma] [gamma |- _ ]
| [gamma |- de_a D1 D2] =>
let [gamma |- F1] = ceq [gamma |- D1] in
let [gamma |- F2] = ceq [gamma |- D2] in
[gamma |- ae_a F1 F2]
| [gamma |- de_l (\x.\u. D)] =>
let [gamma,b:block x:tm, _t:aeq x x, u:deq x x |- F[..,b.1,b.2]] =
ceq [gamma, b:block x:tm, _t:aeq x x, u:deq x x |- D[..,b.1,b.3]]
in
[gamma |- ae_l (\x.\v. F)]
| [gamma |- de_t D1 D2] =>
let [gamma |- F2] = ceq [gamma |- D2] in
let [gamma |- F1] = ceq [gamma |- D1] in
transG [gamma |- F1] [gamma |- F2]
| [gamma |- de_s D] =>
let [gamma |- F] = ceq [gamma |- D] in
symG [gamma |- F]
;
%{{
We explain here the three cases shown in the informal proof in the companion paper (Felty et al, 2014). First, let us consider the case where we used an assumption from the context. Since the context `g`

consists of blocks with the following structure: `block x:tm , ae_v:aeq x x,de_v: deq x x`

, we in fact want to match on the third element of such a block. This is written as `#p.3`

. The type of `#p.3`

is `deq #p.1 #p.1`

. Since our context always contains a block and the parameter variable `#p`

describes such a block, we know that there exists a proof for `aeq #p.1 #p.1`

, which can be described by `#p.2`

.

Second, we consider the case where we applied the reflexivity rule `de_r`

as a last step. In this case, we need to refer to the reflexivity lemma we proved about algorithmic equality. To use the function `reflG`

, which implements the reflexivity lemma for algorithmic equality, we need a context of schema `xaG`

; however, the context used in the proof for `ceqG`

is of schema `daG`

and we rely on context subsumption to justify passing a context `daG`

in place of a context `xaG`

. The cases for transitivity and symmetry are similar.

Third, we consider the case for `de_l`

, the case for lambda-abstractions. In this case, we extend the context with the new declarations about variables and pass to the recursive call `ceqG`

the derivation `[gamma, b:block (x:tm ,ae_v:aeq x x, de_v: deq x x) |- D[..,b.1, b.3]]`

. Declaration weakening (in the informal proof d-wk (Felty et al, 2014)) is built-in. In the pattern, the derivation `D`

has type `[gamma, x:tm , ae_v:aeq x x |- deq M[..,x] N]`

. We hence construct a weakening substitution `.. b.1 b.3`

that allows us to move `D`

to the context `gamma, b:block (x:tm,ae_v:aeq x x, de_v:deq x x)`

. The result of recursive call is a derivation `F`

, where `F`

only depends on `x:tm`

and `u:aeq x x`

. In the on-paper proof we refer to declaration strengthening (d-str) to justify that `F`

cannot depend on `de_v`

assumptions. In Beluga, the programmer uses strengthening by stating which assumptions `F`

can depend on. The coverage checker will then subsequently rely on subordination to verify that the restricted case is sufficient and no other cases have been forgotten. Subordination allows us to verify that indeed assumptions of type `de_v: deq x x`

cannot be used in proofs for `aeq M[.., b.1] N[.., b.1]`

. Finally, we use `F`

to assemble the final result `ae_l (\x.\v. F)`

.

We conclude this example with a few observations: The statement of the theorem is directly and succinctly represented in Beluga using contextual types and contextual objects. Every case in the on-paper proof corresponds directly to a case in the implementation of the recursive function. Type reconstruction is used to reconstruct implicit type arguments and infer the type of free contextual variables that occur in patterns. This is crucial to achieve a palatable source language. Weakening and strengthening are supported in Beluga through the typing rules and on the level of context variables and context schemas using context subsumption. If schema `W`

is a prefix of a schema `W'`

, then we can always use a context of schema `W'`

in place of a context of schema `W`

.