<p>If you intend to formalize meta-theorems in a proof assistant, then it's probably better to avoid the general weakening rule because it will pollute all your inductive arguments. Every single induction on the derivation will contain the case &quot;but what if the context got larger using weakening?&quot; and that's going to be super annoying. I would recommend instead a sane variable rule and no weakening. You can always show that weaking is admissible.</p>
<p>As far as sane variable rules go, the one you quoted works well when variables are symbols and contexts are maps taking symbols to their types. If you indent to use de Bruijn indices, then you should use different variable rules (note that contexts are just lists of types because variable names are just natural numbers):
<span class="math-container">$$
\frac{ }{\Gamma, A \vdash \mathtt{var}_0 : A}
\qquad
\frac{\Gamma \vdash \mathtt{var}_k : B}{\Gamma, A \vdash \mathtt{var}_{\mathtt{succ}(k)} : B}$$</span></p>

CC BY-SA 4.0
2021-01-14T15:11:40.147Z
2021-01-14T15:11:40.147Z
Andrej Bauer
<p>I'm trying to formalize the syntax and typing judgments of the Calculus of Constructions in Coq. I'm choosing to use the Pure Type Systems presentation of CoC; however, I've seen mild variations in the rules for PTS in different resources.</p>
<p>In <em>Type Theory and Formal Proof: An Introduction</em>, Nederpelt and Geuvers add context weakening as an explicit rule:</p>
<pre><code>Γ ⊢ e : T     
x \notin Γ
Γ ⊢ U : s
---------------------- t_weak
Γ, x : U ⊢ e : T

---------------------- t_var
Γ, x : T ⊢ x : T
</code></pre>
<p>Their formalization clearly requires <code>t_weak</code>, since <code>t_var</code> can only type the last variable in the context.</p>
<p>In ATAPL, Pierce instead chooses a more powerful rule for typing variables, and forgoes an explicit context weakening rule.</p>
<pre><code>x : T \in Γ
----------- t_var'
Γ ⊢ x : T
</code></pre>
<p>Presumably, one would be able to derive a weakening rule from the rules Pierce chooses.</p>
<p>Are both these systems indeed equivalent? Is there any reason to choose one over the other for the sake of formalization in a proof assistant?</p>

<type-theory><calculus-of-constructions>
Context weakening as an explicit rule for languages of the the lambda cube?
NJay
# Context weakening as an explicit rule for languages of the the lambda cube?

(Asked by: username_0 on 2021-01-14)

I'm trying to formalize the syntax and typing judgments of the Calculus of Constructions in Coq. I'm choosing to use the Pure Type Systems presentation of CoC; however, I've seen mild variations in the rules for PTS in different resources.
In Type Theory and Formal Proof: An Introduction, Nederpelt and Geuvers add context weakening as an explicit rule:
Γ ⊢ e : T     
x \notin Γ
Γ ⊢ U : s
---------------------- t_weak
Γ, x : U ⊢ e : T

---------------------- t_var
Γ, x : T ⊢ x : T

Their formalization clearly requires t_weak, since t_var can only type the last variable in the context.
In ATAPL, Pierce instead chooses a more powerful rule for typing variables, and forgoes an explicit context weakening rule.
x : T \in Γ
----------- t_var'
Γ ⊢ x : T

Presumably, one would be able to derive a weakening rule from the rules Pierce chooses.
Are both these systems indeed equivalent? Is there any reason to choose one over the other for the sake of formalization in a proof assistant?

**Tags:** type-theory, calculus-of-constructions


---

## 1 answers

### Answer by username_1 on 2021-01-14. Score: 4 | Accepted answer

If you intend to formalize meta-theorems in a proof assistant, then it's probably better to avoid the general weakening rule because it will pollute all your inductive arguments. Every single induction on the derivation will contain the case "but what if the context got larger using weakening?" and that's going to be super annoying. I would recommend instead a sane variable rule and no weakening. You can always show that weaking is admissible.

As far as sane variable rules go, the one you quoted works well when variables are symbols and contexts are maps taking symbols to their types. If you indent to use de Bruijn indices, then you should use different variable rules (note that contexts are just lists of types because variable names are just natural numbers):
$$
\frac{ }{\Gamma, A \vdash \mathtt{var}\_0 : A}
\qquad
\frac{\Gamma \vdash \mathtt{var}\_k : B}{\Gamma, A \vdash \mathtt{var}\_{\mathtt{succ}(k)} : B}$$


---

