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?