Stream: MetaCoq

Topic: New local assumption / weakening

Pierre Vial (Jul 06 2020 at 07:28):

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.

Théo Winterhalter (Jul 06 2020 at 07:32):

Weakening is a theorem in MetaCoq, not a typing rule.

Théo Winterhalter (Jul 06 2020 at 07:32):

There is a weakening operation lift defined in https://github.com/MetaCoq/metacoq/blob/coq-8.11/template-coq/theories/LiftSubst.v.

Théo Winterhalter (Jul 06 2020 at 07:34):

You can find the weakening theorem here, it is found in the checker folder for Template-Coq.

Théo Winterhalter (Jul 06 2020 at 07:35):

A simpler to read corollary is found here.

Théo Winterhalter (Jul 06 2020 at 07:35):

Lemma weakening `{cf : checker_flags} Σ Γ Γ' (t : term) T :
  wf Σ.1 -> wf_local Σ (Γ ,,, Γ') ->
  Σ ;;; Γ |- t : T ->
  Σ ;;; Γ ,,, Γ' |- lift0 #|Γ'| t : lift0 #|Γ'| T.

Pierre Vial (Jul 06 2020 at 07:36):

thanks Théo !

Théo Winterhalter (Jul 06 2020 at 07:36):

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: Apr 18 2024 at 06:01 UTC