Hello,
I would like to know the MetaCoq equivalent of the "weakening" rule in Coq, i.e. the rule W-Local-Assum
in
https://coq.inria.fr/refman/language/cic.html
I fail to recognize it in the inductive typing
or even in the file Typing.v
.
Weakening is a theorem in MetaCoq, not a typing rule.
There is a weakening operation lift
defined in https://github.com/MetaCoq/metacoq/blob/coq-8.11/template-coq/theories/LiftSubst.v.
You can find the weakening theorem here, it is found in the checker
folder for Template-Coq.
A simpler to read corollary is found here.
Lemma weakening `{cf : checker_flags} Σ Γ Γ' (t : term) T :
wf Σ.1 -> wf_local Σ (Γ ,,, Γ') ->
Σ ;;; Γ |- t : T ->
Σ ;;; Γ ,,, Γ' |- lift0 #|Γ'| t : lift0 #|Γ'| T.
thanks Théo !
Herein lift0 k
adds k
to all variables (while taking proper care of binders it would encounter), so if you add k variables at the end of your context, it still has the same type.
Last updated: Oct 13 2024 at 01:02 UTC