# Algorithmic Equality for System F (G-version)

We discuss completeness of algorithmic equality for typed lambda-terms with respect to declarative equality of lambda-terms. This case-study is part of ORBI, Open challenge problem Repository for systems reasoning with BInders. For a detailed description of the proof and a discussion regarding other systems see (Felty et al, 2014).The mechanization highlights several aspects:

- Context schemas with alternative assumptions
- Induction on universally quantified objects
- Stating and proving properties in a generalized context
- Reasoning using context subsumption

## Syntax

System F is described with the following declarations:`tp : `type .

%name tp T a

arr : tp → tp → tp.

all : (tp → tp) → tp.

term : type .

%name term M x

app : term → term → term.

lam : (term → term) → term.

tlam : (tp → term) → term.

tapp : term → tp → term.

## Judgements and Rules

We describe algorithmic and declarative equality for System F as judgements using axioms and inference rules. The Beluga code is a straightforward HOAS encoding of the associated rules.### Algorithmic Equality for types

We add the judgement for type equality`atp`

of type `tm → tm → type`

along with inference rules for universal quantifiers `at_al`

and arrow types `at_arr`

.`atp : tp → tp → `type .

%name atp Q u

at_al : ({a : tp} (atp a a → atp (T a) (S a))) → atp (all T) (all S).

at_arr : atp T1 T2 → atp S1 S2 → atp (arr T1 S1) (arr T2 S2).

### Algorithmic Equality for terms

We extend the term equality judgement given for the untyped lambda-calculus with rules for type abstraction`ae_tl`

and type application `ae_ta`

.`aeq : term → term → `type .

%name aeq D u

ae_a : aeq M1 N1 → aeq M2 N2 → aeq (app M1 M2) (app N1 N2).

ae_l : ({x : term} (aeq x x → aeq (M x) (N x))) → aeq (lam (λx. M x)) (lam (λx. N x)).

ae_tl : ({a : tp} (atp a a → aeq (M a) (N a))) → aeq (tlam (λa. M a)) (tlam (λa. N a)).

ae_ta : aeq M N → atp T S → aeq (tapp M T) (tapp N S).

Note that type equality `atp A B`

can be defined independently of term equality `aeq M N`

. In other words, `aeq M N`

depends on `atp A B`

, but not vice-versa.

### Declarative Equality for types

We define declarative equality for types in order to establish its equivalence with algorithmic equality and prove completeness. Rules for reflexivity, transitivity, and symmetry are explicitly derived.`dtp : tp → tp → `type .

%name atp P u

dt_al : ({a : tp} (dtp a a → dtp (T a) (S a))) → dtp (all T) (all S).

dt_arr : dtp T1 T2 → dtp S1 S2 → dtp (arr T1 S1) (arr T2 S2).

dt_r : dtp T T.

dt_t : dtp T R → dtp R S → dtp T S.

dt_s : dtp T S → dtp S T.

### Declarative Equality for terms

Declarative equality for terms is encoded similarly to its counterpart. Again, we are extending the Untyped Equality case study with constructors for type abstraction`de_tl`

and type application `de_ta`

`deq : term → term → `type .

de_l : ({x : term} (deq x x → deq (M x) (N x))) → deq (lam (λx. M x)) (lam (λx. N x)).

de_a : deq M1 N1 → deq M2 N2 → deq (app M1 M2) (app N1 N2).

de_tl : ({a : tp} (dtp a a → deq (M a) (N a))) → deq (tlam (λa. M a)) (tlam (λa. N a)).

de_ta : deq M N → dtp T S → deq (tapp M T) (tapp N S).

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 declarations

Just as types classify expressions, contexts are classified by context schemas.schema atpCtx = block (a:tp, _t:atp a a);

Since the case for lambda-abstraction `lam`

deals with term assumptions while the type abstraction `tlam`

introduces type assumptions, we need to specify *alternating* assumptions. This alternation of blocks is described by using `+`

in Beluga's concrete syntax.

schema aeqCtx = block (x:term, _u:aeq x x) + block (a:tp, _t:atp a a);

schema dtpCtx = block (a:tp, u:atp a a, _t:dtp a a);

schema deqCtx = block (x:term, u:aeq x x, _t:deq x x) + block (a:tp, u:atp a a, _t:dtp a a);

## Proof of Reflexivity for Types

The reflexivity for types is implemented as a recursive function called`reftp`

of type: `{γ:atpCtx}{T:[γ ⊢ tp ]}[γ ⊢ atp T T]`

. This can be read as: for all contexts `g`

that have schema `atpCtx`

, for all types `T`

, we have a proof that `[ g ⊢ atp T T]`

. Quantification over contexts and contextual objects in computation-level types is denoted between braces `{}`

; the corresponding abstraction on the level of expressions is written as `mlam g ⇒ mlam T1 ⇒ e`

.rec reftp : {γ : atpCtx} {T : [γ ⊢ tp]} [γ ⊢ atp T T] =
mlam γ ⇒ mlam T ⇒ case [γ ⊢ T] of
| [γ ⊢ #p.1] ⇒ [γ ⊢ #p.2]
| [γ ⊢ all (λx. T)] ⇒
let [γ, b : block (a:tp, _t:atp a a) ⊢ D[…, b.1, b.2]] =
reftp [γ, b : block (a:tp, _t:atp a a)] [γ, b ⊢ T[…, b.1]] in [γ ⊢ at_al (λx. λw. D)]
| [γ ⊢ arr T S] ⇒
let [γ ⊢ D1] = reftp [γ] [γ ⊢ T] in
let [γ ⊢ D2] = reftp [γ] [γ ⊢ S] in [γ ⊢ at_arr D1 D2];

In the proof for `refltp`

we begin by introducing and `T`

followed by a case analysis on `[γ ⊢ T]`

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

:

**Variable case.**If`T`

is a variable from`g`

, we write`[γ ⊢ #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`atpCtx`

, it contains blocks`a:tp , _t:atp a a;`

. The first projection allows us to extract the type component, while the second projection denotes the proof of`_t:atp a a;`

.**Existential case.**If`T`

is an existential quantification, then we extend the context and appeal to the induction hypothesis by making a recursive call. Beluga supports declaration weakening which allows us to use`T`

that has type`[γ, a:tp ⊢ tp ]`

in the extended context`[γ, b:block a:tp , _t: atp a a]`

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

with domain`g,a:tp`

and range`g, b:block a:tp , _t: atp a a`

that essentially renames`a`

to`b.1`

in`T`

. The recursive call returns`[γ,b:block a:tp , _t:atp a a ⊢ D[…, b.1 ,b.2]]`

. Using it together with rule`at_la`

we build the final derivation.**Arrow case.**If`T`

is an arrow type, we appeal twice to the induction hypothesis and build a proof for`[γ ⊢ atp (arr T S) (arr T S)]`

.

## Proof of Reflexivity for Terms

The recursive function`ref`

encodes the proof reflexivity for terms. The type signature reads: for all contexts `g`

that have schema `aeqCtx`

, for all terms `M`

, we have a proof that `[ g ⊢ aeq M M]`

.rec ref : {γ : aeqCtx} {M : [γ ⊢ term]} [γ ⊢ aeq M M] =
mlam γ ⇒ mlam M ⇒ case [γ ⊢ M] of
| [γ ⊢ #p.1] ⇒ [γ ⊢ #p.2]
| [γ ⊢ lam (λx. M)] ⇒
let [γ, b : block (y:term, _t:aeq y y) ⊢ D[…, b.1, b.2]] =
ref [γ, b : block (y:term, _t:aeq y y)] [γ, b ⊢ M[…, b.1]] in [γ ⊢ ae_l (λx. λw. D)]
| [γ ⊢ app M1 M2] ⇒
let [γ ⊢ D1] = ref [γ] [γ ⊢ M1] in
let [γ ⊢ D2] = ref [γ] [γ ⊢ M2] in [γ ⊢ ae_a D1 D2]
| [γ ⊢ tlam (λa. M)] ⇒
let [γ, b : block (a:tp, _t:atp a a) ⊢ D[…, b.1, b.2]] =
ref [γ, b : block (a:tp, _t:atp a a)] [γ, b ⊢ M[…, b.1]] in [γ ⊢ ae_tl (λx. λw. D)]
| [γ ⊢ tapp M T] ⇒
let [γ ⊢ D1] = ref [γ] [γ ⊢ M] in
let [γ ⊢ D2] = reftp [γ] [γ ⊢ T] in [γ ⊢ ae_ta D1 D2];

This time, there are five possible cases for our meta-variable `M`

:

**Variable case.**If`M`

is a variable from`g`

, we write`[γ ⊢ #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`aeqCtx`

, 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-abstraction case.**If`M`

is a lambda-term, then we extend the context and appeal to the induction hypothesis by making a recursive call. Automatic context subsumption comes into play again, allowing us to use M that has type`[γ, x:tm ⊢ tm ]`

in the extended context`[γ, 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`[γ,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.**Term application case.**If`M`

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

.**Type abstraction case.**If`M`

is a type abstraction, then we extend the context and appeal to the induction hypothesis by making a recursive call. We use`M`

that has type`[γ, a:tp ⊢ tp ]`

in the extended context`[γ, b:block a:tp , _t: atp a a]`

and construct a weakening substitution`… b.1`

with domain`g,a:tp`

and range`g, b:block a:tp , _t: atp a a`

that essentially renames`a`

to`b.1`

in`T`

. The recursive call returns`[γ,b:block a:tp , _t:atp a a ⊢ D[…, b.1, b.2]]`

. Using it together with rule`at_la`

we build the final derivation.**Type application case.**If`M`

is a type application, we appeal twice to the induction hypothesis and build a proof for`[γ ⊢ aeqCtx (tapp M T) (tapp M T)]`

.

## Proof of Transitivity for Types

rec transtp : (γ:atpCtx) [γ ⊢ atp T R] → [γ ⊢ atp R S] → [γ ⊢ atp T S] =
fn ae1 ⇒ fn ae2 ⇒ case ae1 of
| [γ ⊢ #p.2] ⇒ ae2
| [γ ⊢ at_al (λa. λu. D1[…, a, u])] ⇒
let [γ ⊢ at_al (λa. λu. D2[…, a, u])] = ae2 in
let [γ, b : block (a:tp, _t:atp a a) ⊢ D[…, b.1, b.2]] =
transtp [γ, b : block (a:tp, _t:atp a a) ⊢ D1[…, b.1, b.2]] [γ, b ⊢ D2[…, b.1, b.2]] in
[γ ⊢ at_al (λa. λu. D[…, a, u])]
| [γ ⊢ at_arr D1 D2] ⇒
let [γ ⊢ at_arr D3 D4] = ae2 in
let [γ ⊢ D] = transtp [γ ⊢ D1] [γ ⊢ D3] in
let [γ ⊢ D'] = transtp [γ ⊢ D2] [γ ⊢ D4] in [γ ⊢ at_arr D D'];

## Proof of Transitivity for Terms

rec trans : (γ:aeqCtx) [γ ⊢ aeq T R] → [γ ⊢ aeq R S] → [γ ⊢ aeq T S] =
fn ae1 ⇒ fn ae2 ⇒ case ae1 of
| [γ ⊢ #p.2] ⇒ ae2
| [γ ⊢ ae_l (λx. λu. D1)] ⇒
let [γ ⊢ ae_l (λx. λu. D2)] = ae2 in
let [γ, b : block (x:term, _t:aeq x x) ⊢ D[…, b.1, b.2]] =
trans [γ, b : block (x':term, _t:aeq x' x') ⊢ D1[…, b.1, b.2]] [γ, b ⊢ D2[…, b.1, b.2]] in
[γ ⊢ ae_l (λx. λu. D)]
| [γ ⊢ ae_a D1 D2] ⇒
let [γ ⊢ ae_a D3 D4] = ae2 in
let [γ ⊢ D] = trans [γ ⊢ D1] [γ ⊢ D3] in
let [γ ⊢ D'] = trans [γ ⊢ D2] [γ ⊢ D4] in [γ ⊢ ae_a D D']
| [γ ⊢ ae_tl (λa. λu. D1[…, a, u])] ⇒
let [γ ⊢ ae_tl (λa. λu. D2[…, a, u])] = ae2 in
let [γ, b : block (a:tp, _t:atp a a) ⊢ D[…, b.1, b.2]] =
trans [γ, b : block (a:tp, _t:atp a a) ⊢ D1[…, b.1, b.2]] [γ, b ⊢ D2[…, b.1, b.2]] in
[γ ⊢ ae_tl (λx. λu. D)]
| [γ ⊢ ae_ta D1 Q1] ⇒
let [γ ⊢ ae_ta D2 Q2] = ae2 in
let [γ ⊢ D] = trans [γ ⊢ D1] [γ ⊢ D2] in
let [γ ⊢ Q] = transtp [γ ⊢ Q1] [γ ⊢ Q2] in [γ ⊢ ae_ta D Q];

## Proof of Symmetry for Types

rec symtp : (γ:atpCtx) [γ ⊢ atp T R] → [γ ⊢ atp R T] =
fn ae ⇒ case ae of
| [γ ⊢ #p.2] ⇒ ae
| [γ ⊢ at_al (λx. λu. D)] ⇒
let [γ, b : block (a:tp, _t:atp a a) ⊢ D'[…, b.1, b.2]] =
symtp [γ, b : block (a:tp, _t:atp a a) ⊢ D[…, b.1, b.2]] in [γ ⊢ at_al (λx. λu. D')]
| [γ ⊢ at_arr D1 D2] ⇒
let [γ ⊢ D1'] = symtp [γ ⊢ D1] in
let [γ ⊢ D2'] = symtp [γ ⊢ D2] in [γ ⊢ at_arr D1' D2'];

## Proof of Symmetry for Terms

rec sym : (γ:aeqCtx) [γ ⊢ aeq T R] → [γ ⊢ aeq R T] =
fn ae ⇒ case ae of
| [γ ⊢ #p.2] ⇒ ae
| [γ ⊢ ae_l (λx. λu. D)] ⇒
let [γ, b : block (x:term, _t:aeq x x) ⊢ D'[…, b.1, b.2]] =
sym [γ, b : block (x:term, _t:aeq x x) ⊢ D[…, b.1, b.2]] in [γ ⊢ ae_l (λx. λu. D')]
| [γ ⊢ ae_a D1 D2] ⇒
let [γ ⊢ D1'] = sym [γ ⊢ D1] in
let [γ ⊢ D2'] = sym [γ ⊢ D2] in [γ ⊢ ae_a D1' D2']
| [γ ⊢ ae_tl (λx. λu. D)] ⇒
let [γ, b : block (a:tp, _t:atp a a) ⊢ D'[…, b.1, b.2]] =
sym [γ, b : block (a:tp, _t:atp a a) ⊢ D[…, b.1, b.2]] in [γ ⊢ ae_tl (λx. λu. D')]
| [γ ⊢ ae_ta D Q] ⇒
let [γ ⊢ D'] = sym [γ ⊢ D] in
let [γ ⊢ Q'] = symtp [γ ⊢ Q] in [γ ⊢ ae_ta D' Q'];

## Proof of Completeness for Types

rec ctp : (γ:dtpCtx) [γ ⊢ dtp T S] → [γ ⊢ atp T S] =
fn e ⇒ case e of
| [γ ⊢ #p.3] ⇒ [γ ⊢ #p.2]
| [γ ⊢ dt_r] ⇒ reftp [γ] [γ ⊢ _]
| [γ ⊢ dt_arr F1 F2] ⇒
let [γ ⊢ D1] = ctp [γ ⊢ F1] in
let [γ ⊢ D2] = ctp [γ ⊢ F2] in [γ ⊢ at_arr D1 D2]
| [γ ⊢ dt_al (λx. λu. F)] ⇒
let [γ, b : block (a:tp, u:atp a a, _t:dtp a a) ⊢ D[…, b.1, b.2]] =
ctp [γ, b : block (a:tp, u:atp a a, _t:dtp a a) ⊢ F[…, b.1, b.3]] in
[γ ⊢ at_al (λx. λv. D)]
| [γ ⊢ dt_t F1 F2] ⇒
let [γ ⊢ D2] = ctp [γ ⊢ F2] in
let [γ ⊢ D1] = ctp [γ ⊢ F1] in transtp [γ ⊢ D1] [γ ⊢ D2]
| [γ ⊢ dt_s F] ⇒
let [γ ⊢ D] = ctp [γ ⊢ F] in symtp [γ ⊢ D];

## Proof of Completeness for Terms

rec ceq : (γ:deqCtx) [γ ⊢ deq T S] → [γ ⊢ aeq T S] =
fn e ⇒ case e of
| [γ ⊢ #p.3] ⇒ [γ ⊢ #p.2]
| [γ ⊢ de_r] ⇒ ref [γ] [γ ⊢ _]
| [γ ⊢ de_a F1 F2] ⇒
let [γ ⊢ D1] = ceq [γ ⊢ F1] in
let [γ ⊢ D2] = ceq [γ ⊢ F2] in [γ ⊢ ae_a D1 D2]
| [γ ⊢ de_l (λx. λu. F)] ⇒
let [γ, b : block (x:term, u:aeq x x, _t:deq x x) ⊢ D[…, b.1, b.2]] =
ceq [γ, b : block (x:term, u:aeq x x, _t:deq x x) ⊢ F[…, b.1, b.3]] in
[γ ⊢ ae_l (λx. λv. D)]
| [γ ⊢ de_t F1 F2] ⇒
let [γ ⊢ D2] = ceq [γ ⊢ F2] in
let [γ ⊢ D1] = ceq [γ ⊢ F1] in trans [γ ⊢ D1] [γ ⊢ D2]
| [γ ⊢ de_s F] ⇒
let [γ ⊢ D] = ceq [γ ⊢ F] in sym [γ ⊢ D]
| [γ ⊢ de_tl (λa. λu. F[…, a, u])] ⇒
let [γ, b : block (a:tp, u:atp a a, _t:dtp a a) ⊢ D[…, b.1, b.2]] =
ceq [γ, b : block (a:tp, u:atp a a, _t:dtp a a) ⊢ F[…, b.1, b.3]] in
[γ ⊢ ae_tl (λx. λv. D)]
| [γ ⊢ de_ta F1 P2] ⇒
let [γ ⊢ Q2] = ctp [γ ⊢ P2] in
let [γ ⊢ D1] = ceq [γ ⊢ F1] in [γ ⊢ ae_ta D1 Q2];