S and T cannot depend on the context g, i.e. they are closed.}}%
rec subst : (g:tCtx)
[g,b: block x:tm, of_v: oft x T[] |- oft M[..,b.1] S[]]
-> [g |- oft N T[]]
-> [g |- oft M[..,N] S[]] =
fn d1 => fn d2 =>
let [g, b: block x:tm, of_v: oft x T |- D1[..,b.1,b.2]] = d1 in
-let [g |- D2[..]] = d2 in
+let [g |- D2] = d2 in
[g |- D1[..,_,D2]]
;
@@ -91,34 +91,34 @@ let [g |- D2[..]] = d2 in
% Type preservation for parallel reduction
%{{
## Type Preservation for Parallel Reductions
-We prove type preservation for parallel reduction: when M steps to N and M has type A then N has the same type A. expressions to depend on the context since we may step terms containing variables. Substitution property for parametric and hypothetical derivations is free. }}%
+We prove type preservation for parallel reduction: when M steps to N and M has type A then N has the same type A. expressions to depend on the context since we may step terms containing variables. Substitution property for parametric and hypothetical derivations is free. We do not enforce here that the type A is closed. Although this is possible by writing A[] the statement looks simpler if we do not enforce this extra invariant.}}%
rec tps : (g:trCtx)
- [g |- pr (M[..]) (N[..])] -> [g |- oft (M[..]) A]
- -> [g |- oft (N[..]) A] =
+ [g |- pr M N] -> [g |- oft M A]
+ -> [g |- oft N A] =
fn r => fn d => case r of
-| [g |- #p.3[..] ] => d
-| [g |- pr_b (\x.\pr_v. R1) (R2[..] ) ] =>
- let [g |- of_app (of_lam (\x.\of_v. D1)) (D2[..]) ] = d in
+| [g |- #p.3 ] => d
+| [g |- pr_b (\x.\pr_v. R1) R2 ] =>
+ let [g |- of_app (of_lam (\x.\of_v. D1)) D2 ] = d in
let [g, b: block x:tm, of_v: oft x T, pr_v: pr x x |- F1[..,b.1,b.2]] =
tps [g, b: block x:tm, of_v: oft x _, pr_v: pr x x |- R1[..,b.1,b.3]]
[g, b |- D1[..,b.1,b.2]] in
- let [g |- F2[..] ] = tps [g |- R2[..]] [g |- D2[..]] in
+ let [g |- F2 ] = tps [g |- R2] [g |- D2] in
[g |- F1[..,_,F2]] % use substitution lemma directly
-| [g |- pr_l \x.\pr_v. R] =>
+| [g |- pr_l \x.\pr_v. R] =>
let [g |- of_lam \x.\of_v. D] = d in
let [g, b: block x:tm, of_v: oft x T, pr_v: pr x x |- F[..,b.1,b.2]] =
tps [g, b: block x:tm, of_v: oft x _, pr_v: pr x x |- R[..,b.1,b.3]]
[g, b |- D[..,b.1,b.2]] in
[g |- of_lam \x.\of_v. F]
-| [g |- pr_a (R1[..]) (R2[..]) ] =>
- let [g |- of_app (D1[..]) (D2[..])] = d in
- let [g |- F1[..] ] = tps [g |- R1[..]] [g |- D1[..]] in
- let [g |- F2[..] ] = tps [g |- R2[..]] [g |- D2[..]] in
- [g |- of_app (F1[..]) (F2[..])]
+| [g |- pr_a R1 R2 ] =>
+ let [g |- of_app D1 D2] = d in
+ let [g |- F1] = tps [g |- R1] [g |- D1] in
+ let [g |- F2] = tps [g |- R2] [g |- D2] in
+ [g |- of_app F1 F2]
;
%{{
-The β-reduction case is perhaps the most note-worthy. We know by assumption that d:[g |- oft (app (lam A (\x. M[..]x))(N[..])) (arr A B) and by inversion that d:[g |- of_a (of_l \x. \u. D1[..]x u)(D2[..]) ] where D1 stands for oft (M[..]x) B in the extended context g, x:tm , u:oft x A. Furthermore, D2 describes a derivation oft (N[..])A. A recursive call on D2 yields F2:oft (N'[..])A. Likewise, y the i.h. on D1, we obtain a derivation g, b:block (x:tm , of_x:oft x A). We now want to substitute for x the term N', and for the derivation oft x A the derivation F2. This is achieved by applying to F1 the substitution .. _ (F2[..]). Since in the program above we do not have the name N available, we write an underscore and let Beluga's type reconstruction algorithm infer the appropriate name.
+The β-reduction case is perhaps the most note-worthy. We know by assumption that d:[g |- oft (app (lam A (\x. M x)) N)) (arr A B) and by inversion that d:[g |- of_a (of_l \x. \u. D1 x u)(D2) ] where D1 stands for oft (M x) B in the extended context g, x:tm , u:oft x A. Furthermore, D2 describes a derivation oft N A. A recursive call on D2 yields F2:oft N' A. Likewise, y the i.h. on D1, we obtain a derivation g, b:block (x:tm , of_x:oft x A). We now want to substitute for x the term N', and for the derivation oft x A the derivation F2. This is achieved by applying to F1 the substitution .., _ F2). Since in the program above we do not have the name N available, we write an underscore and let Beluga's type reconstruction algorithm infer the appropriate name.
}}%
diff --git a/examples/literate_beluga/0Beginner/Polymorphic_Algorithmic_Equality.bel b/examples/literate_beluga/0Beginner/Polymorphic_Algorithmic_Equality.bel
index 6bbec4510..44b91bb9e 100755
--- a/examples/literate_beluga/0Beginner/Polymorphic_Algorithmic_Equality.bel
+++ b/examples/literate_beluga/0Beginner/Polymorphic_Algorithmic_Equality.bel
@@ -92,231 +92,229 @@ schema deqCtx = block x: term, u:aeq x x , _t:deq x x
% ----------------------------------------------------------------- %
% Admissibility of Reflexivity
%{{## Proof of Reflexivity for Types
-The reflexivity for types is implemented as a recursive function called reftp of type: {g:atpCtx}{T:[g |- tp ]}[g |- 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 : {g:atpCtx} {T:[g |- tp]} [g |- atp (T[..]) (T[..])] =
-mlam g => mlam T => case [g |- (T[..])] of
-| [g |- #p.1[..]] => [g |- #p.2[..]]
-
-| [g |- all \x. T] =>
- let [g,b:block a:tp , _t:atp a a |- D[..,b.1,b.2]] =
- reftp [g, b:block a:tp , _t:atp a a] [g, b |- T[..,b.1]]
+The reflexivity for types is implemented as a recursive function called reftp of type: {gamma:atpCtx}{T:[gamma |- tp ]}[gamma |- 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 : {gamma:atpCtx} {T:[gamma |- tp]} [gamma |- atp T T] =
+mlam gamma => mlam T => case [gamma |- T] of
+| [gamma |- #p.1] => [gamma |- #p.2]
+
+| [gamma |- all \x. T] =>
+ let [gamma,b:block a:tp , _t:atp a a |- D[..,b.1,b.2]] =
+ reftp [gamma, b:block a:tp , _t:atp a a] [gamma, b |- T[..,b.1]]
in
- [g |- at_al \x. \w. D]
+ [gamma |- at_al \x. \w. D]
-| [g |- arr (T[..]) (S[..])] =>
- let [g |- D1[..]] = reftp [g] [g |- T[..] ] in
- let [g |- D2[..]] = reftp [g] [g |- S[..] ] in
- [g |- at_arr (D1[..]) (D2[..])]
+| [gamma |- arr T S] =>
+ let [gamma |- D1] = reftp [gamma] [gamma |- T ] in
+ let [gamma |- D2] = reftp [gamma] [gamma |- S ] in
+ [gamma |- at_arr (D1) D2]
;
-%{{In the proof for refltp we begin by introducing and T followed by a case analysis on [g |- T[..]] using pattern matching. There are three possible cases for T:
+%{{In the proof for refltp we begin by introducing and T followed by a case analysis on [gamma |- T] using pattern matching. There are three possible cases for T:
T is a variable from g, we write [g |- #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 [g, a:tp |- tp ] in the extended context [g, 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 [g,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 [g |- atp (arr (T[..]) (S[..])) (arr (T[..]) (S[..]))].
+-Variable case. If T 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 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 [gamma, a:tp |- tp ] in the extended context [gamma, 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 [gamma,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 [gamma |- 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 : {g:aeqCtx} {M:[g |- term]} [g |- aeq (M[..]) (M[..])] =
-mlam g => mlam M => case [g |- (M[..])] of
-| [g |- #p.1[..]] => [g |- #p.2[..]]
-
-| [g |- lam \x. M] =>
- let [g,b:block y:term , _t:aeq y y |- D[..,b.1,b.2]] =
- ref [g, b:block y:term , _t:aeq y y] [g, b |- M[..,b.1]]
+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 : {gamma:aeqCtx} {M:[gamma |- term]} [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:term , _t:aeq y y |- D[..,b.1,b.2]] =
+ ref [gamma, b:block y:term , _t:aeq y y] [gamma, b |- M[..,b.1]]
in
- [g |- ae_l \x. \w. D]
+ [gamma |- ae_l \x. \w. D]
-| [g |- app (M1[..]) (M2[..])] =>
- let [g |- D1[..]] = ref [g] [g |- M1[..] ] in
- let [g |- D2[..]] = ref [g] [g |- M2[..] ] in
- [g |- ae_a (D1[..]) (D2[..])]
+| [gamma |- app M1 M2] =>
+ let [gamma |- D1] = ref [gamma] [gamma |- M1 ] in
+ let [gamma |- D2] = ref [gamma] [gamma |- M2 ] in
+ [gamma |- ae_a D1 D2]
-| [g |- tlam \a. M] =>
- let [g,b:block a:tp , _t:atp a a |- D[..,b.1,b.2]] =
- ref [g, b:block a:tp , _t:atp a a] [g, b |- M[..,b.1]]
+| [gamma |- tlam \a. M] =>
+ let [gamma,b:block a:tp , _t:atp a a |- D[..,b.1,b.2]] =
+ ref [gamma, b:block a:tp , _t:atp a a] [gamma, b |- M[..,b.1]]
in
- [g |- ae_tl \x. \w. D]
+ [gamma |- ae_tl \x. \w. D]
-| [g |- tapp (M[..]) (T[..])] =>
- let [g |- D1[..]] = ref [g] [g |- M[..] ] in
- let [g |- D2[..]] = reftp [g] [g |- T[..] ] in
- [g |- ae_ta (D1[..]) (D2[..])]
+| [gamma |- tapp M T] =>
+ let [gamma |- D1] = ref [gamma] [gamma |- M ] in
+ let [gamma |- D2] = reftp [gamma] [gamma |- T ] in
+ [gamma |- ae_ta D1 D2]
;
%{{This time, there are five possible cases for our meta-variable M:
M is a variable from g, we write [g |- #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 [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.
--Term application case. If M is an application, we appeal twice to the induction hypothesis and build a proof for [g |- 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 [g, a:tp |- tp ] in the extended context [g, 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 [g,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 [g |- aeqCtx (tapp (M[..]) (T[..])) (tapp (M[..]) (T[..]))].
+-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 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 [gamma, x:tm |- tm ] in the extended context [gamma, 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 [gamma,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 [gamma |- 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 [gamma, a:tp |- tp ] in the extended context [gamma, 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 [gamma,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 [gamma |- aeqCtx (tapp M T) (tapp M T)].
h_app, it matches the pattern [g |- h_app D1 D2], and forms a contextual object in the context g of type [g |- hastype M T']. D1 corresponds to the first premise of the typing rule for applications with contextual type [g |- hastype M1 (arr T' T)]. Using a let-binding, we invert the second argument, the derivation f which must have type [g |- hastype (app M1 M2) T]. F1 corresponds to the first premise of the typing rule for applications and has the contextual type [g |- hastype M1 (arr S' S)]. The appeal to the induction hypothesis using D1 and F1 in the on-paper proof corresponds to the recursive call unique [g |- D1] [g |- F1]. Note that while unique’s type says it takes a context variable (g:xtG), we do not pass it explicitly; Beluga infers it from the context in the first argument passed. The result of the recursive call is a contextual object of type [ |- eq (arr T1 T2) (arr S1 S2)]. The only rule that could derive such an object is e_ref, and pattern matching establishes that arr T T' = arr S S’ and hence T = S and T' = S’.Lambda case. If the first derivation d concludes with h_lam, it matches the pattern [g |- h_lam (\x.\u. D u)], and is a contextual object in the context g of type hastype (lam T M) (arr T T'). Pattern matching—through a let-binding—serves to invert the second derivation f, which must have been by h_lam with a subderivation F to reach hastype M S that can use x, _t:hastype x T, and assumptions from g.
The use of the induction hypothesis on D and F in a paper proof corresponds to the recursive call to unique. To appeal to the induction hypothesis, we need to extend the context by pairing up x and the typing assumption hastype x T. This is accomplished by creating the declaration b: block x:term, u:hastype x T. In the code, we wrote an underscore _ instead of T, which tells Beluga to reconstruct it since we cannot write T there without binding it by explicitly giving the type of D. To retrieve x we take the first projection b.x, and to retrieve x’s typing assumption we take the second projection b.u.
Now we can appeal to the induction hypothesis using D1[.., b.x, b.u] and F1[.., b.x, b.u] in the context g,b: block x:term, u:hastype x S. From the i.h. we get a contextual object, a closed derivation of (eq (arr T T') (arr S S’))[ ]. The only rule that could derive this is ref, and pattern matching establishes that S must equal S’, since we must have arr T S = arr T1 S’. Therefore, there is a proof of [ |- equal S S’], and we can finish with the reflexivity rule e_ref.
tm and assumptions hastype x T, we pattern match on [g |- #p.2], i.e., we project out the second argument of the block. By the given assumptions, we know that [g |- #p.2] has type [g |- hastype (#p.1) T], because #p has type [g |- block x:tm , u:hastype x T]. We also know that the second input, called f, to the function unique has type [g |- hastype (#p.1) T']. By inversion on f, we know that the only possible object that can inhabit this type is [g |- #p.2] and therefore T' must be identical to T. Moreover, #r denotes the same block as #p.d concludes with h_app, it matches the pattern [g |- h_app D1 D2], and forms a contextual object in the context g of type [g |- hastype M T'[]]. D1 corresponds to the first premise of the typing rule for applications with contextual type [g |- hastype M1 (arr T'[] T[])]. Using a let-binding, we invert the second argument, the derivation f which must have type [g |- hastype (app M1 M2) T[]]. F1 corresponds to the first premise of the typing rule for applications and has the contextual type [g |- hastype M1 (arr S'[] S[])]. The appeal to the induction hypothesis using D1 and F1 in the on-paper proof corresponds to the recursive call unique [g |- D1] [g |- F1]. Note that while unique’s type says it takes a context variable (g:xtG), we do not pass it explicitly; Beluga infers it from the context in the first argument passed. The result of the recursive call is a contextual object of type [ |- eq (arr T1 T2) (arr S1 S2)]. The only rule that could derive such an object is e_ref, and pattern matching establishes that arr T T' = arr S S’ and hence T = S and T' = S’.
+Lambda case. If the first derivation d concludes with h_lam, it matches the pattern [g |- h_lam (\x.\u. D u)], and is a contextual object in the context g of type hastype (lam T[] M) (arr T[] T'[]). Pattern matching—through a let-binding—serves to invert the second derivation f, which must have been by h_lam with a subderivation F to reach hastype M S[] that can use x, u:hastype x T[], and assumptions from g.
The use of the induction hypothesis on D and F in a paper proof corresponds to the recursive call to unique. To appeal to the induction hypothesis, we need to extend the context by pairing up x and the typing assumption hastype x T[]. This is accomplished by creating the declaration b: block x:term, u:hastype x T[]. In the code, we wrote an underscore _ instead of T[], which tells Beluga to reconstruct it since we cannot write T[] there without binding it by explicitly giving the type of D. To retrieve x we take the first projection b.x, and to retrieve x’s typing assumption we take the second projection b.u.
Now we can appeal to the induction hypothesis using D1[.., b.x, b.u] and F1[.., b.x, b.u] in the context g,b: block x:term, u:hastype x S[]. From the i.h. we get a contextual object, a closed derivation of [|- eq (arr T T') (arr S S’)]. The only rule that could derive this is ref, and pattern matching establishes that S must equal S’, since we must have arr T S = arr T1 S’. Therefore, there is a proof of [ |- equal S S’], and we can finish with the reflexivity rule e_ref.
tm and assumptions hastype x T[], we pattern match on [g |- #p.2], i.e., we project out the second argument of the block. By the given assumptions, we know that [g |- #p.2] has type [g |- hastype #p.1 T[]], because #p has type [g |- block x:tm , u:hastype x T[]]. We also know that the second input, called f, to the function unique has type [g |- hastype #p.1 T'[]]. By inversion on f, we know that the only possible object that can inhabit this type is [g |- #p.2] and therefore T' must be identical to T. Moreover, #r denotes the same block as #p.phi, context psi, and a substitution #S that maps variables from phi to the context psi, formally #S:[psi |- phi] as follows:}}%
+
inductive Ctx_xaR : {phi:xG} {psi: xaG} {#S:[psi |- phi]} ctype =
| Nil_xa : Ctx_xaR [] [] [ |- ^ ]
-| Cons_xa : Ctx_xaR [phi] [psi] [psi |- #S[..] ]
- -> Ctx_xaR [phi, x:tm] [psi, b: block (x:tm,u:aeq x x)] [ psi, b |- #S[..],b.1 ]
+| Cons_xa : Ctx_xaR [phi] [psi] [psi |- #S ]
+ -> Ctx_xaR [phi, x:tm] [psi, b: block (x:tm,u:aeq x x)] [ psi, b |- #S[..] ,b.1 ]
;
-%{{The first-class substitution variable #S has domain phi and range psi. If #S relates contexts phi and psi, then the substitution #S b.1 relates phi, x:tm to psi, b:block (x:tm,u:aeq x x) via constructor Cons_xaR.}}%
+%{{The first-class substitution variable #S has domain phi and range psi. If #S relates contexts phi and psi, then the substitution #S, b.1 relates phi, x:tm to psi, b:block (x:tm,u:aeq x x) via constructor Cons_xaR.}}%
inductive EqV : {phi:xG}{psi:xaG}{#S:[psi |- phi]} [phi |- tm] -> [psi |- tm] -> ctype =
| EqV_v: EqV [phi, x:tm] [psi, b: block (x:tm,u:aeq x x)] [ psi, b:block (x:tm, u:aeq x x) |- #S[..],b.1 ]
[phi, x:tm |- x]
[psi, b:block (x:tm, u:aeq x x) |- b.1 ]
-| EqV_p : EqV [phi] [psi] [psi |- #S[..] ] [phi |- #p[..]][psi |- #q.1[..]]
+| EqV_p : EqV [phi] [psi] [psi |- #S ] [phi |- #p][psi |- #q.1]
-> EqV [phi, x:tm] [psi, b: block (x:tm,u:aeq x x)] [ psi, b |- #S[..],b.1 ]
[phi, x:tm |- #p[..]] [psi, b:block (x:tm, u:aeq x x) |- #q.1[..] ]
;
inductive Eq : {phi:xG}{psi:xaG}{#S:[psi |- phi]} [phi |- tm] -> [psi |- tm] -> ctype =
-| Eq_v: EqV [phi] [psi] [psi |- #S[..]] [phi |- #p[..] ] [psi |- #q.1[..]]
- -> Eq [phi] [psi] [psi |- #S[..]] [phi |- #p[..] ] [psi |- #q.1[..]]
+| Eq_v: EqV [phi] [psi] [psi |- #S] [phi |- #p ] [psi |- #q.1]
+ -> Eq [phi] [psi] [psi |- #S] [phi |- #p ] [psi |- #q.1]
| Eq_a:
- Eq [phi] [psi] [psi |- #S[..] ] [phi |- M[..]] [psi |- M'[..]] ->
- Eq [phi] [psi] [psi |- #S[..] ] [phi |- N[..]] [psi |- N'[..]] ->
- Eq [phi] [psi] [psi |- #S[..] ] [phi |- app (M[..]) (N[..])] [psi |- app (M'[..]) (N'[..])]
+ Eq [phi] [psi] [psi |- #S ] [phi |- M] [psi |- M'] ->
+ Eq [phi] [psi] [psi |- #S ] [phi |- N] [psi |- N'] ->
+ Eq [phi] [psi] [psi |- #S ] [phi |- app M N] [psi |- app M' N']
| Eq_l :
Eq [phi,x:tm] [psi,b:block (x:tm, u:aeq x x)] [psi, b:block (x:tm, u:aeq x x) |- #S[..],b.1]
[phi,x:tm |- M] [psi, b:block (x:tm, u:aeq x x) |- M'[..,b.1]]
- -> Eq [phi] [psi] [psi |- #S[..] ]
+ -> Eq [phi] [psi] [psi |- #S ]
[phi |- lam \x. M] [psi |- lam \x. M']
;
%{{
refl of type {phi:xG}{M: [phi |- tm]} Ctx_xaR [phi] [psi] [ psi |- #S[..] ] -> [psi |- aeq (M #S[..]) (M #S[..])]: for all contexts phi and psi that have schema xG and xaG, respectively, if we have a substitution #S s.t. #S:[psi |- phi] then for all terms M depending on phi, we have a proof that [ psi |- aeq (#p #S[..]) (#p #S[..])]." Since the term M depends only on the context phi, it is explicitly weakened through applying #S to move it to the context psi.}}%
+The recursive function refl of type {phi:xG}{M: [phi |- tm]} Ctx_xaR [phi] [psi] [ psi |- #S ] -> [psi |- aeq (M #S) (M #S)]: for all contexts phi and psi that have schema xG and xaG, respectively, if we have a substitution #S s.t. #S:[psi |- phi] then for all terms M depending on phi, we have a proof that [ psi |- aeq (#p #S) (#p #S)]." Since the term M depends only on the context phi, it is explicitly weakened through applying #S to move it to the context psi.}}%
rec ctx_membership :
{#p: [phi |- tm] }
- Ctx_xaR [phi] [psi] [ psi |- #S[..] ] ->
+ Ctx_xaR [phi] [psi] [ psi |- #S ] ->
[psi |- aeq #p[#S] #p[#S]] =
-mlam #p => fn cr => let (cr : Ctx_xaR [phi] [psi] [ psi |- #S[..] ]) = cr in
-case [phi |- #p[..]] of
+mlam #p => fn cr => let (cr : Ctx_xaR [phi] [psi] [ psi |- #S ]) = cr in
+case [phi |- #p] of
| [phi, x:tm |- x] =>
let Cons_xa cr' = cr in
- let (cr' : Ctx_xaR [phi] [psi] [ psi |- #S[..] ]) = cr' in
+ let (cr' : Ctx_xaR [phi] [psi] [ psi |- #S ]) = cr' in
[psi, b: block (x:tm, u:aeq x x) |- b.2]
| [phi, x:tm |- #p[..]] =>
let Cons_xa cr' = cr in
- let [psi |- E[..]] = ctx_membership [phi |- #p] cr' in
+ let [psi |- E] = ctx_membership [phi |- #p] cr' in
[psi, b: block (x:tm,u:aeq x x) |- E[..] ]
;
% Compact version
rec refl : {phi:xG}{M: [phi |- tm]}
- Ctx_xaR [phi] [psi] [ psi |- #S[..] ] ->
+ Ctx_xaR [phi] [psi] [ psi |- #S ] ->
[psi |- aeq M[#S] M[#S]] =
-mlam phi => mlam M => fn cr => case [phi |- M[..]] of
-| [phi |- #p[..]] => ctx_membership [phi |- #p] cr
+mlam phi => mlam M => fn cr => case [phi |- M] of
+| [phi |- #p] => ctx_membership [phi |- #p] cr
-| [phi |- app (M[..] ) (N[..])] =>
- let [psi |- D1[..] ] = refl [phi] [phi |- M[..]] cr in
- let [psi |- D2[..] ] = refl [phi] [phi |- N[..]] cr in
- [psi |- ae_a (D1[..]) (D2[..]) ]
+| [phi |- app (M ) N] =>
+ let [psi |- D1 ] = refl [phi] [phi |- M] cr in
+ let [psi |- D2 ] = refl [phi] [phi |- N] cr in
+ [psi |- ae_a D1 D2 ]
| [phi |- lam \x.M] =>
@@ -105,51 +107,51 @@ mlam phi => mlam M => fn cr => case [phi |- M[..]] of
[psi |- ae_l \x.\u. D]
;
-%{{In the application case, we appeal to the induction hypothesis on [phi |- M1[..]] and [ |- M2 ::] through a recursive call. Since the context phi and the context psi do not change, we can simply make the recursive all on [phi |- M1 ::] and [phi |- M2 ::] respectively using the relation cr.
+%{{In the application case, we appeal to the induction hypothesis on [phi |- M] and [ |- N] through a recursive call. Since the context phi and the context psi do not change, we can simply make the recursive all on [phi |- M] and [phi |- M] respectively using the relation cr.
[phi |- lam \x.M :: x], we want to appeal to the induction hypothesis on [phi |- x:tm. M ::x]. In this instance, we also need a witness relating the context [phi |- x:tm. M ::x] to the context [psi, b:block (x:tm,u:aeq x x)]. Recall that cr stands for Ctx_xaR [phi] [psi] [psi |- #S]. Therefore, by Cons_xa, we know there exists Ctx_xaR [phi ,x:tm] [psi ,b:block (x:tm,u:aeq x x)] [psi, b |- #S b.1] and we appeal to the induction hypothesis by reflR [phi,x:tm] [phi,x:tm.M ::x] (Cons_xa cr).
+When we have [phi |- lam \x.M ], we want to appeal to the induction hypothesis on [phi, x:tm |- M]. In this instance, we also need a witness relating the context [phi, x:tm |- M] to the context [psi, b:block (x:tm,u:aeq x x)]. Recall that cr stands for Ctx_xaR [phi] [psi] [psi |- #S]. Therefore, by Cons_xa, we know there exists Ctx_xaR [phi ,x:tm] [psi ,b:block (x:tm,u:aeq x x)] [psi, b |- #S, b.1] and we appeal to the induction hypothesis by reflR [phi,x:tm] [phi,x:tm.M] (Cons_xa cr).
phi. If [phi,x:tm |- x], then we inspect the context relation cr. Pattern matching forces the original context phi to be phi,x:tm. By pattern matching on cr', we observe that there exists a relation cr', s.t. Ctx_xaR [phi] [psi] [psi |- #S]. Moreover, psi = psi,b:block (x:tm,u:aeq x x) and #S = #S b.1 where the left hand side denotes the original context and substitution, while the right hand side shows the context and substitution refinement after pattern matching. We must show that there exists a proof for aeq x x in the context psi, b:block (x:tm,u:aeq x x). This is simply b.2.}}%
+Finally, we take a close look at the variable case. We distinguish two different cases depending on the position of the variable in the context by pattern matching on the shape of phi. If [phi,x:tm |- x], then we inspect the context relation cr. Pattern matching forces the original context phi to be phi,x:tm. By pattern matching on cr', we observe that there exists a relation cr', s.t. Ctx_xaR [phi] [psi] [psi |- #S]. Moreover, psi = psi,b:block (x:tm,u:aeq x x) and #S = #S, b.1 where the left hand side denotes the original context and substitution, while the right hand side shows the context and substitution refinement after pattern matching. We must show that there exists a proof for aeq x x in the context psi, b:block (x:tm,u:aeq x x). This is simply b.2.}}%
%{{M and M #S[..]. Since we cannot pattern match directly on M #S[..] (because #S is a general substitution and we do not enforce on the type-level that it is a variable-variable substitution) we cannot use unification to solve equations; If #S would be known to be a pattern substitution, then we could solve equations such as M #S[..] = app (M1[..]) (M2[..]); we hence encode such equalities explicitly.
+Following we generalize reasoning about terms which contain substitution variables, reasoning explicitly about equality between terms M and M[#S]. Since we cannot pattern match directly on M[#S] (because #S is a general substitution and we do not enforce on the type-level that it is a variable-variable substitution) we cannot use unification to solve equations; If #S would be known to be a pattern substitution, then we could solve equations such as M[#S] = app M1 M2; we hence encode such equalities explicitly.
reflG of type {g:xaG}{M:[g |- tm ]}[g |- aeq (M[..])(M[..])]: for all contexts g that have schema xaG, for all terms M, we have a proof that [g |- 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: {g:xaG} {M:[g |- tm]} [g |- aeq (M[..]) (M[..])] =
-mlam g => mlam M => case [g |- (M[..])] of
-| [g |- #p.1[..]] => [g |- #p.2[..]]
-| [g |- lam \x. M] =>
- let [g,b:block y:tm, ae_v:aeq y y |- D[..,b.1,b.2]] =
- reflG [g, b:block y:tm, ae_v:aeq y y] [g, b |- M[..,b.1]]
+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
- [g |- ae_l \x. \w. D] % : eq (L) (L)
-| [g |- app (M1[..]) (M2[..])] =>
- let [g |- D1[..]] = reflG [g] [g |- M1[..] ] in
- let [g |- D2[..]] = reflG [g] [g |- M2[..] ] in
- [g |- ae_a (D1[..]) (D2[..])]
+ [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 [g |- M[..]] using pattern matching. There are three possible cases for M:
+%{{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:
M is a variable from g, we write [g |- #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.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.M is an application, we appeal twice to the induction hypothesis and build a proof for [g |- aeq (app (M1[..]) (M2[..])) (app (M1[..]) (M2[..]))].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.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.M is an application, we appeal twice to the induction hypothesis and build a proof for [gamma |- aeq (app M1 M2) (app M1 M2)].[g |- aeq (M[..]) (L[..])] to arrive at the second [g |- 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: (g:xaG)
- [g |- aeq (M[..]) (L[..])] -> [g |- aeq (L[..]) (N[..])]
- -> [g |- aeq (M[..]) (N[..])] =
+Next, we prove admissibility of transitivity. We encode the proof of transitivity by pattern-matching on the first derivation [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
-| [g |- #p.2[..]] => d2
-| [g |- ae_l \x.\u. D1] =>
- let [g |- ae_l \x.\u. D2] = d2 in
- let [g, b:block x:tm, ae_v:aeq x x |- E[..,b.1,b.2]] =
- transG [g, b:block x':tm, ae_v:aeq x' x' |- D1[..,b.1,b.2]]
- [g, b |- D2[..,b.1,b.2]]
+| [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
- [g |- ae_l \x. \u. E]
-| [g |- ae_a (D1[..]) (D2[..])] =>
- let [g |- ae_a (F1[..]) (F2[..])] = d2 in
- let [g |- E1[..]] = transG [g |- D1[..]] [g |- F1[..]] in
- let [g |- E2[..]] = transG [g |- D2[..]] [g |- F2[..]] in
- [g |- ae_a (E1[..]) (E2[..])]
+ [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.}}%
@@ -112,19 +112,19 @@ fn d1 => fn d2 => case d1 of
## 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: (g:xaG)
- [g |- aeq (M[..]) (L[..])] -> [g |- aeq (L[..]) (M[..])] =
+rec symG: (gamma:xaG)
+ [gamma |- aeq M L] -> [gamma |- aeq L M] =
fn d => case d of
-| [g |- #p.2[..]] => d
-| [g |- ae_l \x.\u. D1] =>
- let [g, b:block x:tm, ae_v:aeq x x |- E[..,b.1,b.2]] =
- symG [g, b:block x':tm, ae_v:aeq x' x' |- D1[..,b.1,b.2]]
+| [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
- [g |- ae_l \x. \u. E]
-| [g |- ae_a (D1[..]) (D2[..])] =>
- let [g |- E1[..]] = symG [g |- D1[..]] in
- let [g |- E2[..]] = symG [g |- D2[..]] in
- [g |- ae_a (E1[..]) (E2[..])]
+ [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]
;
% ---------------------------------------------------------------------------
@@ -132,31 +132,31 @@ fn d => case d of
## Proof of Completeness
Finally, we implement the completeness proof as as a recursive function ceqG.
}}%
-rec ceq: (g:daG) [g |- deq (M[..]) (N[..])] -> [g |- aeq (M[..]) (N[..])] =
+rec ceq: (gamma:daG) [gamma |- deq M N] -> [gamma |- aeq M N] =
fn e => case e of
-| [g |- #p.3[..]] => [g |- #p.2[..]]
-| [g |- de_r] => reflG [g] [g |- _ ]
-| [g |- de_a (D1[..]) (D2[..])] =>
- let [g |- F1[..]] = ceq [g |- D1[..]] in
- let [g |- F2[..]] = ceq [g |- D2[..]] in
- [g |- ae_a (F1[..]) (F2[..])]
-| [g |- de_l (\x.(\u. D))] =>
- let [g,b:block x:tm, _t:aeq x x, u:deq x x |- F[..,b.1,b.2]] =
- ceq [g, b:block x:tm, _t:aeq x x, u:deq x x |- D[..,b.1,b.3]]
+| [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
- [g |- ae_l (\x.\v. F)]
-| [g |- de_t (D1[..]) (D2[..])] =>
- let [g |- F2[..]] = ceq [g |- D2[..]] in
- let [g |- F1[..]] = ceq [g |- D1[..]] in
- transG [g |- F1[..]] [g |- F2[..]]
-| [g |- de_s (D[..])] =>
- let [g |- F[..]] = ceq [g |- D[..]] in
- symG [g |- F[..]]
+ [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[..].
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 [g, 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 [g, 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 g, 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 v).
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.