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

`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.

`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).

`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.

`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.

`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.

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);

`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)]`

.

`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)]`

.

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'];

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];

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'];

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'];

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];

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];