Library MetaCoq.PCUIC.PCUICUnivSubst
Universe substitution
Instance subst_instance_constr : UnivSubst term :=
fix subst_instance_constr u c {struct c} : term :=
match c with
| tRel _ | tVar _ ⇒ c
| tEvar ev args ⇒ tEvar ev (List.map (subst_instance_constr u) args)
| tSort s ⇒ tSort (subst_instance_univ u s)
| tConst c u' ⇒ tConst c (subst_instance_instance u u')
| tInd i u' ⇒ tInd i (subst_instance_instance u u')
| tConstruct ind k u' ⇒ tConstruct ind k (subst_instance_instance u u')
| tLambda na T M ⇒ tLambda na (subst_instance_constr u T) (subst_instance_constr u M)
| tApp f v ⇒ tApp (subst_instance_constr u f) (subst_instance_constr u v)
| tProd na A B ⇒ tProd na (subst_instance_constr u A) (subst_instance_constr u B)
| tLetIn na b ty b' ⇒ tLetIn na (subst_instance_constr u b) (subst_instance_constr u ty)
(subst_instance_constr u b')
| tCase ind p c brs ⇒
let brs' := List.map (on_snd (subst_instance_constr u)) brs in
tCase ind (subst_instance_constr u p) (subst_instance_constr u c) brs'
| tProj p c ⇒ tProj p (subst_instance_constr u c)
| tFix mfix idx ⇒
let mfix' := List.map (map_def (subst_instance_constr u) (subst_instance_constr u)) mfix in
tFix mfix' idx
| tCoFix mfix idx ⇒
let mfix' := List.map (map_def (subst_instance_constr u) (subst_instance_constr u)) mfix in
tCoFix mfix' idx
end.
Instance subst_instance_decl : UnivSubst context_decl
:= map_decl ∘ subst_instance_constr.
Instance subst_instance_context : UnivSubst context
:= map_context ∘ subst_instance_constr.
Lemma lift_subst_instance_constr u c n k :
lift n k (subst_instance_constr u c) = subst_instance_constr u (lift n k c).
Lemma subst_instance_constr_mkApps u f a :
subst_instance_constr u (mkApps f a) =
mkApps (subst_instance_constr u f) (map (subst_instance_constr u) a).
Lemma subst_instance_constr_it_mkProd_or_LetIn u ctx t :
subst_instance_constr u (it_mkProd_or_LetIn ctx t) =
it_mkProd_or_LetIn (subst_instance_context u ctx) (subst_instance_constr u t).
Lemma subst_instance_context_length u ctx
: #|subst_instance_context u ctx| = #|ctx|.
Lemma subst_subst_instance_constr u c N k :
subst (map (subst_instance_constr u) N) k (subst_instance_constr u c)
= subst_instance_constr u (subst N k c).
Lemma map_subst_instance_constr_to_extended_list_k u ctx k :
map (subst_instance_constr u) (to_extended_list_k ctx k)
= to_extended_list_k ctx k.
Section Closedu.
Tests that the term is closed over k universe variables
Context (k : nat).
Definition closedu_level (l : Level.t) :=
match l with
| Level.Var n ⇒ n <? k
| _ ⇒ true
end.
Definition closedu_level_expr (s : Universe.Expr.t) :=
closedu_level (fst s).
Definition closedu_universe (u : universe) :=
forallb closedu_level_expr u.
Definition closedu_instance (u : universe_instance) :=
forallb closedu_level u.
Fixpoint closedu (t : term) : bool :=
match t with
| tSort univ ⇒ closedu_universe univ
| tInd _ u ⇒ closedu_instance u
| tConstruct _ _ u ⇒ closedu_instance u
| tConst _ u ⇒ closedu_instance u
| tRel i ⇒ true
| tEvar ev args ⇒ forallb closedu args
| tLambda _ T M | tProd _ T M ⇒ closedu T && closedu M
| tApp u v ⇒ closedu u && closedu v
| tLetIn na b t b' ⇒ closedu b && closedu t && closedu b'
| tCase ind p c brs ⇒
let brs' := forallb (test_snd (closedu)) brs in
closedu p && closedu c && brs'
| tProj p c ⇒ closedu c
| tFix mfix idx ⇒
forallb (test_def closedu closedu ) mfix
| tCoFix mfix idx ⇒
forallb (test_def closedu closedu) mfix
| x ⇒ true
end.
End Closedu.
Definition closedu_level (l : Level.t) :=
match l with
| Level.Var n ⇒ n <? k
| _ ⇒ true
end.
Definition closedu_level_expr (s : Universe.Expr.t) :=
closedu_level (fst s).
Definition closedu_universe (u : universe) :=
forallb closedu_level_expr u.
Definition closedu_instance (u : universe_instance) :=
forallb closedu_level u.
Fixpoint closedu (t : term) : bool :=
match t with
| tSort univ ⇒ closedu_universe univ
| tInd _ u ⇒ closedu_instance u
| tConstruct _ _ u ⇒ closedu_instance u
| tConst _ u ⇒ closedu_instance u
| tRel i ⇒ true
| tEvar ev args ⇒ forallb closedu args
| tLambda _ T M | tProd _ T M ⇒ closedu T && closedu M
| tApp u v ⇒ closedu u && closedu v
| tLetIn na b t b' ⇒ closedu b && closedu t && closedu b'
| tCase ind p c brs ⇒
let brs' := forallb (test_snd (closedu)) brs in
closedu p && closedu c && brs'
| tProj p c ⇒ closedu c
| tFix mfix idx ⇒
forallb (test_def closedu closedu ) mfix
| tCoFix mfix idx ⇒
forallb (test_def closedu closedu) mfix
| x ⇒ true
end.
End Closedu.
Universe-closed terms are unaffected by universe substitution.
Section UniverseClosedSubst.
Lemma closedu_subst_instance_level u t : closedu_level 0 t → subst_instance_level u t = t.
Lemma closedu_subst_instance_level_expr u t : closedu_level_expr 0 t → subst_instance_level_expr u t = t.
Lemma closedu_subst_instance_univ u t : closedu_universe 0 t → subst_instance_univ u t = t.
Lemma closedu_subst_instance_instance u t : closedu_instance 0 t → subst_instance_instance u t = t.
Lemma closedu_subst_instance_constr u t : closedu 0 t → subst_instance_constr u t = t.
End UniverseClosedSubst.
Section SubstInstanceClosed.
Substitution of a universe-closed instance of the right size
produces a universe-closed term.
Context (u : universe_instance) (Hcl : closedu_instance 0 u).
Lemma subst_instance_level_closedu t :
closedu_level #|u| t → closedu_level 0 (subst_instance_level u t).
Lemma subst_instance_level_expr_closedu t :
closedu_level_expr #|u| t
→ closedu_level_expr 0 (subst_instance_level_expr u t).
Lemma subst_instance_univ_closedu t :
closedu_universe #|u| t → closedu_universe 0 (subst_instance_univ u t).
Lemma subst_instance_instance_closedu t :
closedu_instance #|u| t → closedu_instance 0 (subst_instance_instance u t).
Lemma subst_instance_constr_closedu t :
closedu #|u| t → closedu 0 (subst_instance_constr u t).
End SubstInstanceClosed.