Library MetaCoq.PCUIC.PCUICLiftSubst
Lifting and substitution for the AST
Definition shiftn k f :=
fun n ⇒ if Nat.ltb n k then n else k + (f (n - k)).
Fixpoint rename f t : term :=
match t with
| tRel i ⇒ tRel (f i)
| tEvar ev args ⇒ tEvar ev (List.map (rename f) args)
| tLambda na T M ⇒ tLambda na (rename f T) (rename (shiftn 1 f) M)
| tApp u v ⇒ tApp (rename f u) (rename f v)
| tProd na A B ⇒ tProd na (rename f A) (rename (shiftn 1 f) B)
| tLetIn na b t b' ⇒ tLetIn na (rename f b) (rename f t) (rename (shiftn 1 f) b')
| tCase ind p c brs ⇒
let brs' := List.map (on_snd (rename f)) brs in
tCase ind (rename f p) (rename f c) brs'
| tProj p c ⇒ tProj p (rename f c)
| tFix mfix idx ⇒
let mfix' := List.map (map_def (rename f) (rename (shiftn (List.length mfix) f))) mfix in
tFix mfix' idx
| tCoFix mfix idx ⇒
let mfix' := List.map (map_def (rename f) (rename (shiftn (List.length mfix) f))) mfix in
tCoFix mfix' idx
| x ⇒ x
end.
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) (lift n k v)
| tProd na A B ⇒ tProd na (lift n k A) (lift n (S k) B)
| 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).
fun n ⇒ if Nat.ltb n k then n else k + (f (n - k)).
Fixpoint rename f t : term :=
match t with
| tRel i ⇒ tRel (f i)
| tEvar ev args ⇒ tEvar ev (List.map (rename f) args)
| tLambda na T M ⇒ tLambda na (rename f T) (rename (shiftn 1 f) M)
| tApp u v ⇒ tApp (rename f u) (rename f v)
| tProd na A B ⇒ tProd na (rename f A) (rename (shiftn 1 f) B)
| tLetIn na b t b' ⇒ tLetIn na (rename f b) (rename f t) (rename (shiftn 1 f) b')
| tCase ind p c brs ⇒
let brs' := List.map (on_snd (rename f)) brs in
tCase ind (rename f p) (rename f c) brs'
| tProj p c ⇒ tProj p (rename f c)
| tFix mfix idx ⇒
let mfix' := List.map (map_def (rename f) (rename (shiftn (List.length mfix) f))) mfix in
tFix mfix' idx
| tCoFix mfix idx ⇒
let mfix' := List.map (map_def (rename f) (rename (shiftn (List.length mfix) f))) mfix in
tCoFix mfix' idx
| x ⇒ x
end.
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) (lift n k v)
| tProd na A B ⇒ tProd na (lift n k A) (lift n (S k) B)
| 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).
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 ⇒ tApp (subst s k u) (subst s k v)
| tProd na A B ⇒ tProd na (subst s k A) (subst s (S k) B)
| 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 && closedn k v
| 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 = true → ¬ isApp (lift n k t) = true.
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 simpl_subst_rec :
∀ 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 n p, p ≤ n → subst N p (lift0 (length N + n) M) = lift0 n M.
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) 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 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 subst_empty k 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) :
∀ k p, p = #|N| → subst N k (lift p k M) = M.
Lemma subst_app_decomp l l' k t :
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 :
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 fix_context (m : mfixpoint term) : context :=
List.rev (mapi (fun i d ⇒ vass d.(dname) (lift0 i d.(dtype))) m).
Lemma shiftn_ext n f f' : (∀ i, f i = f' i) → ∀ t, shiftn n f t = shiftn n f' t.
Lemma rename_ext f f' : (∀ i, f i = f' i) → (∀ t, rename f t = rename f' t).
Definition lift_renaming n k :=
fun i ⇒
if Nat.leb k i then n + i
else i.
Lemma shiftn_lift_renaming n m k : ∀ i, shiftn m (lift_renaming n k) i = lift_renaming n (m + k) i.
Lemma lift_rename n k t : lift n k t = rename (lift_renaming n k) t.
Definition up k (s : nat → term) :=
fun i ⇒
if k <=? i then rename (add k) (s (i - k))
else tRel i.
Notation "`=1`" := (pointwise_relation _ Logic.eq) (at level 80).
Infix "=1" := (pointwise_relation _ Logic.eq) (at level 90).
Lemma shiftn_compose n f f' : shiftn n f ∘ shiftn n f' =1 shiftn n (f ∘ f').
Lemma rename_compose f f' : rename f ∘ rename f' =1 rename (f ∘ f').
Lemma up_up k k' s : up k (up k' s) =1 up (k + k') s.
Fixpoint inst s u :=
match u with
| tRel n ⇒ s n
| tEvar ev args ⇒ tEvar ev (List.map (inst s) args)
| tLambda na T M ⇒ tLambda na (inst s T) (inst (up 1 s) M)
| tApp u v ⇒ tApp (inst s u) (inst s v)
| tProd na A B ⇒ tProd na (inst s A) (inst (up 1 s) B)
| tLetIn na b ty b' ⇒ tLetIn na (inst s b) (inst s ty) (inst (up 1 s) b')
| tCase ind p c brs ⇒
let brs' := List.map (on_snd (inst s)) brs in
tCase ind (inst s p) (inst s c) brs'
| tProj p c ⇒ tProj p (inst s c)
| tFix mfix idx ⇒
let mfix' := List.map (map_def (inst s) (inst (up (List.length mfix) s))) mfix in
tFix mfix' idx
| tCoFix mfix idx ⇒
let mfix' := List.map (map_def (inst s) (inst (up (List.length mfix) s))) mfix in
tCoFix mfix' idx
| x ⇒ x
end.
Definition subst_fn (l : list term) :=
fun i ⇒
match List.nth_error l i with
| None ⇒ tRel (i - List.length l)
| Some t ⇒ t
end.
Lemma up_ext k s s' : s =1 s' → up k s =1 up k s'.
Lemma inst_ext s s' : s =1 s' → inst s =1 inst s'.
Definition ren (f : nat → nat) : nat → term :=
fun i ⇒ tRel (f i).
Lemma ren_shiftn n f : up n (ren f) =1 ren (shiftn n f).
Instance proper_inst : Proper (`=1` ==> Logic.eq ==> Logic.eq) inst.
Instance proper_ext_eq {A B} : Proper (`=1` ==> `=1` ==> iff) (@pointwise_relation A _ (@Logic.eq B)).
Lemma rename_inst f : rename f =1 inst (ren f).
Instance rename_proper : Proper (`=1` ==> Logic.eq ==> Logic.eq) rename.
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 && closedn k v
| 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 = true → ¬ isApp (lift n k t) = true.
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 simpl_subst_rec :
∀ 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 n p, p ≤ n → subst N p (lift0 (length N + n) M) = lift0 n M.
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) 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 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 subst_empty k 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) :
∀ k p, p = #|N| → subst N k (lift p k M) = M.
Lemma subst_app_decomp l l' k t :
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 :
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 fix_context (m : mfixpoint term) : context :=
List.rev (mapi (fun i d ⇒ vass d.(dname) (lift0 i d.(dtype))) m).
Lemma shiftn_ext n f f' : (∀ i, f i = f' i) → ∀ t, shiftn n f t = shiftn n f' t.
Lemma rename_ext f f' : (∀ i, f i = f' i) → (∀ t, rename f t = rename f' t).
Definition lift_renaming n k :=
fun i ⇒
if Nat.leb k i then n + i
else i.
Lemma shiftn_lift_renaming n m k : ∀ i, shiftn m (lift_renaming n k) i = lift_renaming n (m + k) i.
Lemma lift_rename n k t : lift n k t = rename (lift_renaming n k) t.
Definition up k (s : nat → term) :=
fun i ⇒
if k <=? i then rename (add k) (s (i - k))
else tRel i.
Notation "`=1`" := (pointwise_relation _ Logic.eq) (at level 80).
Infix "=1" := (pointwise_relation _ Logic.eq) (at level 90).
Lemma shiftn_compose n f f' : shiftn n f ∘ shiftn n f' =1 shiftn n (f ∘ f').
Lemma rename_compose f f' : rename f ∘ rename f' =1 rename (f ∘ f').
Lemma up_up k k' s : up k (up k' s) =1 up (k + k') s.
Fixpoint inst s u :=
match u with
| tRel n ⇒ s n
| tEvar ev args ⇒ tEvar ev (List.map (inst s) args)
| tLambda na T M ⇒ tLambda na (inst s T) (inst (up 1 s) M)
| tApp u v ⇒ tApp (inst s u) (inst s v)
| tProd na A B ⇒ tProd na (inst s A) (inst (up 1 s) B)
| tLetIn na b ty b' ⇒ tLetIn na (inst s b) (inst s ty) (inst (up 1 s) b')
| tCase ind p c brs ⇒
let brs' := List.map (on_snd (inst s)) brs in
tCase ind (inst s p) (inst s c) brs'
| tProj p c ⇒ tProj p (inst s c)
| tFix mfix idx ⇒
let mfix' := List.map (map_def (inst s) (inst (up (List.length mfix) s))) mfix in
tFix mfix' idx
| tCoFix mfix idx ⇒
let mfix' := List.map (map_def (inst s) (inst (up (List.length mfix) s))) mfix in
tCoFix mfix' idx
| x ⇒ x
end.
Definition subst_fn (l : list term) :=
fun i ⇒
match List.nth_error l i with
| None ⇒ tRel (i - List.length l)
| Some t ⇒ t
end.
Lemma up_ext k s s' : s =1 s' → up k s =1 up k s'.
Lemma inst_ext s s' : s =1 s' → inst s =1 inst s'.
Definition ren (f : nat → nat) : nat → term :=
fun i ⇒ tRel (f i).
Lemma ren_shiftn n f : up n (ren f) =1 ren (shiftn n f).
Instance proper_inst : Proper (`=1` ==> Logic.eq ==> Logic.eq) inst.
Instance proper_ext_eq {A B} : Proper (`=1` ==> `=1` ==> iff) (@pointwise_relation A _ (@Logic.eq B)).
Lemma rename_inst f : rename f =1 inst (ren f).
Instance rename_proper : Proper (`=1` ==> Logic.eq ==> Logic.eq) rename.
Show the σ-calculus equations.
Additional combinators: idsn n for n-identity, consn for consing a parallel substitution.
Definition substitution := nat → term.
Notation "t '.[' σ ]" := (inst σ t) (at level 6, format "t .[ σ ]") : sigma_scope.
Definition subst_cons (t : term) (f : nat → term) :=
fun i ⇒
match i with
| 0 ⇒ t
| S n ⇒ f n
end.
Notation " t ⋅ s " := (subst_cons t s) (at level 90) : sigma_scope.
Instance subst_cons_proper : Proper (Logic.eq ==> `=1` ==> `=1`) subst_cons.
Definition shift : nat → term := tRel ∘ S.
Notation "↑" := shift : sigma_scope.
Definition subst_compose (σ τ : nat → term) :=
fun i ⇒ (σ i).[τ].
Infix "∘" := subst_compose : sigma_scope.
Instance subst_compose_proper : Proper (`=1` ==> `=1` ==> `=1`) subst_compose.
Definition Up σ : substitution := tRel 0 ⋅ (σ ∘ ↑).
Notation "⇑ s" := (Up s) (at level 20).
Lemma up_Up σ : up 1 σ =1 ⇑ σ.
Simplify away up 1
Definition ids (x : nat) := tRel x.
Definition ren_id (x : nat) := x.
Lemma ren_id_ids : ren ren_id =1 ids.
Lemma shiftn_id n : shiftn n ren_id =1 ren_id.
Lemma rename_ren_id : rename ren_id =1 id.
Lemma subst_ids t : t.[ids] = t.
Lemma compose_ids_r σ : σ ∘ ids =1 σ.
Lemma compose_ids_l σ : ids ∘ σ =1 σ.
Definition shiftk (k : nat) (x : nat) := tRel (k + x).
Notation "↑^ k" := (shiftk k) (at level 30, k at level 2, format "↑^ k") : sigma_scope.
Lemma shiftk_0 : shiftk 0 =1 ids.
Definition subst_consn {A} (l : list A) (σ : nat → A) :=
fun i ⇒
match List.nth_error l i with
| None ⇒ σ (i - List.length l)
| Some t ⇒ t
end.
Notation " t ⋅n s " := (subst_consn t s) (at level 40) : sigma_scope.
Lemma subst_consn_nil {A} (σ : nat → A) : nil ⋅n σ =1 σ.
Lemma subst_consn_subst_cons t l σ : (t :: l) ⋅n σ =1 (t ⋅ subst_consn l σ).
Lemma subst_consn_tip t σ : [t] ⋅n σ =1 (t ⋅ σ).
Instance subst_consn_proper {A} : Proper (Logic.eq ==> `=1` ==> `=1`) (@subst_consn A).
Instance subst_consn_proper_ext {A} : Proper (Logic.eq ==> `=1` ==> Logic.eq ==> Logic.eq) (@subst_consn A).
Fixpoint idsn n : list term :=
match n with
| 0 ⇒ []
| S n ⇒ idsn n ++ [tRel n]
end.
Definition Upn n σ := idsn n ⋅n (σ ∘ ↑^n).
Notation "⇑^ n σ" := (Upn n σ) (at level 30, n at level 2, format "⇑^ n σ") : sigma_scope.
Lemma Upn_eq n σ : Upn n σ = idsn n ⋅n (σ ∘ ↑^n).
Lemma Upn_proper : Proper (Logic.eq ==> `=1` ==> `=1`) Upn.
Definition subst_cons_gen {A} (t : A) (f : nat → A) :=
fun i ⇒
match i with
| 0 ⇒ t
| S n ⇒ f n
end.
Instance subst_cons_gen_proper {A} : Proper (Logic.eq ==> `=1` ==> `=1`) (@subst_cons_gen A).
Lemma subst_consn_subst_cons_gen {A} (t : A) l σ : subst_consn (t :: l) σ =1 (subst_cons_gen t (l ⋅n σ)).
Lemma subst_consn_app {A} {l l' : list A} {σ} : (l ++ l') ⋅n σ =1 l ⋅n (l' ⋅n σ).
Lemma subst_consn_ge {A} {l : list A} {i σ} : #|l| ≤ i → (l ⋅n σ) i = σ (i - #|l|).
Lemma subst_consn_lt {A} {l : list A} {i} :
i < #|l| →
{ x : _ & (List.nth_error l i = Some x) ∧ (∀ σ, (l ⋅n σ) i = x) }%type.
Lemma idsn_length n : #|idsn n| = n.
Lemma idsn_lt {n i} : i < n → nth_error (idsn n) i = Some (tRel i).
Lemma nth_error_idsn_Some :
∀ n k,
k < n →
nth_error (idsn n) k = Some (tRel k).
Lemma nth_error_idsn_None :
∀ n k,
k ≥ n →
nth_error (idsn n) k = None.
Lemma up_Upn {n σ} : up n σ =1 ⇑^n σ.
Simplify away iterated up's
The σ-calculus equations for Coq
Lemma inst_app {s t σ} : (tApp s t).[σ] = tApp s.[σ] t.[σ].
Lemma inst_lam {na t b σ} : (tLambda na t b).[σ] = tLambda na t.[σ] b.[⇑ σ].
Lemma inst_prod {na t b σ} : (tProd na t b).[σ] = tProd na t.[σ] b.[⇑ σ].
Lemma inst_letin {na t b b' σ} : (tLetIn na t b b').[σ] = tLetIn na t.[σ] b.[σ] b'.[⇑ σ].
Lemma inst_fix {mfix idx σ} : (tFix mfix idx).[σ] =
tFix (map (map_def (inst σ) (inst (⇑^#|mfix| σ))) mfix) idx.
Lemma inst_cofix {mfix idx σ} : (tCoFix mfix idx).[σ] =
tCoFix (map (map_def (inst σ) (inst (⇑^#|mfix| σ))) mfix) idx.
Lemma inst_mkApps :
∀ t l σ,
(mkApps t l).[σ] = mkApps t.[σ] (map (inst σ) l).
Lemma subst_cons_0 t σ : (tRel 0).[t ⋅ σ] = t.
Lemma subst_cons_shift t σ : ↑ ∘ (t ⋅ σ) = σ.
Lemma shiftk_shift n : ↑^(S n) =1 ↑^n ∘ ↑.
Lemma shiftk_shift_l n : ↑^(S n) =1 ↑ ∘ ↑^n.
Lemma Upn_1_Up σ : ⇑^1 σ =1 ⇑ σ.
Lemma subst_subst_consn s σ τ : (s ⋅ σ) ∘ τ =1 (s.[τ] ⋅ σ ∘ τ).
Lemma ren_shift : ↑ =1 ren S.
Lemma compose_ren f g : ren f ∘ ren g =1 ren (Basics.compose g f).
Lemma subst_cons_ren i f : (tRel i ⋅ ren f) =1 ren (subst_cons_gen i f).
Fixpoint ren_ids (n : nat) :=
match n with
| 0 ⇒ []
| S n ⇒ ren_ids n ++ [n]
end.
Lemma ren_ids_length n : #|ren_ids n| = n.
Lemma ren_ids_lt {n i} : i < n → nth_error (ren_ids n) i = Some i.
Infix "=2" := (Logic.eq ==> (pointwise_relation _ Logic.eq))%signature (at level 80).
Definition compose2 {A B C} (g : B → C) (f : A → B) : A → C :=
fun x ⇒ g (f x).
Infix "∘'" := compose2 (at level 90).
Lemma subst_consn_subst_cons' {A} (t : A) l : subst_consn (t :: l) =2 (subst_cons_gen t ∘ subst_consn l)%prog.
Lemma subst_consn_ids_ren n f : (idsn n ⋅n ren f) =1 ren (ren_ids n ⋅n f).
Lemma ren_shiftk n : ↑^n =1 ren (add n).
Specific lemma for the fix/cofix cases where we are subst_cons'ing a list of ids in front
of the substitution.
Lemma ren_subst_consn_comm:
∀ (f : nat → nat) (σ : nat → term) (n : nat),
ren (subst_consn (ren_ids n) (Init.Nat.add n ∘ f)%prog) ∘ subst_consn (idsn n) (σ ∘ ↑^n) =1
subst_consn (idsn n) (ren f ∘ σ ∘ ↑^n).
Lemma rename_inst_assoc t f σ : t.[ren f].[σ] = t.[ren f ∘ σ].
Lemma inst_rename_assoc_n:
∀ (f : nat → nat) (σ : nat → term) (n : nat),
subst_consn (idsn n) (σ ∘ ↑^n) ∘ ren (subst_consn (ren_ids n) (Init.Nat.add n ∘ f)%prog) =1
subst_consn (idsn n) (σ ∘ ren f ∘ ↑^n).
Lemma inst_rename_assoc t f σ : t.[σ].[ren f] = t.[σ ∘ ren f].
Lemma rename_subst_compose1 r s s' : ren r ∘ (s ∘ s') =1 ren r ∘ s ∘ s'.
Lemma rename_subst_compose2 r s s' : s ∘ (ren r ∘ s') =1 s ∘ ren r ∘ s'.
Lemma rename_subst_compose3 r s s' : s ∘ (s' ∘ ren r) =1 s ∘ s' ∘ ren r.
Lemma Up_Up_assoc:
∀ s s' : nat → term, (⇑ s) ∘ (⇑ s') =1 ⇑ (s ∘ s').
Lemma up_up_assoc:
∀ (s s' : nat → term) (n : nat), up n s ∘ up n s' =1 up n (s ∘ s').
Lemma inst_assoc t s s' : t.[s].[s'] = t.[s ∘ s'].
Lemma subst_compose_assoc s s' s'' : (s ∘ s') ∘ s'' =1 s ∘ (s' ∘ s'').
Lemma Upn_0 σ : ⇑^0 σ =1 σ.
Lemma Upn_Up σ n : ⇑^(S n) σ =1 ⇑^n ⇑ σ.
Lemma Upn_1 σ : ⇑^1 σ =1 ⇑ σ.
Lemma subst_cons_0_shift : tRel 0 ⋅ ↑ =1 ids.
Lemma subst_cons_0s_shifts σ : (σ 0) ⋅ (↑ ∘ σ) =1 σ.
Lemma subst_inst_aux s k t : subst s k t = inst (up k (subst_fn s)) t.
Lemma subst_fn_subst_consn s : subst_fn s =1 subst_consn s ids.
Theorem subst_inst s k t : subst s k t = inst (⇑^k (subst_consn s ids)) t.
∀ (f : nat → nat) (σ : nat → term) (n : nat),
ren (subst_consn (ren_ids n) (Init.Nat.add n ∘ f)%prog) ∘ subst_consn (idsn n) (σ ∘ ↑^n) =1
subst_consn (idsn n) (ren f ∘ σ ∘ ↑^n).
Lemma rename_inst_assoc t f σ : t.[ren f].[σ] = t.[ren f ∘ σ].
Lemma inst_rename_assoc_n:
∀ (f : nat → nat) (σ : nat → term) (n : nat),
subst_consn (idsn n) (σ ∘ ↑^n) ∘ ren (subst_consn (ren_ids n) (Init.Nat.add n ∘ f)%prog) =1
subst_consn (idsn n) (σ ∘ ren f ∘ ↑^n).
Lemma inst_rename_assoc t f σ : t.[σ].[ren f] = t.[σ ∘ ren f].
Lemma rename_subst_compose1 r s s' : ren r ∘ (s ∘ s') =1 ren r ∘ s ∘ s'.
Lemma rename_subst_compose2 r s s' : s ∘ (ren r ∘ s') =1 s ∘ ren r ∘ s'.
Lemma rename_subst_compose3 r s s' : s ∘ (s' ∘ ren r) =1 s ∘ s' ∘ ren r.
Lemma Up_Up_assoc:
∀ s s' : nat → term, (⇑ s) ∘ (⇑ s') =1 ⇑ (s ∘ s').
Lemma up_up_assoc:
∀ (s s' : nat → term) (n : nat), up n s ∘ up n s' =1 up n (s ∘ s').
Lemma inst_assoc t s s' : t.[s].[s'] = t.[s ∘ s'].
Lemma subst_compose_assoc s s' s'' : (s ∘ s') ∘ s'' =1 s ∘ (s' ∘ s'').
Lemma Upn_0 σ : ⇑^0 σ =1 σ.
Lemma Upn_Up σ n : ⇑^(S n) σ =1 ⇑^n ⇑ σ.
Lemma Upn_1 σ : ⇑^1 σ =1 ⇑ σ.
Lemma subst_cons_0_shift : tRel 0 ⋅ ↑ =1 ids.
Lemma subst_cons_0s_shifts σ : (σ 0) ⋅ (↑ ∘ σ) =1 σ.
Lemma subst_inst_aux s k t : subst s k t = inst (up k (subst_fn s)) t.
Lemma subst_fn_subst_consn s : subst_fn s =1 subst_consn s ids.
Theorem subst_inst s k t : subst s k t = inst (⇑^k (subst_consn s ids)) t.
Simplify away subst to the σ-calculus inst primitive.
Lemma term_forall_ctx_list_ind :
∀ P : context → term → Type,
(∀ Γ (n : nat), P Γ (tRel n)) →
(∀ Γ (i : ident), P Γ (tVar i)) →
(∀ Γ (n : nat) (l : list term), All (P Γ) l → P Γ (tEvar n l)) →
(∀ Γ s, P Γ (tSort s)) →
(∀ Γ (n : name) (t : term), P Γ t → ∀ t0 : term, P (vass n t :: Γ) t0 → P Γ (tProd n t t0)) →
(∀ Γ (n : name) (t : term), P Γ t → ∀ t0 : term, P (vass n t :: Γ) t0 → P Γ (tLambda n t t0)) →
(∀ Γ (n : name) (t : term),
P Γ t → ∀ t0 : term, P Γ t0 → ∀ t1 : term, P (vdef n t t0 :: Γ) t1 → P Γ (tLetIn n t t0 t1)) →
(∀ Γ (t u : term), P Γ t → P Γ u → P Γ (tApp t u)) →
(∀ Γ (s : String.string) (u : list Level.t), P Γ (tConst s u)) →
(∀ Γ (i : inductive) (u : list Level.t), P Γ (tInd i u)) →
(∀ Γ (i : inductive) (n : nat) (u : list Level.t), P Γ (tConstruct i n u)) →
(∀ Γ (p : inductive × nat) (t : term),
P Γ t → ∀ t0 : term, P Γ t0 → ∀ l : list (nat × term),
tCaseBrsProp (P Γ) l → P Γ (tCase p t t0 l)) →
(∀ Γ (s : projection) (t : term), P Γ t → P Γ (tProj s t)) →
(∀ Γ (m : mfixpoint term) (n : nat), tFixProp (P Γ) (P (Γ ,,, fix_context m)) m → P Γ (tFix m n)) →
(∀ Γ (m : mfixpoint term) (n : nat), tFixProp (P Γ) (P (Γ ,,, fix_context m)) m → P Γ (tCoFix m n)) →
∀ Γ (t : term), P Γ t.
Definition lift_decl n k d := (map_decl (lift n k) d).
Definition lift_context n k (Γ : context) : context :=
fold_context (fun k' ⇒ lift n (k' + k)) Γ.
Lemma lift_decl0 k d : map_decl (lift 0 k) d = d.
Lemma lift0_context k Γ : lift_context 0 k Γ = Γ.
Lemma lift_context_length n k Γ : #|lift_context n k Γ| = #|Γ|.
Definition lift_context_snoc0 n k Γ d : lift_context n k (d :: Γ) = lift_context n k Γ ,, lift_decl n (#|Γ| + k) d.
Lemma lift_context_snoc n k Γ d : lift_context n k (Γ ,, d) = lift_context n k Γ ,, lift_decl n (#|Γ| + k) d.
Lemma lift_context_alt n k Γ :
lift_context n k Γ =
mapi (fun k' d ⇒ lift_decl n (Nat.pred #|Γ| - k' + k) d) Γ.
Lemma lift_context_app n k Γ Δ :
lift_context n k (Γ ,,, Δ) = lift_context n k Γ ,,, lift_context n (#|Γ| + k) Δ.
Lemma nth_error_lift_context:
∀ (Γ' Γ'' : context) (v : nat),
v < #|Γ'| → ∀ nth k,
nth_error Γ' v = Some nth →
nth_error (lift_context #|Γ''| k Γ') v = Some (lift_decl #|Γ''| (#|Γ'| - S v + k) nth).
Lemma nth_error_lift_context_eq:
∀ (Γ' Γ'' : context) (v : nat) k,
nth_error (lift_context #|Γ''| k Γ') v =
option_map (lift_decl #|Γ''| (#|Γ'| - S v + k)) (nth_error Γ' v).