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: Feb 09 2023 at 02:02 UTC