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
:
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;
.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.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
:
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
.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.M
is an application, we appeal twice to the induction hypothesis and build a proof for [γ ⊢ aeq (app M1 M2) (app M1 M2)]
.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.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];