Library MetaCoq.Template.LiftSubst
Lifting and substitution for the AST
Fixpoint lift n k t : term :=
match t with
| tRel i ⇒ if Nat.leb k i then tRel (n + i) else tRel i
| tEvar ev args ⇒ tEvar ev (List.map (lift n k) args)
| tLambda na T M ⇒ tLambda na (lift n k T) (lift n (S k) M)
| tApp u v ⇒ tApp (lift n k u) (List.map (lift n k) v)
| tProd na A B ⇒ tProd na (lift n k A) (lift n (S k) B)
| tCast c kind t ⇒ tCast (lift n k c) kind (lift n k t)
| tLetIn na b t b' ⇒ tLetIn na (lift n k b) (lift n k t) (lift n (S k) b')
| tCase ind p c brs ⇒
let brs' := List.map (on_snd (lift n k)) brs in
tCase ind (lift n k p) (lift n k c) brs'
| tProj p c ⇒ tProj p (lift n k c)
| tFix mfix idx ⇒
let k' := List.length mfix + k in
let mfix' := List.map (map_def (lift n k) (lift n k')) mfix in
tFix mfix' idx
| tCoFix mfix idx ⇒
let k' := List.length mfix + k in
let mfix' := List.map (map_def (lift n k) (lift n k')) mfix in
tCoFix mfix' idx
| x ⇒ x
end.
Notation lift0 n := (lift n 0).
Definition up := lift 1 0.
Parallel substitution: it assumes that all terms in the substitution live in the
same context
Fixpoint subst s k u :=
match u with
| tRel n ⇒
if Nat.leb k n then
match nth_error s (n - k) with
| Some b ⇒ lift0 k b
| None ⇒ tRel (n - List.length s)
end
else tRel n
| tEvar ev args ⇒ tEvar ev (List.map (subst s k) args)
| tLambda na T M ⇒ tLambda na (subst s k T) (subst s (S k) M)
| tApp u v ⇒ mkApps (subst s k u) (List.map (subst s k) v)
| tProd na A B ⇒ tProd na (subst s k A) (subst s (S k) B)
| tCast c kind ty ⇒ tCast (subst s k c) kind (subst s k ty)
| tLetIn na b ty b' ⇒ tLetIn na (subst s k b) (subst s k ty) (subst s (S k) b')
| tCase ind p c brs ⇒
let brs' := List.map (on_snd (subst s k)) brs in
tCase ind (subst s k p) (subst s k c) brs'
| tProj p c ⇒ tProj p (subst s k c)
| tFix mfix idx ⇒
let k' := List.length mfix + k in
let mfix' := List.map (map_def (subst s k) (subst s k')) mfix in
tFix mfix' idx
| tCoFix mfix idx ⇒
let k' := List.length mfix + k in
let mfix' := List.map (map_def (subst s k) (subst s k')) mfix in
tCoFix mfix' idx
| x ⇒ x
end.
Notation subst0 t := (subst t 0).
Definition subst1 t k u := subst [t] k u.
Notation subst10 t := (subst1 t 0).
Notation "M { j := N }" := (subst1 N j M) (at level 10, right associativity).
Fixpoint closedn k (t : term) : bool :=
match t with
| tRel i ⇒ Nat.ltb i k
| tEvar ev args ⇒ List.forallb (closedn k) args
| tLambda _ T M | tProd _ T M ⇒ closedn k T && closedn (S k) M
| tApp u v ⇒ closedn k u && List.forallb (closedn k) v
| tCast c kind t ⇒ closedn k c && closedn k t
| tLetIn na b t b' ⇒ closedn k b && closedn k t && closedn (S k) b'
| tCase ind p c brs ⇒
let brs' := List.forallb (test_snd (closedn k)) brs in
closedn k p && closedn k c && brs'
| tProj p c ⇒ closedn k c
| tFix mfix idx ⇒
let k' := List.length mfix + k in
List.forallb (test_def (closedn k) (closedn k')) mfix
| tCoFix mfix idx ⇒
let k' := List.length mfix + k in
List.forallb (test_def (closedn k) (closedn k')) mfix
| x ⇒ true
end.
Notation closed t := (closedn 0 t).
Notation subst_rec N M k := (subst N k M) (only parsing).
Lemma lift_rel_ge :
∀ k n p, p ≤ n → lift k p (tRel n) = tRel (k + n).
Lemma lift_rel_lt : ∀ k n p, p > n → lift k p (tRel n) = tRel n.
Lemma lift_rel_alt : ∀ n k i, lift n k (tRel i) = tRel (if Nat.leb k i then n + i else i).
Lemma subst_rel_lt : ∀ u n k, k > n → subst u k (tRel n) = tRel n.
Lemma subst_rel_gt :
∀ u n k, n ≥ k + length u → subst u k (tRel n) = tRel (n - length u).
Lemma subst_rel_eq :
∀ (u : list term) n i t p,
List.nth_error u i = Some t → p = n + i →
subst u n (tRel p) = lift0 n t.
Lemma on_snd_eq_id_spec {A B} (f : B → B) (x : A × B) :
f (snd x) = snd x ↔
on_snd f x = x.
Lemma map_def_eq_spec {A B : Set} (f f' g g' : A → B) (x : def A) :
f (dtype x) = g (dtype x) →
f' (dbody x) = g' (dbody x) →
map_def f f' x = map_def g g' x.
Lemma map_def_id_spec {A : Set} (f f' : A → A) (x : def A) :
f (dtype x) = (dtype x) →
f' (dbody x) = (dbody x) →
map_def f f' x = x.
Lemma lift0_id : ∀ M k, lift 0 k M = M.
Lemma lift0_p : ∀ M, lift0 0 M = M.
Lemma simpl_lift :
∀ M n k p i,
i ≤ k + n →
k ≤ i → lift p i (lift n k M) = lift (p + n) k M.
Lemma simpl_lift0 : ∀ M n, lift0 (S n) M = lift0 1 (lift0 n M).
Lemma permute_lift :
∀ M n k p i,
i ≤ k →
lift p i (lift n k M) = lift n (k + p) (lift p i M).
Lemma permute_lift0 :
∀ M k, lift0 1 (lift 1 k M) = lift 1 (S k) (lift0 1 M).
Lemma lift_isApp n k t : isApp t = false → isApp (lift n k t) = false.
Lemma map_non_nil {A B} (f : A → B) l : l ≠ nil → map f l ≠ nil.
Lemma isLambda_lift n k (bod : term) :
isLambda bod = true → isLambda (lift n k bod) = true.
Lemma wf_lift n k t : wf t → wf (lift n k t).
Lemma mkApps_tApp t l :
isApp t = false → l ≠ nil → mkApps t l = tApp t l.
Lemma simpl_subst_rec :
∀ M (H : wf M) N n p k,
p ≤ n + k →
k ≤ p → subst N p (lift (List.length N + n) k M) = lift n k M.
Lemma simpl_subst :
∀ N M (H : wf M) n p, p ≤ n → subst N p (lift0 (length N + n) M) = lift0 n M.
Lemma mkApps_tRel n a l : mkApps (tRel n) (a :: l) = tApp (tRel n) (a :: l).
Lemma lift_mkApps n k t l : lift n k (mkApps t l) = mkApps (lift n k t) (map (lift n k) l).
Lemma commut_lift_subst_rec :
∀ M N n p k,
k ≤ p →
lift n k (subst N p M) = subst N (p + n) (lift n k M).
Lemma commut_lift_subst :
∀ M N k, subst N (S k) (lift0 1 M) = lift0 1 (subst N k M).
Lemma distr_lift_subst_rec :
∀ M N n p k,
lift n (p + k) (subst N p M) =
subst (List.map (lift n k) N) p (lift n (p + length N + k) M).
Lemma distr_lift_subst :
∀ M N n k,
lift n k (subst0 N M) = subst0 (map (lift n k) N) (lift n (length N + k) M).
Lemma distr_lift_subst10 :
∀ M N n k,
lift n k (subst10 N M) = subst10 (lift n k N) (lift n (S k) M).
Lemma subst_mkApps u k t l :
subst u k (mkApps t l) = mkApps (subst u k t) (map (subst u k) l).
Lemma subst1_mkApps u k t l : subst1 u k (mkApps t l) = mkApps (subst1 u k t) (map (subst1 u k) l).
Lemma distr_subst_rec :
∀ M N (P : list term) (wfP : All wf P) n p,
subst P (p + n) (subst N p M) =
subst (map (subst P n) N) p (subst P (p + length N + n) M).
Lemma distr_subst :
∀ P (wfP : All Ast.wf P) N M k,
subst P k (subst0 N M) = subst0 (map (subst P k) N) (subst P (length N + k) M).
Lemma lift_closed n k t : closedn k t → lift n k t = t.
Lemma closed_upwards {k t} k' : closedn k t → k' ≥ k → closedn k' t.
Lemma mkApps_mkApp u a v : mkApps (mkApp u a) v = mkApps u (a :: v).
Lemma wf_mkApp u a : wf u → wf a → wf (mkApp u a).
Lemma wf_mkApps u a : wf u → List.Forall wf a → wf (mkApps u a).
Lemma wf_subst ts k u : List.Forall wf ts → wf u → wf (subst ts k u).
Lemma wf_subst1 t k u : wf t → wf u → wf (subst1 t k u).
Lemma subst_empty k a : Ast.wf a → subst [] k a = a.
Lemma lift_to_extended_list_k Γ k : ∀ k',
to_extended_list_k Γ (k' + k) = map (lift0 k') (to_extended_list_k Γ k).
Lemma simpl_subst_k (N : list term) (M : term) :
Ast.wf M → ∀ k p, p = #|N| → subst N k (lift p k M) = M.
Lemma subst_app_decomp l l' k t :
Ast.wf t → Forall Ast.wf l →
subst (l ++ l') k t = subst l' k (subst (List.map (lift0 (length l')) l) k t).
Lemma subst_app_simpl l l' k t :
Ast.wf t → Forall Ast.wf l → Forall Ast.wf l' →
subst (l ++ l') k t = subst l k (subst l' (k + length l) t).
Lemma isLambda_subst (s : list term) k (bod : term) :
isLambda bod = true → isLambda (subst s k bod) = true.
Lemma map_vass_map_def g l n k :
(mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d)))
(map (map_def (lift n k) g) l)) =
(mapi (fun i d ⇒ map_decl (lift n (i + k)) d) (mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d))) l)).
Definition subst1 t k u := subst [t] k u.
Notation subst10 t := (subst1 t 0).
Notation "M { j := N }" := (subst1 N j M) (at level 10, right associativity).
Fixpoint closedn k (t : term) : bool :=
match t with
| tRel i ⇒ Nat.ltb i k
| tEvar ev args ⇒ List.forallb (closedn k) args
| tLambda _ T M | tProd _ T M ⇒ closedn k T && closedn (S k) M
| tApp u v ⇒ closedn k u && List.forallb (closedn k) v
| tCast c kind t ⇒ closedn k c && closedn k t
| tLetIn na b t b' ⇒ closedn k b && closedn k t && closedn (S k) b'
| tCase ind p c brs ⇒
let brs' := List.forallb (test_snd (closedn k)) brs in
closedn k p && closedn k c && brs'
| tProj p c ⇒ closedn k c
| tFix mfix idx ⇒
let k' := List.length mfix + k in
List.forallb (test_def (closedn k) (closedn k')) mfix
| tCoFix mfix idx ⇒
let k' := List.length mfix + k in
List.forallb (test_def (closedn k) (closedn k')) mfix
| x ⇒ true
end.
Notation closed t := (closedn 0 t).
Notation subst_rec N M k := (subst N k M) (only parsing).
Lemma lift_rel_ge :
∀ k n p, p ≤ n → lift k p (tRel n) = tRel (k + n).
Lemma lift_rel_lt : ∀ k n p, p > n → lift k p (tRel n) = tRel n.
Lemma lift_rel_alt : ∀ n k i, lift n k (tRel i) = tRel (if Nat.leb k i then n + i else i).
Lemma subst_rel_lt : ∀ u n k, k > n → subst u k (tRel n) = tRel n.
Lemma subst_rel_gt :
∀ u n k, n ≥ k + length u → subst u k (tRel n) = tRel (n - length u).
Lemma subst_rel_eq :
∀ (u : list term) n i t p,
List.nth_error u i = Some t → p = n + i →
subst u n (tRel p) = lift0 n t.
Lemma on_snd_eq_id_spec {A B} (f : B → B) (x : A × B) :
f (snd x) = snd x ↔
on_snd f x = x.
Lemma map_def_eq_spec {A B : Set} (f f' g g' : A → B) (x : def A) :
f (dtype x) = g (dtype x) →
f' (dbody x) = g' (dbody x) →
map_def f f' x = map_def g g' x.
Lemma map_def_id_spec {A : Set} (f f' : A → A) (x : def A) :
f (dtype x) = (dtype x) →
f' (dbody x) = (dbody x) →
map_def f f' x = x.
Lemma lift0_id : ∀ M k, lift 0 k M = M.
Lemma lift0_p : ∀ M, lift0 0 M = M.
Lemma simpl_lift :
∀ M n k p i,
i ≤ k + n →
k ≤ i → lift p i (lift n k M) = lift (p + n) k M.
Lemma simpl_lift0 : ∀ M n, lift0 (S n) M = lift0 1 (lift0 n M).
Lemma permute_lift :
∀ M n k p i,
i ≤ k →
lift p i (lift n k M) = lift n (k + p) (lift p i M).
Lemma permute_lift0 :
∀ M k, lift0 1 (lift 1 k M) = lift 1 (S k) (lift0 1 M).
Lemma lift_isApp n k t : isApp t = false → isApp (lift n k t) = false.
Lemma map_non_nil {A B} (f : A → B) l : l ≠ nil → map f l ≠ nil.
Lemma isLambda_lift n k (bod : term) :
isLambda bod = true → isLambda (lift n k bod) = true.
Lemma wf_lift n k t : wf t → wf (lift n k t).
Lemma mkApps_tApp t l :
isApp t = false → l ≠ nil → mkApps t l = tApp t l.
Lemma simpl_subst_rec :
∀ M (H : wf M) N n p k,
p ≤ n + k →
k ≤ p → subst N p (lift (List.length N + n) k M) = lift n k M.
Lemma simpl_subst :
∀ N M (H : wf M) n p, p ≤ n → subst N p (lift0 (length N + n) M) = lift0 n M.
Lemma mkApps_tRel n a l : mkApps (tRel n) (a :: l) = tApp (tRel n) (a :: l).
Lemma lift_mkApps n k t l : lift n k (mkApps t l) = mkApps (lift n k t) (map (lift n k) l).
Lemma commut_lift_subst_rec :
∀ M N n p k,
k ≤ p →
lift n k (subst N p M) = subst N (p + n) (lift n k M).
Lemma commut_lift_subst :
∀ M N k, subst N (S k) (lift0 1 M) = lift0 1 (subst N k M).
Lemma distr_lift_subst_rec :
∀ M N n p k,
lift n (p + k) (subst N p M) =
subst (List.map (lift n k) N) p (lift n (p + length N + k) M).
Lemma distr_lift_subst :
∀ M N n k,
lift n k (subst0 N M) = subst0 (map (lift n k) N) (lift n (length N + k) M).
Lemma distr_lift_subst10 :
∀ M N n k,
lift n k (subst10 N M) = subst10 (lift n k N) (lift n (S k) M).
Lemma subst_mkApps u k t l :
subst u k (mkApps t l) = mkApps (subst u k t) (map (subst u k) l).
Lemma subst1_mkApps u k t l : subst1 u k (mkApps t l) = mkApps (subst1 u k t) (map (subst1 u k) l).
Lemma distr_subst_rec :
∀ M N (P : list term) (wfP : All wf P) n p,
subst P (p + n) (subst N p M) =
subst (map (subst P n) N) p (subst P (p + length N + n) M).
Lemma distr_subst :
∀ P (wfP : All Ast.wf P) N M k,
subst P k (subst0 N M) = subst0 (map (subst P k) N) (subst P (length N + k) M).
Lemma lift_closed n k t : closedn k t → lift n k t = t.
Lemma closed_upwards {k t} k' : closedn k t → k' ≥ k → closedn k' t.
Lemma mkApps_mkApp u a v : mkApps (mkApp u a) v = mkApps u (a :: v).
Lemma wf_mkApp u a : wf u → wf a → wf (mkApp u a).
Lemma wf_mkApps u a : wf u → List.Forall wf a → wf (mkApps u a).
Lemma wf_subst ts k u : List.Forall wf ts → wf u → wf (subst ts k u).
Lemma wf_subst1 t k u : wf t → wf u → wf (subst1 t k u).
Lemma subst_empty k a : Ast.wf a → subst [] k a = a.
Lemma lift_to_extended_list_k Γ k : ∀ k',
to_extended_list_k Γ (k' + k) = map (lift0 k') (to_extended_list_k Γ k).
Lemma simpl_subst_k (N : list term) (M : term) :
Ast.wf M → ∀ k p, p = #|N| → subst N k (lift p k M) = M.
Lemma subst_app_decomp l l' k t :
Ast.wf t → Forall Ast.wf l →
subst (l ++ l') k t = subst l' k (subst (List.map (lift0 (length l')) l) k t).
Lemma subst_app_simpl l l' k t :
Ast.wf t → Forall Ast.wf l → Forall Ast.wf l' →
subst (l ++ l') k t = subst l k (subst l' (k + length l) t).
Lemma isLambda_subst (s : list term) k (bod : term) :
isLambda bod = true → isLambda (subst s k bod) = true.
Lemma map_vass_map_def g l n k :
(mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d)))
(map (map_def (lift n k) g) l)) =
(mapi (fun i d ⇒ map_decl (lift n (i + k)) d) (mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d))) l)).