Library MetaCoq.PCUIC.PCUICSubstitution
From MetaCoq.Template Require Import utils config.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICInduction
PCUICLiftSubst PCUICEquality PCUICPosition PCUICCases PCUICSigmaCalculus
PCUICUnivSubst PCUICContextSubst PCUICTyping
PCUICWeakeningEnvConv PCUICWeakeningEnvTyp PCUICClosed PCUICClosedConv PCUICClosedTyp
PCUICReduction PCUICWeakeningConv PCUICWeakeningTyp PCUICCumulativity PCUICUnivSubstitutionConv
PCUICRenameDef PCUICRenameConv PCUICInstDef PCUICInstConv PCUICInstTyp PCUICOnFreeVars.
Require Import ssreflect.
From Equations Require Import Equations.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICInduction
PCUICLiftSubst PCUICEquality PCUICPosition PCUICCases PCUICSigmaCalculus
PCUICUnivSubst PCUICContextSubst PCUICTyping
PCUICWeakeningEnvConv PCUICWeakeningEnvTyp PCUICClosed PCUICClosedConv PCUICClosedTyp
PCUICReduction PCUICWeakeningConv PCUICWeakeningTyp PCUICCumulativity PCUICUnivSubstitutionConv
PCUICRenameDef PCUICRenameConv PCUICInstDef PCUICInstConv PCUICInstTyp PCUICOnFreeVars.
Require Import ssreflect.
From Equations Require Import Equations.
Substitution lemmas for typing derivations. Substitution is now derived from a general
instantiation lemma, but the rest of the theory is using substituion lemmas instead of the slightly more general but also more technical instantiation lemmas.Implicit Types (cf : checker_flags) (Σ : global_env_ext).
Local Set Keyed Unification.
Set Default Goal Selector "!".
#[global]
Hint Rewrite @app_context_length : wf.
Generalizable Variables Σ Γ t T.
Local Open Scope sigma_scope.
Well-typed substitution into a context with *no* let-ins
Inductive subs {cf:checker_flags} (Σ : global_env_ext) (Γ : context) : list term → context → Type :=
| emptys : subs Σ Γ [] []
| cons_ass Δ s na t T : subs Σ Γ s Δ → Σ ;;; Γ |- t : subst0 s T → subs Σ Γ (t :: s) (Δ ,, vass na T).
Lemma subs_length {cf:checker_flags} {Σ} {Γ s Δ} : subs Σ Γ s Δ → #|s| = #|Δ|.
Proof.
induction 1; simpl; auto. f_equal. auto.
Qed.
Well-typed substitution into a context with let-ins
Inductive subslet {cf:checker_flags} Σ (Γ : context) : list term → context → Type :=
| emptyslet : subslet Σ Γ [] []
| cons_let_ass Δ s na t T : subslet Σ Γ s Δ →
Σ ;;; Γ |- t : subst0 s T →
subslet Σ Γ (t :: s) (Δ ,, vass na T)
| cons_let_def Δ s na t T :
subslet Σ Γ s Δ →
Σ ;;; Γ |- subst0 s t : subst0 s T →
subslet Σ Γ (subst0 s t :: s) (Δ ,, vdef na t T).
#[global] Hint Constructors subslet : pcuic.
Lemma subslet_def {cf} {Σ : global_env_ext} {Γ Δ s na t T t'} :
subslet Σ Γ s Δ →
Σ;;; Γ |- subst0 s t : subst0 s T →
t' = subst0 s t →
subslet Σ Γ (t' :: s) (Δ ,, vdef na t T).
Proof.
now intros sub Ht ->; constructor.
Qed.
Lemma subslet_ass_tip {cf} {Σ : global_env_ext} {Γ na t T} :
Σ;;; Γ |- t : T →
subslet Σ Γ [t] [vass na T].
Proof.
intros; repeat constructor.
now rewrite !subst_empty.
Qed.
Lemma subslet_def_tip {cf} {Σ : global_env_ext} {Γ na t T} :
Σ;;; Γ |- t : T →
subslet Σ Γ [t] [vdef na t T].
Proof.
intros; apply subslet_def; try constructor.
all:now rewrite !subst_empty.
Qed.
#[global] Hint Resolve subslet_ass_tip subslet_def_tip : pcuic.
Lemma subslet_nth_error {cf:checker_flags} {Σ Γ s Δ decl n} :
subslet Σ Γ s Δ →
nth_error Δ n = Some decl →
∑ t, nth_error s n = Some t ×
let ty := subst0 (skipn (S n) s) (decl_type decl) in
Σ ;;; Γ |- t : ty ×
match decl_body decl return Type with
| Some t' ⇒
let b := subst0 (skipn (S n) s) t' in
(t = b)
| None ⇒ unit
end.
Proof.
induction 1 in n |- *; simpl; auto; destruct n; simpl; try congruence.
- intros [= <-]. ∃ t; split; auto.
simpl. split; auto. exact tt.
- intros. destruct decl as [na' [b|] ty]; cbn in ×.
+ specialize (IHX _ H) as [t' [hnth [hty heq]]]. ∃ t'; intuition auto.
+ now apply IHX.
- intros [= <-]. eexists; split; eauto.
simpl. split; auto.
- apply IHX.
Qed.
Lemma subslet_length {cf:checker_flags} {Σ Γ s Δ} : subslet Σ Γ s Δ → #|s| = #|Δ|.
Proof.
induction 1; simpl; f_equal; auto.
Qed.
Lemma subst_decl_closed n k d : closed_decl k d → subst_decl n k d = d.
Proof.
case: d ⇒ na [body|] ty; rewrite /subst_decl /map_decl /=.
- move/andb_and ⇒ [cb cty]. rewrite !subst_closedn //.
- move⇒ cty; now rewrite !subst_closedn //.
Qed.
Lemma closed_ctx_subst n k ctx : closed_ctx ctx = true → subst_context n k ctx = ctx.
Proof.
induction ctx in n, k |- *; auto.
rewrite closedn_ctx_cons.
move/andb_and ⇒ /= [Hctx Hd].
rewrite subst_context_snoc /snoc /= IHctx // subst_decl_closed //.
now apply: closed_decl_upwards.
Qed.
Lemma closed_tele_subst n k ctx :
closed_ctx ctx →
mapi (fun (k' : nat) (decl : context_decl) ⇒ subst_decl n (k' + k) decl) (List.rev ctx) = List.rev ctx.
Proof.
rewrite test_context_k_eq /mapi. simpl. generalize 0.
induction ctx using rev_ind; try easy.
move⇒ n0.
rewrite /closedn_ctx !rev_app_distr /id /=.
move/andb_and ⇒ [closedx Hctx].
rewrite subst_decl_closed //.
- rewrite (closed_decl_upwards n0) //; lia.
- f_equal. now rewrite IHctx.
Qed.
Lemma map_vass_map_def_subst g l n k :
(mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d)))
(map (map_def (subst n k) g) l)) =
(mapi (fun i d ⇒ map_decl (subst n (i + k)) d) (mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d))) l)).
Proof.
rewrite mapi_mapi mapi_map. apply mapi_ext.
intros. unfold map_decl, vass; simpl; f_equal.
rewrite commut_lift_subst_rec. 1: lia. f_equal; lia.
Qed.
Lemma All_local_env_subst {cf:checker_flags} (P Q : context → term → typ_or_sort → Type) c n k :
All_local_env Q c →
(∀ Γ t T,
Q Γ t T →
P (subst_context n k Γ) (subst n (#|Γ| + k) t)
(typ_or_sort_map (subst n (#|Γ| + k)) T)
) →
All_local_env P (subst_context n k c).
Proof.
intros Hq Hf.
induction Hq in |- *; try econstructor; eauto;
simpl; unfold snoc; rewrite subst_context_snoc; econstructor; eauto.
- simpl. eapply (Hf _ _ Sort). eauto.
- simpl. eapply (Hf _ _ Sort). eauto.
- simpl. eapply (Hf _ _ (Typ t)). eauto.
Qed.
Lemma subst_length {cf:checker_flags} Σ Γ s Γ' : subs Σ Γ s Γ' → #|s| = #|Γ'|.
Proof.
induction 1; simpl; lia.
Qed.
Lemma subs_nth_error_ge {cf:checker_flags} Σ Γ Γ' Γ'' v s :
subs Σ Γ s Γ' →
#|Γ' ,,, Γ''| ≤ v →
nth_error (Γ ,,, Γ' ,,, Γ'') v =
nth_error (Γ ,,, subst_context s 0 Γ'') (v - #|Γ'|).
Proof.
simpl.
intros. rewrite app_context_length in H.
rewrite !nth_error_app_ge; autorewrite with wf; f_equal; try lia.
Qed.
Lemma nth_error_subst_context (Γ' : context) s (v : nat) k :
nth_error (subst_context s k Γ') v =
option_map (subst_decl s (#|Γ'| - S v + k)) (nth_error Γ' v).
Proof.
induction Γ' in v |- *; intros.
- simpl. unfold subst_context, fold_context_k; simpl; rewrite nth_error_nil. easy.
- simpl. destruct v; rewrite subst_context_snoc.
+ simpl. repeat f_equal; try lia.
+ simpl. rewrite IHΓ'; simpl in ×. lia_f_equal.
Qed.
Lemma subs_nth_error_lt {cf:checker_flags} Σ Γ Γ' Γ'' v s :
subs Σ Γ s Γ' →
v < #|Γ''| →
nth_error (Γ ,,, subst_context s 0 Γ'') v =
option_map (map_decl (subst s (#|Γ''| - S v))) (nth_error (Γ ,,, Γ' ,,, Γ'') v).
Proof.
simpl. intros Hs Hv.
rewrite !nth_error_app_lt; autorewrite with wf; f_equal; try lia.
erewrite nth_error_subst_context. f_equal. unfold subst_decl. rewrite Nat.add_0_r. reflexivity.
Qed.
Lemma subslet_nth_error_lt {cf:checker_flags} Σ Γ Γ' Γ'' v s :
subslet Σ Γ s Γ' →
v < #|Γ''| →
nth_error (Γ ,,, subst_context s 0 Γ'') v =
option_map (map_decl (subst s (#|Γ''| - S v))) (nth_error (Γ ,,, Γ' ,,, Γ'') v).
Proof.
simpl. intros Hs Hv.
rewrite !nth_error_app_lt; autorewrite with wf; f_equal; try lia.
erewrite nth_error_subst_context. f_equal. unfold subst_decl. rewrite Nat.add_0_r. reflexivity.
Qed.
Lemma expand_lets_subst_comm' Γ s k x :
closedn (k + #|Γ|) x →
expand_lets (subst_context s k Γ) x = subst s (k + context_assumptions Γ) (expand_lets Γ x).
Proof.
unfold expand_lets, expand_lets_k; simpl; intros clx.
len.
rewrite !subst_extended_subst.
rewrite distr_subst. f_equal.
len. rewrite subst_closedn //.
rewrite Nat.add_assoc; eapply closedn_lift.
now rewrite Nat.add_comm.
Qed.
Notation subst_predicate s := (map_predicate_k id (subst s)).
Lemma subst_iota_red s p k pars args br :
#|skipn pars args| = context_assumptions br.(bcontext) →
closedn_ctx #|pparams p| (bcontext br) →
subst s k (iota_red pars p args br) =
iota_red pars (subst_predicate s k p) (List.map (subst s k) args) (map_branch_k (subst s) id k br).
Proof.
intros hctx cl. rewrite !subst_inst.
rewrite inst_iota_red //.
f_equal.
- rewrite /inst_predicate /map_predicate_k.
f_equal.
× apply map_ext ⇒ ?. now rewrite subst_inst.
× now rewrite subst_inst up_Upn Upn_Upn.
- eapply map_ext ⇒ ?. now rewrite subst_inst.
- now rewrite /inst_branch /map_branch_k subst_inst up_Upn Upn_Upn.
Qed.
Lemma subst_unfold_fix n k mfix idx narg fn :
unfold_fix mfix idx = Some (narg, fn) →
unfold_fix (map (map_def (subst n k) (subst n (#|mfix| + k))) mfix) idx = Some (narg, subst n k fn).
Proof.
unfold unfold_fix.
rewrite nth_error_map. destruct (nth_error mfix idx) eqn:Hdef; try congruence.
move⇒ [= <- <-] /=. f_equal. f_equal.
solve_all.
erewrite (distr_subst_rec _ _ _ k 0).
rewrite fix_subst_length. simpl. f_equal.
unfold fix_subst. rewrite !map_length.
generalize #|mfix| at 2 3. induction n0; auto. simpl.
f_equal. apply IHn0.
Qed.
#[global]
Hint Resolve subst_unfold_fix : core.
Lemma subst_unfold_cofix n k mfix idx narg fn :
unfold_cofix mfix idx = Some (narg, fn) →
unfold_cofix (map (map_def (subst n k) (subst n (#|mfix| + k))) mfix) idx = Some (narg, subst n k fn).
Proof.
unfold unfold_cofix.
rewrite nth_error_map. destruct (nth_error mfix idx) eqn:Hdef; try congruence.
intros [= <- <-]. simpl. do 2 f_equal. solve_all.
erewrite (distr_subst_rec _ _ _ k 0).
rewrite cofix_subst_length. simpl. f_equal.
unfold cofix_subst. rewrite !map_length.
generalize #|mfix| at 2 3. induction n0; auto. simpl.
f_equal. apply IHn0.
Qed.
#[global]
Hint Resolve subst_unfold_cofix : core.
Lemma decompose_app_rec_subst n k t l :
let (f, a) := decompose_app_rec t l in
subst n k f = f →
decompose_app_rec (subst n k t) (map (subst n k) l) = (f, map (subst n k) a).
Proof.
induction t in k, l |- *; simpl; auto; try congruence.
- destruct Nat.leb; try reflexivity.
destruct nth_error.
+ simpl. intros →. simpl. reflexivity.
+ intros →. simpl. reflexivity.
- specialize (IHt1 k (t2 :: l)).
destruct decompose_app_rec. intros H. rewrite IHt1; auto.
Qed.
Lemma decompose_app_subst n k t f a :
decompose_app t = (f, a) → subst n k f = f →
decompose_app (subst n k t) = (subst n k f, map (subst n k) a).
Proof.
generalize (decompose_app_rec_subst n k t []).
unfold decompose_app. destruct decompose_app_rec.
move⇒ Heq [= <- <-] Heq'. now rewrite Heq' (Heq Heq').
Qed.
#[global]
Hint Rewrite decompose_app_subst using auto : lift.
Lemma subst_is_constructor:
∀ (args : list term) (narg : nat) n k,
is_constructor narg args = true → is_constructor narg (map (subst n k) args) = true.
Proof.
intros args narg.
unfold is_constructor; intros.
rewrite nth_error_map. destruct nth_error; try discriminate. simpl. intros.
unfold isConstruct_app in ×.
destruct (decompose_app t) eqn:Heq. eapply decompose_app_subst in Heq as →.
- destruct t0; try discriminate || reflexivity.
- destruct t0; try discriminate || reflexivity.
Qed.
#[global]
Hint Resolve subst_is_constructor : core.
#[global]
Hint Constructors All_local_env : core.
Lemma typed_subst `{checker_flags} Σ Γ t T n k :
wf Σ.1 → k ≥ #|Γ| →
Σ ;;; Γ |- t : T → subst n k T = T ∧ subst n k t = t.
Proof.
intros wfΣ Hk Hty.
pose proof (typing_wf_local Hty).
apply typecheck_closed in Hty; eauto.
destruct Hty as [_ [Hcl [Ht HT]%andb_and]].
pose proof (closed_upwards k Ht).
simpl in ×. forward H0 by lia.
pose proof (closed_upwards k HT).
simpl in ×. forward H1 by lia.
apply (subst_closedn n) in H0; apply (subst_closedn n) in H1; auto.
Qed.
Lemma subst_wf_local `{checker_flags} Σ Γ n k :
wf Σ.1 →
wf_local Σ Γ →
subst_context n k Γ = Γ.
Proof.
intros wfΣ.
induction 1; auto; unfold subst_context, snoc; rewrite fold_context_k_snoc0;
auto; unfold snoc;
f_equal; auto; unfold map_decl; simpl.
- destruct t0 as [s Hs]. unfold vass. simpl. f_equal.
eapply typed_subst; eauto. lia.
- unfold vdef.
f_equal.
+ f_equal. eapply typed_subst; eauto. lia.
+ eapply typed_subst in t1 as [Ht HT]; eauto. lia.
Qed.
Lemma subst_declared_constant `{H:checker_flags} Σ cst decl n k u :
wf Σ →
declared_constant Σ cst decl →
map_constant_body (subst n k) (map_constant_body (subst_instance u) decl) =
map_constant_body (subst_instance u) decl.
Proof.
intros.
eapply declared_decl_closed in H0; eauto.
unfold map_constant_body.
do 2 red in H0. destruct decl as [ty [body|] univs]; simpl in ×.
- rewrite → andb_and in H0. intuition auto.
rewrite <- (closedn_subst_instance 0 body u) in H1.
rewrite <- (closedn_subst_instance 0 ty u) in H2.
f_equal.
+ apply subst_closedn; eauto using closed_upwards with arith wf.
+ f_equal. apply subst_closedn; eauto using closed_upwards with arith wf.
- red in H0. f_equal.
intuition. simpl in ×.
rewrite <- (closedn_subst_instance 0 ty u) in H0.
rewrite andb_true_r in H0.
eapply subst_closedn; eauto using closed_upwards with arith wf.
Qed.
Definition subst_mutual_inductive_body n k m :=
map_mutual_inductive_body (fun k' ⇒ subst n (k' + k)) m.
Lemma subst_fix_context:
∀ (mfix : list (def term)) n (k : nat),
fix_context (map (map_def (subst n k) (subst n (#|mfix| + k))) mfix) =
subst_context n k (fix_context mfix).
Proof.
intros mfix n k. unfold fix_context.
rewrite map_vass_map_def_subst rev_mapi.
fold (fix_context mfix).
rewrite (subst_context_alt n k (fix_context mfix)).
now rewrite /subst_decl mapi_length fix_context_length.
Qed.
Lemma subst_destArity ctx t n k :
match destArity ctx t with
| Some (args, s) ⇒
destArity (subst_context n k ctx) (subst n (#|ctx| + k) t) = Some (subst_context n k args, s)
| None ⇒ True
end.
Proof.
revert ctx.
induction t in n, k |- × using term_forall_list_ind; intros ctx; simpl; trivial.
- move: (IHt2 n k (ctx,, vass n0 t1)).
now rewrite subst_context_snoc /= /subst_decl /map_decl /vass /=.
- move: (IHt3 n k (ctx,, vdef n0 t1 t2)).
now rewrite subst_context_snoc /= /subst_decl /map_decl /vass /=.
Qed.
Lemma decompose_prod_n_assum0 ctx t : decompose_prod_n_assum ctx 0 t = Some (ctx, t).
Proof. destruct t; simpl; reflexivity. Qed.
Lemma to_extended_list_k_map_subst:
∀ n (k : nat) (c : context) k',
#|c| + k' ≤ k →
to_extended_list_k c k' = map (subst n k) (to_extended_list_k c k').
Proof.
intros n k c k'.
pose proof (to_extended_list_k_spec c k').
symmetry. solve_all.
destruct H as [x' [-> Hx']]. intuition. simpl.
destruct (leb_spec_Set k x').
- lia.
- reflexivity.
Qed.
Lemma wf_arities_context' {cf:checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} {mind mdecl} :
on_inductive cumulSpec0 (lift_typing typing) Σ mind mdecl →
wf_local Σ (arities_context (ind_bodies mdecl)).
Proof.
intros Hdecl.
apply onInductives in Hdecl.
unfold arities_context.
revert Hdecl.
induction (ind_bodies mdecl) using rev_ind. 1: constructor.
intros Ha.
rewrite rev_map_app.
simpl. apply Alli_app in Ha as [Hl Hx].
inv Hx. clear X0.
apply onArity in X as [s Hs].
specialize (IHl Hl).
econstructor; eauto.
fold (arities_context l) in ×.
unshelve epose proof (weakening Σ [] (arities_context l) _ _ wfΣ _ Hs).
1: now rewrite app_context_nil_l.
simpl in X.
eapply (env_prop_typing typecheck_closed) in Hs; eauto.
rewrite → andb_and in Hs. destruct Hs as [Hs Ht].
simpl in Hs. apply (lift_closed #|arities_context l|) in Hs.
rewrite → Hs, app_context_nil_l in X. simpl. ∃ s.
apply X.
Qed.
Lemma wf_arities_context {cf:checker_flags} {Σ : global_env} {wfΣ : wf Σ} {mind mdecl} :
declared_minductive Σ mind mdecl → wf_local (Σ, ind_universes mdecl) (arities_context mdecl.(ind_bodies)).
Proof.
intros Hdecl.
eapply declared_minductive_inv in Hdecl. 2:apply weaken_env_prop_typing. all:eauto.
eapply wf_arities_context'; eauto.
Qed.
Lemma on_constructor_closed_arities {cf:checker_flags} {Σ : global_env} {wfΣ : wf Σ} {mind mdecl idecl indices cdecl cs} :
on_constructor cumulSpec0 (lift_typing typing) (Σ, ind_universes mdecl) mdecl (inductive_ind mind) indices idecl cdecl cs →
closedn #|arities_context (ind_bodies mdecl)| cdecl.(cstr_type).
Proof.
intros [? ? [s Hs] _ _ _ _].
pose proof (typing_wf_local Hs).
destruct cdecl as [id cty car].
apply subject_closed in Hs; eauto.
Qed.
Lemma on_constructor_closed {cf:checker_flags} {Σ : global_env} {wfΣ : wf Σ} {mind mdecl u idecl indices cdecl cs} :
on_constructor cumulSpec0 (lift_typing typing) (Σ, ind_universes mdecl) mdecl (inductive_ind mind) indices idecl cdecl cs →
let cty := subst0 (inds (inductive_mind mind) u (ind_bodies mdecl))
(subst_instance u cdecl.(cstr_type))
in closed cty.
Proof.
intros [? ? [s Hs] _ _ _ _].
pose proof (typing_wf_local Hs).
destruct cdecl as [id cty car].
apply subject_closed in Hs; eauto.
rewrite arities_context_length in Hs.
simpl in ×.
eapply (closedn_subst _ 0 0).
- clear. unfold inds.
induction #|ind_bodies mdecl|; simpl; try constructor; auto.
- simpl. now rewrite → inds_length, closedn_subst_instance.
Qed.
Lemma subst_cstr_concl_head ind u mdecl (arity : context) args :
let head := tRel (#|ind_bodies mdecl| - S (inductive_ind ind) + #|ind_params mdecl| + #|arity|) in
let s := (inds (inductive_mind ind) u (ind_bodies mdecl)) in
inductive_ind ind < #|ind_bodies mdecl| →
subst s (#|arity| + #|ind_params mdecl|)
(subst_instance u (mkApps head (to_extended_list_k (ind_params mdecl) #|arity| ++ args)))
= mkApps (tInd ind u) (to_extended_list_k (ind_params mdecl) #|arity| ++
map (subst s (#|arity| + #|ind_params mdecl|)) (map (subst_instance u) args)).
Proof.
intros.
rewrite subst_instance_mkApps subst_mkApps.
f_equal.
- subst head. simpl subst_instance.
rewrite (subst_rel_eq _ _ (#|ind_bodies mdecl| - S (inductive_ind ind)) (tInd ind u)) //; try lia.
subst s. rewrite inds_spec rev_mapi nth_error_mapi /=.
elim nth_error_spec.
+ intros. simpl.
f_equal. destruct ind; simpl. f_equal. f_equal. simpl in H. lia.
+ rewrite List.rev_length. lia.
- rewrite !map_app. f_equal.
rewrite map_subst_instance_to_extended_list_k.
erewrite to_extended_list_k_map_subst at 2.
+ now rewrite Nat.add_comm.
+ lia.
Qed.
Lemma subst_to_extended_list_k s k args ctx :
make_context_subst (List.rev ctx) args [] = Some s →
map (subst s k) (to_extended_list_k ctx k) = map (lift0 k) args.
Proof.
move/make_context_subst_spec. rewrite List.rev_involutive.
move⇒ H; induction H; simpl; auto.
- rewrite map_app -IHcontext_subst //.
rewrite to_extended_list_k_cons /= !map_app.
f_equal.
+ rewrite (lift_to_extended_list_k _ _ 1) map_map_compose.
pose proof (to_extended_list_k_spec Γ k).
solve_all. destruct H0 as [n [-> Hn]].
rewrite /lift (subst_app_decomp [a] s k); auto with wf.
rewrite subst_rel_gt.
× simpl. lia.
× unf_term. repeat (f_equal; simpl; try lia).
+ now rewrite /map (subst_rel_eq _ _ 0 a).
- rewrite -IHcontext_subst // to_extended_list_k_cons /=.
rewrite (lift_to_extended_list_k _ _ 1) map_map_compose.
pose proof (to_extended_list_k_spec Γ k).
solve_all. destruct H0 as [n [-> Hn]].
rewrite /lift (subst_app_decomp [subst0 s b] s k); auto with wf.
rewrite subst_rel_gt.
+ simpl; lia.
+ unf_term. repeat (f_equal; simpl; try lia).
Qed.
Lemma Alli_map_option_out_mapi_Some_spec' {A B} (f g : nat → A → option B) h l t P :
All P l →
(∀ i x t, P x → f i x = Some t → g i x = Some (h t)) →
map_option_out (mapi f l) = Some t →
map_option_out (mapi g l) = Some (map h t).
Proof.
unfold mapi. generalize 0.
move ⇒ n Ha Hfg. move: t.
induction Ha in n |- *; try constructor; auto.
- destruct t; cbnr; discriminate.
- move⇒ t /=. case E: (f n x) ⇒ [b|]; try congruence.
rewrite (Hfg n _ _ p E).
case E' : map_option_out ⇒ [b'|]; try congruence.
move⇒ [= <-]. now rewrite (IHHa _ _ E').
Qed.
#[global]
Hint Unfold subst1 : subst.
#[global]
Hint Rewrite subst_mkApps distr_subst: subst.
Inductive untyped_subslet (Γ : context) : list term → context → Type :=
| untyped_emptyslet : untyped_subslet Γ [] []
| untyped_cons_let_ass Δ s na t T :
untyped_subslet Γ s Δ →
untyped_subslet Γ (t :: s) (Δ ,, vass na T)
| untyped_cons_let_def Δ s na t T :
untyped_subslet Γ s Δ →
untyped_subslet Γ (subst0 s t :: s) (Δ ,, vdef na t T).
Lemma subslet_untyped_subslet {cf:checker_flags} Σ Γ s Γ' : subslet Σ Γ s Γ' → untyped_subslet Γ s Γ'.
Proof.
induction 1; constructor; auto.
Qed.
Coercion subslet_untyped_subslet : subslet >-> untyped_subslet.
Lemma decompose_prod_assum_it_mkProd_or_LetIn ctx t ctx' t' :
decompose_prod_assum ctx t = (ctx', t') →
it_mkProd_or_LetIn ctx t = it_mkProd_or_LetIn ctx' t'.
Proof.
induction t in ctx, ctx', t' |- *; simpl; try intros [= → <-]; auto.
- intros H. now apply IHt2 in H.
- intros H. now apply IHt3 in H.
Qed.
Inductive decompose_prod_assum_graph : term → (context × term) → Type :=
| decompose_arity ctx t : decompose_prod_assum_graph (it_mkProd_or_LetIn ctx t) (ctx, t).
Lemma decompose_prod_assum_spec ctx t :
decompose_prod_assum_graph (it_mkProd_or_LetIn ctx t) (decompose_prod_assum ctx t).
Proof.
induction t in ctx |- *; simpl; try constructor 1.
- specialize (IHt2 (vass na t1 :: ctx)).
apply IHt2.
- apply (IHt3 (vdef na t1 t2 :: ctx)).
Qed.
Lemma subst_decompose_prod_assum_rec ctx t s k :
let (ctx', t') := decompose_prod_assum ctx t in
∑ ctx'' t'',
(decompose_prod_assum [] (subst s (#|ctx'| + k) t') = (ctx'', t'')) ×
(decompose_prod_assum (subst_context s k ctx) (subst s (length ctx + k) t) =
(subst_context s k ctx' ,,, ctx'', t'')).
Proof.
induction t in ctx, k |- *; simpl; try solve [ eexists _, _; pcuicfo ].
- elim: leb_spec_Set ⇒ comp.
+ destruct (nth_error s (n - (#|ctx| + k))) eqn:Heq.
× destruct decompose_prod_assum eqn:Heq'.
eexists _, _; intuition eauto.
now rewrite decompose_prod_assum_ctx Heq'.
× eexists _,_; pcuicfo.
+ eexists _,_; pcuicfo.
- destruct decompose_prod_assum eqn:Heq.
rewrite decompose_prod_assum_ctx in Heq.
destruct (decompose_prod_assum [] t2) eqn:Heq'.
noconf Heq.
specialize (IHt2 ctx (S k)).
rewrite decompose_prod_assum_ctx in IHt2.
rewrite Heq' in IHt2.
destruct IHt2 as [ctx'' [t'' [eqt eqt2]]].
∃ ctx'', t''. rewrite -eqt.
split.
× unfold snoc; simpl. rewrite !app_context_length.
simpl. lia_f_equal.
× rewrite decompose_prod_assum_ctx in eqt2.
rewrite decompose_prod_assum_ctx.
rewrite Nat.add_succ_r in eqt2.
destruct (decompose_prod_assum [] (subst s _ t2)) eqn:Heq''.
rewrite subst_context_app in eqt2.
rewrite !subst_context_app subst_context_snoc.
injection eqt2. intros <-.
intros eqctx. f_equal.
unfold app_context in eqctx.
rewrite app_assoc in eqctx.
apply app_inv_tail in eqctx.
subst c. rewrite app_context_assoc.
unfold snoc. simpl. lia_f_equal.
- destruct decompose_prod_assum eqn:Heq.
rewrite decompose_prod_assum_ctx in Heq.
destruct (decompose_prod_assum [] t3) eqn:Heq'.
noconf Heq.
specialize (IHt3 ctx (S k)).
rewrite decompose_prod_assum_ctx in IHt3.
rewrite Heq' in IHt3.
destruct IHt3 as [ctx'' [t'' [eqt eqt3]]].
∃ ctx'', t''. rewrite -eqt.
split.
× unfold snoc; simpl. rewrite !app_context_length.
simpl. lia_f_equal.
× rewrite decompose_prod_assum_ctx in eqt3.
rewrite decompose_prod_assum_ctx.
rewrite Nat.add_succ_r in eqt3.
destruct (decompose_prod_assum [] (subst s _ t3)) eqn:Heq''.
rewrite subst_context_app in eqt3.
rewrite !subst_context_app subst_context_snoc.
injection eqt3. intros <-.
intros eqctx. f_equal.
unfold app_context in eqctx.
rewrite app_assoc in eqctx.
apply app_inv_tail in eqctx.
subst c. rewrite app_context_assoc.
unfold snoc. simpl. lia_f_equal.
Qed.
Arguments Nat.sub : simpl nomatch.
Lemma assumption_context_skipn Γ n :
assumption_context Γ →
assumption_context (skipn n Γ).
Proof.
induction 1 in n |- *; simpl.
- destruct n; constructor.
- destruct n.
× rewrite skipn_0. constructor; auto.
× now rewrite skipn_S.
Qed.
#[global]
Hint Rewrite idsn_length : len.
Lemma subst_fn_eq s s' x : s = s' → subst_fn s x = subst_fn s' x.
Proof.
intros → ; reflexivity.
Qed.
Lemma map_option_out_impl {A B} (l : list A) (f g : A → option B) x :
(∀ x y, f x = Some y → g x = Some y) →
map_option_out (map f l) = Some x →
map_option_out (map g l) = Some x.
Proof.
intros Hfg.
induction l in x |- *; simpl; auto.
destruct (f a) eqn:fa.
- rewrite (Hfg _ _ fa).
move: IHl; destruct map_option_out.
× move⇒ H'. specialize (H' _ eq_refl).
rewrite H'. congruence.
× discriminate.
- discriminate.
Qed.
Lemma substitution_check_one_fix s k mfix inds :
map_option_out (map check_one_fix mfix) = Some inds →
map_option_out (map (fun x : def term ⇒
check_one_fix (map_def (subst s k) (subst s (#|mfix| + k)) x)) mfix) = Some inds.
Proof.
apply map_option_out_impl.
move⇒ [na ty def rarg] /=.
rewrite decompose_prod_assum_ctx.
destruct (decompose_prod_assum _ ty) eqn:decomp.
rewrite decompose_prod_assum_ctx in decomp.
destruct (decompose_prod_assum [] ty) eqn:decty.
noconf decomp. rewrite !app_context_nil_l.
pose proof (subst_decompose_prod_assum_rec [] ty s k).
rewrite decty in X.
destruct X as [ctx'' [t'' [dect decty']]].
rewrite subst_context_nil in decty'; simpl in decty'.
rewrite decty'. intros ind.
rewrite smash_context_app.
rewrite (smash_context_acc _ (smash_context _ _)).
rewrite List.rev_app_distr.
destruct (nth_error_spec (List.rev (smash_context [] c0)) rarg) ⇒ /= //;
autorewrite with len in l; simpl in ×.
rewrite nth_error_app_lt; autorewrite with len; simpl; try lia.
rewrite (smash_context_subst []) /=.
rewrite nth_error_rev_inv; autorewrite with len; simpl; try lia.
rewrite nth_error_subst_context /=.
autorewrite with len.
rewrite nth_error_rev_inv in e; autorewrite with len; auto.
autorewrite with len in e. simpl in e. rewrite e.
simpl.
destruct (decompose_app (decl_type x)) eqn:Happ.
destruct t0; try discriminate. simpl in ×.
erewrite decompose_app_subst; eauto. simpl. auto.
Qed.
Lemma substitution_check_one_cofix s k mfix inds :
map_option_out (map check_one_cofix mfix) = Some inds →
map_option_out (map (fun x : def term ⇒
check_one_cofix (map_def (subst s k) (subst s (#|mfix| + k)) x)) mfix) = Some inds.
Proof.
apply map_option_out_impl. move⇒ [na ty def rarg] /= ind.
destruct (decompose_prod_assum [] ty) eqn:decty.
destruct (decompose_app t) eqn:eqapp.
destruct t0; try discriminate. simpl.
pose proof (subst_decompose_prod_assum_rec [] ty s k).
rewrite decty in X.
destruct X as [ctx'' [t'' [dect decty']]].
rewrite decty'.
apply decompose_app_inv in eqapp.
subst t.
rewrite subst_mkApps /= in dect.
rewrite decompose_prod_assum_mkApps in dect. noconf dect.
rewrite decompose_app_mkApps //.
Qed.
Lemma subs_nth_error {cf:checker_flags} Σ Γ s Δ decl n t :
subs Σ Γ s Δ →
nth_error Δ n = Some decl →
nth_error s n = Some t →
match decl_body decl return Type with
| Some t' ⇒ False
| None ⇒
let ty := subst0 (skipn (S n) s) (decl_type decl) in
Σ ;;; Γ |- t : ty
end.
Proof.
induction 1 in n |- *; simpl; auto; destruct n; simpl; try congruence.
- intros [= <-]. intros [= ->].
simpl. exact t1.
- intros. destruct decl as [na' [b|] ty]; cbn in ×.
+ eapply IHX. all: eauto.
+ now apply IHX.
Qed.
Lemma untyped_subslet_nth_error Γ s Δ decl n t :
untyped_subslet Γ s Δ →
nth_error Δ n = Some decl →
nth_error s n = Some t →
match decl_body decl return Type with
| Some t' ⇒ t = subst0 (skipn (S n) s) t'
| None ⇒ True
end.
Proof.
induction 1 in n |- *; simpl; auto; destruct n; simpl; try congruence.
- intros [= <-]. intros [= ->].
simpl. auto.
- intros. destruct decl as [na' [b|] ty]; cbn in ×. 2: auto.
specialize (IHX _ H H0). intuition auto.
- intros [= <-]. intros [= <-].
simpl. split; auto.
- apply IHX.
Qed.
Arguments iota_red : simpl never.
Substitution without lets in Γ'
Lemma subs_usubst {cf:checker_flags} Σ Γ Γ' Γ'' s :
subs Σ Γ s Γ' →
usubst (Γ,,, Γ',,, Γ'') (⇑^#|Γ''| (s ⋅n ids)) (Γ,,, subst_context s 0 Γ'').
Proof.
intros subs n decl.
case: (nth_error_app_context (Γ ,,, Γ') Γ'' n) ⇒ // x hnth hlt [=] hx; subst x ⇒ b hb.
- left; eexists n, _.
split; auto.
× rewrite Upn_eq /subst_consn idsn_lt //.
× rewrite nth_error_app_lt; len ⇒ //.
change (fun m ⇒ S (n + m)) with (lift_renaming (S n) 0).
rewrite nth_error_subst_context /= hnth /=. split; eauto.
rewrite /= hb /=. f_equal.
rewrite subst_inst. rewrite Nat.add_0_r.
rewrite rename_inst.
replace #|Γ''| with ((#|Γ''| - S n) + S n) at 2 by lia.
set (k := S n).
sigma. apply inst_ext.
rewrite /rshiftk. rewrite (ren_shiftk (S n)).
rewrite -shiftn_Upn - !Upn_Upn. intros i; lia_f_equal.
- move: hnth.
case: (nth_error_app_context Γ Γ' _) ⇒ // x' hnth hn' [=] eq; subst x'.
× elimtype False.
revert subs hnth hb; generalize (n - #|Γ''|); clear.
intros n subs; induction subs in n |- *; simpl ⇒ //.
{ now rewrite nth_error_nil //. }
{ destruct n; simpl.
× intros [= <-] ⇒ //.
× intros hnth. now specialize (IHsubs _ hnth). }
× left; ∃ (n - #|Γ'|), decl.
repeat split.
+ rewrite Upn_eq /subst_consn nth_error_idsn_None //; try lia.
unfold subst_compose.
apply subs_length in subs.
rewrite (proj2 (nth_error_None _ _)); try (len; lia).
simpl. len. unfold shiftk. lia_f_equal.
+ rewrite nth_error_app_ge; len; try lia.
rewrite -hnth. lia_f_equal.
+ rewrite -lift_renaming_0_rshift hb /=.
f_equal. rewrite rename_inst. rewrite lift_renaming_spec shiftn0 ren_shiftk.
apply inst_ext.
apply subs_length in subs.
replace (S n) with ((S (n - #|Γ''|)) + #|Γ''|) by lia.
rewrite -shiftk_compose subst_compose_assoc.
rewrite shiftn_Upn -subst_compose_assoc.
replace (S (n - #|Γ''|)) with ((S (n - #|Γ''|) - #|Γ'|) + #|Γ'|) by lia.
rewrite -shiftk_compose !subst_compose_assoc.
rewrite -(subst_compose_assoc _ _ (↑^#|Γ''|)).
rewrite subst_consn_shiftn //.
rewrite !shiftk_compose. intros i; lia_f_equal.
Qed.
Lemma untyped_subslet_length {Γ s Δ} : untyped_subslet Γ s Δ → #|s| = #|Δ|.
Proof.
induction 1; simpl; lia.
Qed.
Lemma subslet_usubst {Γ Δ Γ' s} :
untyped_subslet Γ s Δ →
usubst (Γ,,, Δ,,, Γ') (⇑^#|Γ'| (s ⋅n ids)) (Γ,,, subst_context s 0 Γ').
Proof.
intros subs n decl.
case: (nth_error_app_context (Γ ,,, Δ) Γ' n) ⇒ // x hnth hlt [=] hx; subst x ⇒ b hb.
- left; eexists n, _.
split; auto.
× rewrite Upn_eq /subst_consn idsn_lt //.
× rewrite nth_error_app_lt; len ⇒ //.
change (rshiftk (S n)) with (lift_renaming (S n) 0).
rewrite nth_error_subst_context /= hnth /=. split; eauto.
rewrite /= hb /=. f_equal.
rewrite subst_inst. rewrite Nat.add_0_r.
rewrite rename_inst. rewrite ren_lift_renaming Upn_0.
replace #|Γ'| with ((#|Γ'| - S n) + S n) at 2 by lia.
set (k := S n).
sigma. apply inst_ext.
rewrite -shiftn_Upn - !Upn_Upn. intros i; lia_f_equal.
- move: hnth.
case: (nth_error_app_context Γ Δ _) ⇒ // x' hnth hn' [=] eq; subst x'.
× right.
pose proof (untyped_subslet_length subs).
rewrite Upn_eq {1}/subst_consn nth_error_idsn_None; try lia.
len. rewrite subst_consn_compose subst_consn_lt; len; try lia.
rewrite /subst_fn nth_error_map.
case: nth_error_spec; try lia. move⇒ x hs hns /=.
epose proof (untyped_subslet_nth_error _ _ _ _ _ _ subs hnth hs).
rewrite hb in X; rewrite X; cbn.
rewrite subst_inst Upn_0 inst_assoc. apply inst_ext.
(rewrite skipn_subst; try by lia); [].
rewrite !subst_compose_assoc.
rewrite subst_consn_compose. sigma.
rewrite -subst_compose_assoc -shiftk_shift -subst_compose_assoc.
rewrite -shiftk_shift.
(rewrite (shift_subst_consn_ge (S n)); try by len; lia); [].
now len.
× left; ∃ (n - #|s|), decl.
pose proof (untyped_subslet_length subs).
repeat split.
+ rewrite Upn_eq /subst_consn nth_error_idsn_None //; try lia.
unfold subst_compose.
rewrite (proj2 (nth_error_None _ _)); try (len; lia).
simpl. len. unfold shiftk. lia_f_equal.
+ rewrite nth_error_app_ge; len; try lia.
rewrite -hnth. lia_f_equal.
+ rewrite -lift_renaming_0_rshift hb /=.
f_equal; sigma.
apply inst_ext. rewrite -shiftk_shift.
rewrite - !subst_compose_assoc -shiftk_shift.
replace (S n) with ((S n - #|Γ'|) + #|Γ'|) by lia.
rewrite -shiftk_compose subst_compose_assoc shiftn_Upn.
replace (S n - #|Γ'|) with (S (n - #|Γ'| - #|s|) + #|s|) by lia.
rewrite -shiftk_compose subst_compose_assoc -(subst_compose_assoc (↑^#|s|)).
rewrite subst_consn_shiftn //. sigma.
rewrite -shiftk_shift. rewrite -shiftk_shift_l shiftk_compose.
now replace (n - #|Γ'| - #|s| + S #|Γ'|) with (S (n - #|s|)) by lia.
Qed.
Lemma subst_skipn {n s k t} : n ≤ #|s| → subst (skipn n s) k t = subst s k (lift n k t).
Proof.
intros Hn.
assert (#|firstn n s| = n) by (rewrite firstn_length_le; lia).
rewrite <- (firstn_skipn n s) at 2.
rewrite subst_app_simpl. rewrite H.
rewrite <- commut_lift_subst_rec; auto with arith.
rewrite -{3}H. now rewrite simpl_subst_k.
Qed.
Lemma subst_compare_term {cf:checker_flags} le Σ (φ : ConstraintSet.t) (l : list term) (k : nat) (T U : term) :
compare_term le Σ φ T U → compare_term le Σ φ (subst l k T) (subst l k U).
Proof.
destruct le; simpl.
- apply subst_eq_term.
- apply subst_leq_term.
Qed.
Lemma subst_compare_decl `{checker_flags} {le Σ ϕ l k d d'} :
compare_decl le Σ ϕ d d' → compare_decl le Σ ϕ (subst_decl l k d) (subst_decl l k d').
Proof.
intros []; constructor; auto; destruct le;
intuition eauto using subst_compare_term, subst_eq_term, subst_leq_term.
Qed.
Lemma subst_compare_context `{checker_flags} le Σ φ l l' n k :
compare_context le Σ φ l l' →
compare_context le Σ φ (subst_context n k l) (subst_context n k l').
Proof.
induction 1; rewrite ?subst_context_snoc /=; constructor; auto.
erewrite (All2_fold_length X). simpl.
apply (subst_compare_decl p).
Qed.
From Coq Require Import ssrbool.
Section CtxReduction.
Context {cf : checker_flags}.
Context {Σ : global_env}.
Context (wfΣ : wf Σ).
Lemma red_abs_alt Γ na M M' N N' : red Σ Γ M M' → red Σ (Γ ,, vass na M) N N' →
red Σ Γ (tLambda na M N) (tLambda na M' N').
Proof using Type.
intros. transitivity (tLambda na M N').
× now eapply (red_ctx_congr (tCtxLambda_r _ _ tCtxHole)).
× now eapply (red_ctx_congr (tCtxLambda_l _ tCtxHole _)).
Qed.
Lemma red_letin_alt Γ na d0 d1 t0 t1 b0 b1 :
red Σ Γ d0 d1 → red Σ Γ t0 t1 → red Σ (Γ ,, vdef na d0 t0) b0 b1 →
red Σ Γ (tLetIn na d0 t0 b0) (tLetIn na d1 t1 b1).
Proof using Type.
intros; transitivity (tLetIn na d0 t0 b1).
× now eapply (red_ctx_congr (tCtxLetIn_r _ _ _ tCtxHole)).
× transitivity (tLetIn na d0 t1 b1).
+ now eapply (red_ctx_congr (tCtxLetIn_b _ _ tCtxHole _)).
+ now apply (red_ctx_congr (tCtxLetIn_l _ tCtxHole _ _)).
Qed.
End CtxReduction.
Record wt_cumul_pb {cf} (c : conv_pb) Σ (Γ : context) T U :=
{ wt_cumul_pb_dom : isType Σ Γ T;
wt_cumul_pb_codom : isType Σ Γ U;
wt_cumul_pb_eq : cumulAlgo_gen Σ Γ c T U }.
Arguments wt_cumul_pb_dom {cf c Σ Γ T U}.
Arguments wt_cumul_pb_codom {cf c Σ Γ T U}.
Arguments wt_cumul_pb_eq {cf c Σ Γ T U}.
Definition wt_cumul {cf} := wt_cumul_pb Cumul.
Definition wt_conv {cf} := wt_cumul_pb Conv.
Notation " Σ ;;; Γ |- t <= u ✓" := (wt_cumul Σ Γ t u) (at level 50, Γ, t, u at next level).
Notation " Σ ;;; Γ |- t = u ✓" := (wt_conv Σ Γ t u) (at level 50, Γ, t, u at next level).
Definition wt_cumul_cum {cf} {Σ Γ T U} : Σ ;;; Γ |- T ≤ U ✓ → Σ ;;; Γ |- T ≤ U.
Proof. intros H. apply (wt_cumul_pb_eq H). Defined.
Coercion wt_cumul_cum : wt_cumul >-> cumulAlgo.
Definition wt_conv_conv {cf} {Σ Γ T U} : Σ ;;; Γ |- T = U ✓ → Σ ;;; Γ |- T = U.
Proof. intros H; apply (wt_cumul_pb_eq H). Defined.
Coercion wt_conv_conv : wt_conv >-> convAlgo.
Definition red1P P Σ Γ t v :=
on_ctx_free_vars P Γ × on_free_vars P t × red1 Σ Γ t v.
Definition red1P_red1 {P Σ Γ t v} : red1P P Σ Γ t v → red1 Σ Γ t v := fun x ⇒ x.2.2.
Definition red1P_on_free_vars_left {P Σ Γ t v} : red1P P Σ Γ t v → on_free_vars P t := fun x ⇒ x.2.1.
Definition red1P_on_free_vars_ctx {P Σ Γ t v} : red1P P Σ Γ t v → on_ctx_free_vars P Γ := fun x ⇒ x.1.
Definition red1P_on_free_vars_right {cf} {P Σ} {wfΣ : wf Σ} {Γ t v} : red1P P Σ Γ t v → on_free_vars P v.
Proof.
intros [onΓ [ont red]].
eapply red1_on_free_vars; tea.
Qed.
Reserved Notation " Σ ;;; Γ |-[ P ] t <=[ le ] u" (at level 50, Γ, t, u at next level,
format "Σ ;;; Γ |-[ P ] t <=[ le ] u").
Inductive cumulP {cf} (pb : conv_pb) (Σ : global_env_ext) (P : nat → bool) (Γ : context) : term → term → Type :=
| wt_cumul_refl t u : compare_term pb Σ.1 (global_ext_constraints Σ) t u → Σ ;;; Γ |-[P] t <=[pb] u
| wt_cumul_red_l t u v : red1P P Σ Γ t v → Σ ;;; Γ |-[P] v <=[pb] u → Σ ;;; Γ |-[P] t <=[pb] u
| wt_cumul_red_r t u v : Σ ;;; Γ |-[P] t <=[pb] v → red1P P Σ Γ u v → Σ ;;; Γ |-[P] t <=[pb] u
where " Σ ;;; Γ |-[ P ] t <=[ le ] u " := (cumulP le Σ P Γ t u) : type_scope.
Notation " Σ ;;; Γ |-[ P ] t <= u " := (cumulP Cumul Σ P Γ t u) (at level 50, Γ, t, u at next level,
format "Σ ;;; Γ |-[ P ] t <= u") : type_scope.
Notation " Σ ;;; Γ |-[ P ] t = u " := (cumulP Conv Σ P Γ t u) (at level 50, Γ, t, u at next level,
format "Σ ;;; Γ |-[ P ] t = u") : type_scope.
Lemma isType_wf_local {cf:checker_flags} {Σ Γ T} : isType Σ Γ T → wf_local Σ Γ.
Proof.
move⇒ [s Hs].
now eapply typing_wf_local.
Qed.
Lemma shiftnPF_closedPT (Γ : context) : shiftnP #|Γ| xpred0 =1 closedP #|Γ| xpredT.
Proof.
intros i; rewrite /shiftnP /closedP orb_false_r.
now destruct Nat.ltb.
Qed.
Section SubstitutionLemmas.
Context {cf} {Σ} {wfΣ : wf Σ}.
Lemma isType_closedPT Γ T : isType Σ Γ T → on_free_vars (closedP #|Γ| xpredT) T.
Proof using wfΣ.
move/isType_closed/(closedn_on_free_vars (P:=xpred0)).
now rewrite shiftnPF_closedPT.
Qed.
Lemma wt_cumul_pb_equalityP {le} {Γ : context} {T U} : wt_cumul_pb le Σ Γ T U → cumulP le Σ (closedP #|Γ| xpredT) Γ T U.
Proof using wfΣ.
move⇒ [] dom.
move: (isType_wf_local dom) ⇒ /closed_wf_local clΓ.
rewrite closed_ctx_on_ctx_free_vars in clΓ; tea.
move/isType_closedPT: dom ⇒ clT.
move/isType_closedPT ⇒ clU cum.
destruct le.
{ induction cum.
- constructor; auto.
- econstructor 2.
× econstructor; [|split]; tea.
× eapply IHcum ⇒ //.
now eapply red1_on_free_vars in r.
- econstructor 3.
× eapply IHcum ⇒ //.
now eapply red1_on_free_vars.
× econstructor; [|split]; tea. }
{ induction cum.
- constructor; auto.
- econstructor 2.
× econstructor; [|split]; tea.
× eapply IHcum ⇒ //.
now eapply red1_on_free_vars in r.
- econstructor 3.
× eapply IHcum ⇒ //.
now eapply red1_on_free_vars.
× econstructor; [|split]; tea. }
Qed.
Lemma substitution_red1 {Γ Γ' Γ'' s M N} :
subs Σ Γ s Γ' → wf_local Σ Γ →
is_open_term (Γ,,, Γ',,, Γ'') M →
red1 Σ (Γ ,,, Γ' ,,, Γ'') M N →
red Σ (Γ ,,, subst_context s 0 Γ'') (subst s #|Γ''| M) (subst s #|Γ''| N).
Proof using wfΣ.
intros Hs wfΓ H.
rewrite !subst_inst.
eapply red1_inst; eauto.
now eapply subs_usubst.
Qed.
Lemma substitution_let_red {Γ Δ Γ' s M N} :
subslet Σ Γ s Δ →
is_open_term (Γ,,, Δ,,, Γ') M →
red1 Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros Hs wfΓ H.
rewrite !subst_inst.
eapply red1_inst; eauto.
now eapply (subslet_usubst Hs).
Qed.
Lemma substitution_untyped_let_red {Γ Δ Γ' s M N} :
untyped_subslet Γ s Δ →
is_open_term (Γ,,, Δ,,, Γ') M →
red1 Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros Hs H.
rewrite !subst_inst.
eapply red1_inst; eauto.
now eapply subslet_usubst.
Qed.
Lemma substitution_untyped_red {Γ Δ Γ' s M N} :
untyped_subslet Γ s Δ →
is_open_term (Γ ,,, Δ ,,, Γ') M →
on_ctx_free_vars (shiftnP #|Γ,,, Δ,,, Γ'| xpred0) (Γ,,, Δ,,, Γ') →
red Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros subsl onM onΓ.
induction 1; trea.
- eapply substitution_untyped_let_red; eassumption.
- etransitivity; [eapply IHX1|eapply IHX2]; tea.
eapply red_on_free_vars in X1; tea.
Qed.
Lemma substitution_red {Γ Δ Γ' s M N} :
subslet Σ Γ s Δ → wf_local Σ Γ →
is_open_term (Γ ,,, Δ ,,, Γ') M →
on_ctx_free_vars (shiftnP #|Γ,,, Δ,,, Γ'| xpred0) (Γ,,, Δ,,, Γ') →
red Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros Hs Hl onM onctx Hred. induction Hred; trea.
- eapply substitution_let_red; eauto.
- etransitivity; [eapply IHHred1|eapply IHHred2]; tea.
eapply red_on_free_vars in Hred1; eauto.
Qed.
Ltac simpl_IHs :=
repeat match goal with
| [ H : ?A → ?B, H' : ?A |- _ ] ⇒
specialize (H H')
end.
Lemma subst_inst_case_context_wf s k pars puinst ctx :
test_context_k (fun k : nat ⇒ on_free_vars (closedP k xpredT)) #|pars| ctx →
subst_context s k (inst_case_context pars puinst ctx) =
inst_case_context (map (subst s k) pars) puinst ctx.
Proof using Type.
intros Hctx.
rewrite subst_context_inst_context.
rewrite inst_inst_case_context_wf //. f_equal.
apply map_ext ⇒ x. now rewrite subst_inst.
Qed.
Lemma on_ctx_free_vars_snoc p Γ d :
on_ctx_free_vars (shiftnP 1 p) (Γ ,, d) = on_ctx_free_vars p Γ && on_free_vars_decl p d.
Proof using Type.
now rewrite (on_ctx_free_vars_concat _ _ [_]) on_ctx_free_vars_tip /= addnP_shiftnP.
Qed.
Lemma addnP_shiftnP_k k n p : addnP (k + n) (shiftnP k p) =1 addnP n p.
Proof using Type.
now rewrite Nat.add_comm -addnP_add addnP_shiftnP.
Qed.
Lemma subst_context_app' s k Γ Δ :
subst_context s k (Γ ,,, Δ) = subst_context s k Γ ,,, subst_context s (k + #|Γ|) Δ.
Proof using Type.
rewrite subst_context_app. lia_f_equal.
Qed.
Lemma red_red {P Γ Δ Γ' s s' b} :
on_ctx_free_vars P (Γ ,,, Δ ,,, Γ') →
on_free_vars P b →
All2 (red Σ Γ) s s' →
All (on_free_vars (addnP (#|Γ'| + #|Δ|) P)) s →
untyped_subslet Γ s Δ →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| b) (subst s' #|Γ'| b).
Proof using wfΣ.
intros onΓ onb Hall ons Hsubs.
revert P b onb Γ Δ Γ' onΓ Hall Hsubs ons.
apply: term_on_free_vars_ind;
intros; match goal with
|- context [tRel _] ⇒ idtac
| |- _ ⇒ cbn -[plus]
end; try easy;
autorewrite with map;
rewrite ?Nat.add_assoc;
try solve [f_equal; auto; solve_all].
- unfold subst.
destruct (#|Γ'| <=? i) eqn:Heq.
+ destruct nth_error eqn:Heq'.
× destruct (All2_nth_error_Some _ _ Hall Heq') as [t' [-> Ptt']].
intros. relativize #|Γ'|; [eapply (weakening_red (Γ':=[]))|]; tea.
2:now eapply nth_error_all in ons; tea.
2:now len.
simpl.
rewrite !on_ctx_free_vars_app in onΓ.
setoid_rewrite addnP_add in onΓ.
rewrite Nat.add_comm in onΓ. now move/and3P: onΓ ⇒ [].
× rewrite (All2_nth_error_None _ Hall Heq').
apply All2_length in Hall as →. reflexivity.
+ reflexivity.
- apply red_evar. eapply All2_map, All_All2; tea. intuition auto.
specialize (X1 _ _ _ onΓ). now simpl_IHs.
- apply red_prod; eauto.
specialize (X0 Γ Δ (Γ' ,, vass na dom)).
rewrite subst_context_snoc Nat.add_0_r in X0. apply X0 ⇒ //.
× rewrite /= on_ctx_free_vars_snoc onΓ /=; auto with fvs.
× cbn. eapply (All_impl ons) ⇒ ?; now rewrite (addnP_shiftnP_k 1).
- apply red_abs_alt; eauto.
specialize (X0 Γ Δ (Γ' ,, vass na ty)).
rewrite subst_context_snoc Nat.add_0_r in X0. apply X0 ⇒ //.
× rewrite /= on_ctx_free_vars_snoc onΓ /=; auto with fvs.
× cbn. apply (All_impl ons) ⇒ ?; now rewrite (addnP_shiftnP_k 1).
- apply red_letin_alt; eauto.
specialize (X1 Γ Δ (Γ' ,, vdef na def ty)).
rewrite subst_context_snoc Nat.add_0_r in X1. apply X1 ⇒ //.
× rewrite /= on_ctx_free_vars_snoc onΓ /=; auto with fvs.
× cbn. apply (All_impl ons) ⇒ ?; now rewrite (addnP_shiftnP_k 1).
- apply red_app; eauto.
- eapply (red_case (p:=(map_predicate_k id (subst s) #|Γ'| pred))); simpl; solve_all.
× eapply All_All2; tea. solve_all. eapply b; eauto; solve_all.
× rewrite /map_predicate_k /= /PCUICCases.inst_case_predicate_context /=.
rewrite map_subst_inst.
rewrite -inst_inst_case_context_wf //.
{ rewrite test_context_k_closed_on_free_vars_ctx //. }
rewrite -subst_context_inst_context -app_context_assoc -(subst_context_app' _ 0).
relativize (_ + _); [eapply X2|]; tea; auto; len; solve_all.
{ rewrite !app_context_assoc.
relativize #|pcontext pred|; [erewrite on_ctx_free_vars_extend|]; len ⇒ //.
rewrite onΓ ⇒ /=.
eapply on_free_vars_ctx_inst_case_context; trea; revgoals.
{ erewrite test_context_k_closed_on_free_vars_ctx; tea. }
{ solve_all. } }
{ len. rewrite Nat.add_comm -addnP_add Nat.add_comm -addnP_add addnP_shiftnP addnP_add Nat.add_comm //. }
× eapply X3; eauto; solve_all.
× red. solve_all.
eapply All_All2; tea ⇒ /=. solve_all; unfold on_Trel; simpl.
+ rewrite /inst_case_branch_context /= map_subst_inst -inst_inst_case_context_wf //.
{ rewrite test_context_k_closed_on_free_vars_ctx //. apply X. }
rewrite -subst_context_inst_context -app_context_assoc -(subst_context_app' _ 0).
relativize (_ + _); [eapply X|]; tea; auto; len; solve_all.
{ rewrite !app_context_assoc.
relativize #|bcontext x|; [erewrite on_ctx_free_vars_extend|]; len ⇒ //.
rewrite onΓ ⇒ /=. eapply on_free_vars_ctx_inst_case_context; trea; solve_all.
erewrite test_context_k_closed_on_free_vars_ctx; tea. apply X. }
{ len. rewrite Nat.add_comm -addnP_add Nat.add_comm -addnP_add addnP_shiftnP addnP_add Nat.add_comm //. }
- apply red_proj_c; eauto.
- apply red_fix_congr; eauto.
solve_all. eapply All_All2; tea; simpl; solve_all.
× eapply a; tea; solve_all.
× rewrite subst_fix_context.
specialize (b1 Γ Δ (Γ' ,,, (fix_context m))).
rewrite (subst_context_app' _ 0) !app_context_assoc /= in b1. len in b1.
eapply b1; eauto; len; solve_all.
{ relativize #|m|; [erewrite on_ctx_free_vars_extend|]; len ⇒ //.
rewrite onΓ. apply on_free_vars_fix_context. rewrite /test_def. solve_all.
now len in b2. }
now rewrite -Nat.add_assoc addnP_shiftnP_k.
- apply red_cofix_congr; eauto.
solve_all. eapply All_All2; tea; simpl; solve_all.
× eapply a; tea; solve_all.
× rewrite subst_fix_context.
specialize (b1 Γ Δ (Γ' ,,, (fix_context m))).
rewrite (subst_context_app' _ 0) !app_context_assoc /= in b1. len in b1.
eapply b1; eauto; len; solve_all.
{ relativize #|m|; [erewrite on_ctx_free_vars_extend|]; len ⇒ //.
rewrite onΓ. apply on_free_vars_fix_context. rewrite /test_def. solve_all.
now len in b2. }
now rewrite -Nat.add_assoc addnP_shiftnP_k.
Qed.
Lemma untyped_substitution_red {Γ Δ Γ' s M N} :
untyped_subslet Γ s Δ →
on_ctx_free_vars (shiftnP #|Γ,,, Δ,,, Γ'| xpred0) (Γ ,,, Δ ,,, Γ') →
is_open_term (Γ ,,, Δ ,,, Γ') M →
red Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros Hs onΓ onM Hred. induction Hred; trea.
- eapply substitution_untyped_let_red; eauto.
- etransitivity; [eapply IHHred1|eapply IHHred2]; eauto.
eapply red_on_free_vars in Hred1; tea.
Qed.
subs Σ Γ s Γ' →
usubst (Γ,,, Γ',,, Γ'') (⇑^#|Γ''| (s ⋅n ids)) (Γ,,, subst_context s 0 Γ'').
Proof.
intros subs n decl.
case: (nth_error_app_context (Γ ,,, Γ') Γ'' n) ⇒ // x hnth hlt [=] hx; subst x ⇒ b hb.
- left; eexists n, _.
split; auto.
× rewrite Upn_eq /subst_consn idsn_lt //.
× rewrite nth_error_app_lt; len ⇒ //.
change (fun m ⇒ S (n + m)) with (lift_renaming (S n) 0).
rewrite nth_error_subst_context /= hnth /=. split; eauto.
rewrite /= hb /=. f_equal.
rewrite subst_inst. rewrite Nat.add_0_r.
rewrite rename_inst.
replace #|Γ''| with ((#|Γ''| - S n) + S n) at 2 by lia.
set (k := S n).
sigma. apply inst_ext.
rewrite /rshiftk. rewrite (ren_shiftk (S n)).
rewrite -shiftn_Upn - !Upn_Upn. intros i; lia_f_equal.
- move: hnth.
case: (nth_error_app_context Γ Γ' _) ⇒ // x' hnth hn' [=] eq; subst x'.
× elimtype False.
revert subs hnth hb; generalize (n - #|Γ''|); clear.
intros n subs; induction subs in n |- *; simpl ⇒ //.
{ now rewrite nth_error_nil //. }
{ destruct n; simpl.
× intros [= <-] ⇒ //.
× intros hnth. now specialize (IHsubs _ hnth). }
× left; ∃ (n - #|Γ'|), decl.
repeat split.
+ rewrite Upn_eq /subst_consn nth_error_idsn_None //; try lia.
unfold subst_compose.
apply subs_length in subs.
rewrite (proj2 (nth_error_None _ _)); try (len; lia).
simpl. len. unfold shiftk. lia_f_equal.
+ rewrite nth_error_app_ge; len; try lia.
rewrite -hnth. lia_f_equal.
+ rewrite -lift_renaming_0_rshift hb /=.
f_equal. rewrite rename_inst. rewrite lift_renaming_spec shiftn0 ren_shiftk.
apply inst_ext.
apply subs_length in subs.
replace (S n) with ((S (n - #|Γ''|)) + #|Γ''|) by lia.
rewrite -shiftk_compose subst_compose_assoc.
rewrite shiftn_Upn -subst_compose_assoc.
replace (S (n - #|Γ''|)) with ((S (n - #|Γ''|) - #|Γ'|) + #|Γ'|) by lia.
rewrite -shiftk_compose !subst_compose_assoc.
rewrite -(subst_compose_assoc _ _ (↑^#|Γ''|)).
rewrite subst_consn_shiftn //.
rewrite !shiftk_compose. intros i; lia_f_equal.
Qed.
Lemma untyped_subslet_length {Γ s Δ} : untyped_subslet Γ s Δ → #|s| = #|Δ|.
Proof.
induction 1; simpl; lia.
Qed.
Lemma subslet_usubst {Γ Δ Γ' s} :
untyped_subslet Γ s Δ →
usubst (Γ,,, Δ,,, Γ') (⇑^#|Γ'| (s ⋅n ids)) (Γ,,, subst_context s 0 Γ').
Proof.
intros subs n decl.
case: (nth_error_app_context (Γ ,,, Δ) Γ' n) ⇒ // x hnth hlt [=] hx; subst x ⇒ b hb.
- left; eexists n, _.
split; auto.
× rewrite Upn_eq /subst_consn idsn_lt //.
× rewrite nth_error_app_lt; len ⇒ //.
change (rshiftk (S n)) with (lift_renaming (S n) 0).
rewrite nth_error_subst_context /= hnth /=. split; eauto.
rewrite /= hb /=. f_equal.
rewrite subst_inst. rewrite Nat.add_0_r.
rewrite rename_inst. rewrite ren_lift_renaming Upn_0.
replace #|Γ'| with ((#|Γ'| - S n) + S n) at 2 by lia.
set (k := S n).
sigma. apply inst_ext.
rewrite -shiftn_Upn - !Upn_Upn. intros i; lia_f_equal.
- move: hnth.
case: (nth_error_app_context Γ Δ _) ⇒ // x' hnth hn' [=] eq; subst x'.
× right.
pose proof (untyped_subslet_length subs).
rewrite Upn_eq {1}/subst_consn nth_error_idsn_None; try lia.
len. rewrite subst_consn_compose subst_consn_lt; len; try lia.
rewrite /subst_fn nth_error_map.
case: nth_error_spec; try lia. move⇒ x hs hns /=.
epose proof (untyped_subslet_nth_error _ _ _ _ _ _ subs hnth hs).
rewrite hb in X; rewrite X; cbn.
rewrite subst_inst Upn_0 inst_assoc. apply inst_ext.
(rewrite skipn_subst; try by lia); [].
rewrite !subst_compose_assoc.
rewrite subst_consn_compose. sigma.
rewrite -subst_compose_assoc -shiftk_shift -subst_compose_assoc.
rewrite -shiftk_shift.
(rewrite (shift_subst_consn_ge (S n)); try by len; lia); [].
now len.
× left; ∃ (n - #|s|), decl.
pose proof (untyped_subslet_length subs).
repeat split.
+ rewrite Upn_eq /subst_consn nth_error_idsn_None //; try lia.
unfold subst_compose.
rewrite (proj2 (nth_error_None _ _)); try (len; lia).
simpl. len. unfold shiftk. lia_f_equal.
+ rewrite nth_error_app_ge; len; try lia.
rewrite -hnth. lia_f_equal.
+ rewrite -lift_renaming_0_rshift hb /=.
f_equal; sigma.
apply inst_ext. rewrite -shiftk_shift.
rewrite - !subst_compose_assoc -shiftk_shift.
replace (S n) with ((S n - #|Γ'|) + #|Γ'|) by lia.
rewrite -shiftk_compose subst_compose_assoc shiftn_Upn.
replace (S n - #|Γ'|) with (S (n - #|Γ'| - #|s|) + #|s|) by lia.
rewrite -shiftk_compose subst_compose_assoc -(subst_compose_assoc (↑^#|s|)).
rewrite subst_consn_shiftn //. sigma.
rewrite -shiftk_shift. rewrite -shiftk_shift_l shiftk_compose.
now replace (n - #|Γ'| - #|s| + S #|Γ'|) with (S (n - #|s|)) by lia.
Qed.
Lemma subst_skipn {n s k t} : n ≤ #|s| → subst (skipn n s) k t = subst s k (lift n k t).
Proof.
intros Hn.
assert (#|firstn n s| = n) by (rewrite firstn_length_le; lia).
rewrite <- (firstn_skipn n s) at 2.
rewrite subst_app_simpl. rewrite H.
rewrite <- commut_lift_subst_rec; auto with arith.
rewrite -{3}H. now rewrite simpl_subst_k.
Qed.
Lemma subst_compare_term {cf:checker_flags} le Σ (φ : ConstraintSet.t) (l : list term) (k : nat) (T U : term) :
compare_term le Σ φ T U → compare_term le Σ φ (subst l k T) (subst l k U).
Proof.
destruct le; simpl.
- apply subst_eq_term.
- apply subst_leq_term.
Qed.
Lemma subst_compare_decl `{checker_flags} {le Σ ϕ l k d d'} :
compare_decl le Σ ϕ d d' → compare_decl le Σ ϕ (subst_decl l k d) (subst_decl l k d').
Proof.
intros []; constructor; auto; destruct le;
intuition eauto using subst_compare_term, subst_eq_term, subst_leq_term.
Qed.
Lemma subst_compare_context `{checker_flags} le Σ φ l l' n k :
compare_context le Σ φ l l' →
compare_context le Σ φ (subst_context n k l) (subst_context n k l').
Proof.
induction 1; rewrite ?subst_context_snoc /=; constructor; auto.
erewrite (All2_fold_length X). simpl.
apply (subst_compare_decl p).
Qed.
From Coq Require Import ssrbool.
Section CtxReduction.
Context {cf : checker_flags}.
Context {Σ : global_env}.
Context (wfΣ : wf Σ).
Lemma red_abs_alt Γ na M M' N N' : red Σ Γ M M' → red Σ (Γ ,, vass na M) N N' →
red Σ Γ (tLambda na M N) (tLambda na M' N').
Proof using Type.
intros. transitivity (tLambda na M N').
× now eapply (red_ctx_congr (tCtxLambda_r _ _ tCtxHole)).
× now eapply (red_ctx_congr (tCtxLambda_l _ tCtxHole _)).
Qed.
Lemma red_letin_alt Γ na d0 d1 t0 t1 b0 b1 :
red Σ Γ d0 d1 → red Σ Γ t0 t1 → red Σ (Γ ,, vdef na d0 t0) b0 b1 →
red Σ Γ (tLetIn na d0 t0 b0) (tLetIn na d1 t1 b1).
Proof using Type.
intros; transitivity (tLetIn na d0 t0 b1).
× now eapply (red_ctx_congr (tCtxLetIn_r _ _ _ tCtxHole)).
× transitivity (tLetIn na d0 t1 b1).
+ now eapply (red_ctx_congr (tCtxLetIn_b _ _ tCtxHole _)).
+ now apply (red_ctx_congr (tCtxLetIn_l _ tCtxHole _ _)).
Qed.
End CtxReduction.
Record wt_cumul_pb {cf} (c : conv_pb) Σ (Γ : context) T U :=
{ wt_cumul_pb_dom : isType Σ Γ T;
wt_cumul_pb_codom : isType Σ Γ U;
wt_cumul_pb_eq : cumulAlgo_gen Σ Γ c T U }.
Arguments wt_cumul_pb_dom {cf c Σ Γ T U}.
Arguments wt_cumul_pb_codom {cf c Σ Γ T U}.
Arguments wt_cumul_pb_eq {cf c Σ Γ T U}.
Definition wt_cumul {cf} := wt_cumul_pb Cumul.
Definition wt_conv {cf} := wt_cumul_pb Conv.
Notation " Σ ;;; Γ |- t <= u ✓" := (wt_cumul Σ Γ t u) (at level 50, Γ, t, u at next level).
Notation " Σ ;;; Γ |- t = u ✓" := (wt_conv Σ Γ t u) (at level 50, Γ, t, u at next level).
Definition wt_cumul_cum {cf} {Σ Γ T U} : Σ ;;; Γ |- T ≤ U ✓ → Σ ;;; Γ |- T ≤ U.
Proof. intros H. apply (wt_cumul_pb_eq H). Defined.
Coercion wt_cumul_cum : wt_cumul >-> cumulAlgo.
Definition wt_conv_conv {cf} {Σ Γ T U} : Σ ;;; Γ |- T = U ✓ → Σ ;;; Γ |- T = U.
Proof. intros H; apply (wt_cumul_pb_eq H). Defined.
Coercion wt_conv_conv : wt_conv >-> convAlgo.
Definition red1P P Σ Γ t v :=
on_ctx_free_vars P Γ × on_free_vars P t × red1 Σ Γ t v.
Definition red1P_red1 {P Σ Γ t v} : red1P P Σ Γ t v → red1 Σ Γ t v := fun x ⇒ x.2.2.
Definition red1P_on_free_vars_left {P Σ Γ t v} : red1P P Σ Γ t v → on_free_vars P t := fun x ⇒ x.2.1.
Definition red1P_on_free_vars_ctx {P Σ Γ t v} : red1P P Σ Γ t v → on_ctx_free_vars P Γ := fun x ⇒ x.1.
Definition red1P_on_free_vars_right {cf} {P Σ} {wfΣ : wf Σ} {Γ t v} : red1P P Σ Γ t v → on_free_vars P v.
Proof.
intros [onΓ [ont red]].
eapply red1_on_free_vars; tea.
Qed.
Reserved Notation " Σ ;;; Γ |-[ P ] t <=[ le ] u" (at level 50, Γ, t, u at next level,
format "Σ ;;; Γ |-[ P ] t <=[ le ] u").
Inductive cumulP {cf} (pb : conv_pb) (Σ : global_env_ext) (P : nat → bool) (Γ : context) : term → term → Type :=
| wt_cumul_refl t u : compare_term pb Σ.1 (global_ext_constraints Σ) t u → Σ ;;; Γ |-[P] t <=[pb] u
| wt_cumul_red_l t u v : red1P P Σ Γ t v → Σ ;;; Γ |-[P] v <=[pb] u → Σ ;;; Γ |-[P] t <=[pb] u
| wt_cumul_red_r t u v : Σ ;;; Γ |-[P] t <=[pb] v → red1P P Σ Γ u v → Σ ;;; Γ |-[P] t <=[pb] u
where " Σ ;;; Γ |-[ P ] t <=[ le ] u " := (cumulP le Σ P Γ t u) : type_scope.
Notation " Σ ;;; Γ |-[ P ] t <= u " := (cumulP Cumul Σ P Γ t u) (at level 50, Γ, t, u at next level,
format "Σ ;;; Γ |-[ P ] t <= u") : type_scope.
Notation " Σ ;;; Γ |-[ P ] t = u " := (cumulP Conv Σ P Γ t u) (at level 50, Γ, t, u at next level,
format "Σ ;;; Γ |-[ P ] t = u") : type_scope.
Lemma isType_wf_local {cf:checker_flags} {Σ Γ T} : isType Σ Γ T → wf_local Σ Γ.
Proof.
move⇒ [s Hs].
now eapply typing_wf_local.
Qed.
Lemma shiftnPF_closedPT (Γ : context) : shiftnP #|Γ| xpred0 =1 closedP #|Γ| xpredT.
Proof.
intros i; rewrite /shiftnP /closedP orb_false_r.
now destruct Nat.ltb.
Qed.
Section SubstitutionLemmas.
Context {cf} {Σ} {wfΣ : wf Σ}.
Lemma isType_closedPT Γ T : isType Σ Γ T → on_free_vars (closedP #|Γ| xpredT) T.
Proof using wfΣ.
move/isType_closed/(closedn_on_free_vars (P:=xpred0)).
now rewrite shiftnPF_closedPT.
Qed.
Lemma wt_cumul_pb_equalityP {le} {Γ : context} {T U} : wt_cumul_pb le Σ Γ T U → cumulP le Σ (closedP #|Γ| xpredT) Γ T U.
Proof using wfΣ.
move⇒ [] dom.
move: (isType_wf_local dom) ⇒ /closed_wf_local clΓ.
rewrite closed_ctx_on_ctx_free_vars in clΓ; tea.
move/isType_closedPT: dom ⇒ clT.
move/isType_closedPT ⇒ clU cum.
destruct le.
{ induction cum.
- constructor; auto.
- econstructor 2.
× econstructor; [|split]; tea.
× eapply IHcum ⇒ //.
now eapply red1_on_free_vars in r.
- econstructor 3.
× eapply IHcum ⇒ //.
now eapply red1_on_free_vars.
× econstructor; [|split]; tea. }
{ induction cum.
- constructor; auto.
- econstructor 2.
× econstructor; [|split]; tea.
× eapply IHcum ⇒ //.
now eapply red1_on_free_vars in r.
- econstructor 3.
× eapply IHcum ⇒ //.
now eapply red1_on_free_vars.
× econstructor; [|split]; tea. }
Qed.
Lemma substitution_red1 {Γ Γ' Γ'' s M N} :
subs Σ Γ s Γ' → wf_local Σ Γ →
is_open_term (Γ,,, Γ',,, Γ'') M →
red1 Σ (Γ ,,, Γ' ,,, Γ'') M N →
red Σ (Γ ,,, subst_context s 0 Γ'') (subst s #|Γ''| M) (subst s #|Γ''| N).
Proof using wfΣ.
intros Hs wfΓ H.
rewrite !subst_inst.
eapply red1_inst; eauto.
now eapply subs_usubst.
Qed.
Lemma substitution_let_red {Γ Δ Γ' s M N} :
subslet Σ Γ s Δ →
is_open_term (Γ,,, Δ,,, Γ') M →
red1 Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros Hs wfΓ H.
rewrite !subst_inst.
eapply red1_inst; eauto.
now eapply (subslet_usubst Hs).
Qed.
Lemma substitution_untyped_let_red {Γ Δ Γ' s M N} :
untyped_subslet Γ s Δ →
is_open_term (Γ,,, Δ,,, Γ') M →
red1 Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros Hs H.
rewrite !subst_inst.
eapply red1_inst; eauto.
now eapply subslet_usubst.
Qed.
Lemma substitution_untyped_red {Γ Δ Γ' s M N} :
untyped_subslet Γ s Δ →
is_open_term (Γ ,,, Δ ,,, Γ') M →
on_ctx_free_vars (shiftnP #|Γ,,, Δ,,, Γ'| xpred0) (Γ,,, Δ,,, Γ') →
red Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros subsl onM onΓ.
induction 1; trea.
- eapply substitution_untyped_let_red; eassumption.
- etransitivity; [eapply IHX1|eapply IHX2]; tea.
eapply red_on_free_vars in X1; tea.
Qed.
Lemma substitution_red {Γ Δ Γ' s M N} :
subslet Σ Γ s Δ → wf_local Σ Γ →
is_open_term (Γ ,,, Δ ,,, Γ') M →
on_ctx_free_vars (shiftnP #|Γ,,, Δ,,, Γ'| xpred0) (Γ,,, Δ,,, Γ') →
red Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros Hs Hl onM onctx Hred. induction Hred; trea.
- eapply substitution_let_red; eauto.
- etransitivity; [eapply IHHred1|eapply IHHred2]; tea.
eapply red_on_free_vars in Hred1; eauto.
Qed.
Ltac simpl_IHs :=
repeat match goal with
| [ H : ?A → ?B, H' : ?A |- _ ] ⇒
specialize (H H')
end.
Lemma subst_inst_case_context_wf s k pars puinst ctx :
test_context_k (fun k : nat ⇒ on_free_vars (closedP k xpredT)) #|pars| ctx →
subst_context s k (inst_case_context pars puinst ctx) =
inst_case_context (map (subst s k) pars) puinst ctx.
Proof using Type.
intros Hctx.
rewrite subst_context_inst_context.
rewrite inst_inst_case_context_wf //. f_equal.
apply map_ext ⇒ x. now rewrite subst_inst.
Qed.
Lemma on_ctx_free_vars_snoc p Γ d :
on_ctx_free_vars (shiftnP 1 p) (Γ ,, d) = on_ctx_free_vars p Γ && on_free_vars_decl p d.
Proof using Type.
now rewrite (on_ctx_free_vars_concat _ _ [_]) on_ctx_free_vars_tip /= addnP_shiftnP.
Qed.
Lemma addnP_shiftnP_k k n p : addnP (k + n) (shiftnP k p) =1 addnP n p.
Proof using Type.
now rewrite Nat.add_comm -addnP_add addnP_shiftnP.
Qed.
Lemma subst_context_app' s k Γ Δ :
subst_context s k (Γ ,,, Δ) = subst_context s k Γ ,,, subst_context s (k + #|Γ|) Δ.
Proof using Type.
rewrite subst_context_app. lia_f_equal.
Qed.
Lemma red_red {P Γ Δ Γ' s s' b} :
on_ctx_free_vars P (Γ ,,, Δ ,,, Γ') →
on_free_vars P b →
All2 (red Σ Γ) s s' →
All (on_free_vars (addnP (#|Γ'| + #|Δ|) P)) s →
untyped_subslet Γ s Δ →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| b) (subst s' #|Γ'| b).
Proof using wfΣ.
intros onΓ onb Hall ons Hsubs.
revert P b onb Γ Δ Γ' onΓ Hall Hsubs ons.
apply: term_on_free_vars_ind;
intros; match goal with
|- context [tRel _] ⇒ idtac
| |- _ ⇒ cbn -[plus]
end; try easy;
autorewrite with map;
rewrite ?Nat.add_assoc;
try solve [f_equal; auto; solve_all].
- unfold subst.
destruct (#|Γ'| <=? i) eqn:Heq.
+ destruct nth_error eqn:Heq'.
× destruct (All2_nth_error_Some _ _ Hall Heq') as [t' [-> Ptt']].
intros. relativize #|Γ'|; [eapply (weakening_red (Γ':=[]))|]; tea.
2:now eapply nth_error_all in ons; tea.
2:now len.
simpl.
rewrite !on_ctx_free_vars_app in onΓ.
setoid_rewrite addnP_add in onΓ.
rewrite Nat.add_comm in onΓ. now move/and3P: onΓ ⇒ [].
× rewrite (All2_nth_error_None _ Hall Heq').
apply All2_length in Hall as →. reflexivity.
+ reflexivity.
- apply red_evar. eapply All2_map, All_All2; tea. intuition auto.
specialize (X1 _ _ _ onΓ). now simpl_IHs.
- apply red_prod; eauto.
specialize (X0 Γ Δ (Γ' ,, vass na dom)).
rewrite subst_context_snoc Nat.add_0_r in X0. apply X0 ⇒ //.
× rewrite /= on_ctx_free_vars_snoc onΓ /=; auto with fvs.
× cbn. eapply (All_impl ons) ⇒ ?; now rewrite (addnP_shiftnP_k 1).
- apply red_abs_alt; eauto.
specialize (X0 Γ Δ (Γ' ,, vass na ty)).
rewrite subst_context_snoc Nat.add_0_r in X0. apply X0 ⇒ //.
× rewrite /= on_ctx_free_vars_snoc onΓ /=; auto with fvs.
× cbn. apply (All_impl ons) ⇒ ?; now rewrite (addnP_shiftnP_k 1).
- apply red_letin_alt; eauto.
specialize (X1 Γ Δ (Γ' ,, vdef na def ty)).
rewrite subst_context_snoc Nat.add_0_r in X1. apply X1 ⇒ //.
× rewrite /= on_ctx_free_vars_snoc onΓ /=; auto with fvs.
× cbn. apply (All_impl ons) ⇒ ?; now rewrite (addnP_shiftnP_k 1).
- apply red_app; eauto.
- eapply (red_case (p:=(map_predicate_k id (subst s) #|Γ'| pred))); simpl; solve_all.
× eapply All_All2; tea. solve_all. eapply b; eauto; solve_all.
× rewrite /map_predicate_k /= /PCUICCases.inst_case_predicate_context /=.
rewrite map_subst_inst.
rewrite -inst_inst_case_context_wf //.
{ rewrite test_context_k_closed_on_free_vars_ctx //. }
rewrite -subst_context_inst_context -app_context_assoc -(subst_context_app' _ 0).
relativize (_ + _); [eapply X2|]; tea; auto; len; solve_all.
{ rewrite !app_context_assoc.
relativize #|pcontext pred|; [erewrite on_ctx_free_vars_extend|]; len ⇒ //.
rewrite onΓ ⇒ /=.
eapply on_free_vars_ctx_inst_case_context; trea; revgoals.
{ erewrite test_context_k_closed_on_free_vars_ctx; tea. }
{ solve_all. } }
{ len. rewrite Nat.add_comm -addnP_add Nat.add_comm -addnP_add addnP_shiftnP addnP_add Nat.add_comm //. }
× eapply X3; eauto; solve_all.
× red. solve_all.
eapply All_All2; tea ⇒ /=. solve_all; unfold on_Trel; simpl.
+ rewrite /inst_case_branch_context /= map_subst_inst -inst_inst_case_context_wf //.
{ rewrite test_context_k_closed_on_free_vars_ctx //. apply X. }
rewrite -subst_context_inst_context -app_context_assoc -(subst_context_app' _ 0).
relativize (_ + _); [eapply X|]; tea; auto; len; solve_all.
{ rewrite !app_context_assoc.
relativize #|bcontext x|; [erewrite on_ctx_free_vars_extend|]; len ⇒ //.
rewrite onΓ ⇒ /=. eapply on_free_vars_ctx_inst_case_context; trea; solve_all.
erewrite test_context_k_closed_on_free_vars_ctx; tea. apply X. }
{ len. rewrite Nat.add_comm -addnP_add Nat.add_comm -addnP_add addnP_shiftnP addnP_add Nat.add_comm //. }
- apply red_proj_c; eauto.
- apply red_fix_congr; eauto.
solve_all. eapply All_All2; tea; simpl; solve_all.
× eapply a; tea; solve_all.
× rewrite subst_fix_context.
specialize (b1 Γ Δ (Γ' ,,, (fix_context m))).
rewrite (subst_context_app' _ 0) !app_context_assoc /= in b1. len in b1.
eapply b1; eauto; len; solve_all.
{ relativize #|m|; [erewrite on_ctx_free_vars_extend|]; len ⇒ //.
rewrite onΓ. apply on_free_vars_fix_context. rewrite /test_def. solve_all.
now len in b2. }
now rewrite -Nat.add_assoc addnP_shiftnP_k.
- apply red_cofix_congr; eauto.
solve_all. eapply All_All2; tea; simpl; solve_all.
× eapply a; tea; solve_all.
× rewrite subst_fix_context.
specialize (b1 Γ Δ (Γ' ,,, (fix_context m))).
rewrite (subst_context_app' _ 0) !app_context_assoc /= in b1. len in b1.
eapply b1; eauto; len; solve_all.
{ relativize #|m|; [erewrite on_ctx_free_vars_extend|]; len ⇒ //.
rewrite onΓ. apply on_free_vars_fix_context. rewrite /test_def. solve_all.
now len in b2. }
now rewrite -Nat.add_assoc addnP_shiftnP_k.
Qed.
Lemma untyped_substitution_red {Γ Δ Γ' s M N} :
untyped_subslet Γ s Δ →
on_ctx_free_vars (shiftnP #|Γ,,, Δ,,, Γ'| xpred0) (Γ ,,, Δ ,,, Γ') →
is_open_term (Γ ,,, Δ ,,, Γ') M →
red Σ (Γ ,,, Δ ,,, Γ') M N →
red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).
Proof using wfΣ.
intros Hs onΓ onM Hred. induction Hred; trea.
- eapply substitution_untyped_let_red; eauto.
- etransitivity; [eapply IHHred1|eapply IHHred2]; eauto.
eapply red_on_free_vars in Hred1; tea.
Qed.
The cumulativity relation is substitutive, yay!
Lemma substitution_untyped_cumul {Γ Γ' Γ'' s M N} :
untyped_subslet Γ s Γ' →
is_open_term (Γ ,,, Γ' ,,, Γ'') M →
is_open_term (Γ ,,, Γ' ,,, Γ'') N →
on_ctx_free_vars (shiftnP #|Γ ,,, Γ' ,,, Γ''| xpred0) (Γ ,,, Γ' ,,, Γ'') →
Σ ;;; Γ ,,, Γ' ,,, Γ'' |- M ≤ N →
Σ ;;; Γ ,,, subst_context s 0 Γ'' |- subst s #|Γ''| M ≤ subst s #|Γ''| N.
Proof using wfΣ.
intros Hs onN onM onΓ h. induction h.
- constructor.
now apply subst_leq_term.
- epose proof (substitution_untyped_let_red Hs onN r); tea.
eapply red_cumul_cumul; eauto.
eapply IHh; tea. eapply red1_on_free_vars in r; tea.
- epose proof (substitution_untyped_let_red Hs onM r).
eapply red_cumul_cumul_inv; eauto.
eapply IHh; tea. eapply red1_on_free_vars in r; tea.
Qed.
Lemma substitution_cumul0 {Γ na t u u' a} :
on_ctx_free_vars (shiftnP #|Γ ,, vass na t| xpred0) (Γ ,, vass na t) →
is_open_term (Γ ,, vass na t) u →
is_open_term (Γ ,, vass na t) u' →
Σ ;;; Γ ,, vass na t |- u ≤ u' →
Σ ;;; Γ |- subst10 a u ≤ subst10 a u'.
Proof using wfΣ.
move⇒ onΓ onu onu' Hu.
pose proof (@substitution_untyped_cumul Γ [vass na t] [] [a] u u').
forward X.
{ constructor. constructor. }
simpl in X. now apply X.
Qed.
Lemma substitution_cumul_let {Γ na t ty u u'} :
on_ctx_free_vars (shiftnP #|Γ ,, vdef na t ty| xpred0) (Γ ,, vdef na t ty) →
is_open_term (Γ ,, vdef na t ty) u →
is_open_term (Γ ,, vdef na t ty) u' →
Σ ;;; Γ ,, vdef na t ty |- u ≤ u' →
Σ ;;; Γ |- subst10 t u ≤ subst10 t u'.
Proof using wfΣ.
move⇒ onΓ onu onu' Hu.
pose proof (@substitution_untyped_cumul Γ [vdef na t ty] [] [t] u u').
forward X.
{ rewrite - {1}(subst_empty 0 t). constructor. constructor. }
simpl in X. now apply X.
Qed.
Lemma usubst_well_subst {Γ σ Δ} :
usubst Γ σ Δ →
(∀ x decl, nth_error Γ x = Some decl →
Σ ;;; Δ |- σ x : (decl.(decl_type)).[↑^(S x) ∘s σ]) →
well_subst Σ Γ σ Δ.
Proof using Type.
intros us hty. split; eauto.
intros x decl hnth. specialize (hty x decl hnth). now sigma.
Qed.
Lemma subslet_well_subst {Γ Γ' s Δ} :
subslet Σ Γ s Γ' →
wf_local Σ (Γ ,,, subst_context s 0 Δ) →
well_subst Σ (Γ ,,, Γ' ,,, Δ) (⇑^#|Δ| (s ⋅n ids)) (Γ ,,, subst_context s 0 Δ).
Proof using wfΣ.
intros hs hsΔ.
apply usubst_well_subst.
× apply (subslet_usubst hs).
× intros x decl.
case: nth_error_app_context ⇒ //.
{ intros d hnth hn [= ->].
rewrite {1}Upn_eq subst_consn_lt; len ⇒ //. rewrite /subst_fn.
rewrite idsn_lt //.
eapply meta_conv.
- econstructor; auto.
rewrite nth_error_app_lt; len ⇒ //.
now rewrite nth_error_subst_context hnth.
- rewrite /subst_decl. simpl.
sigma. rewrite -shiftk_shift -subst_compose_assoc -shiftk_shift.
rewrite subst_shift_comm.
rewrite -subst_fn_subst_consn. lia_f_equal. }
{ intros n hnth; len; intros hd [= ->].
pose proof (subslet_length hs).
move: hnth; case: nth_error_app_context ⇒ //.
× intros n hnth hx [= ->].
rewrite {1}Upn_eq subst_consn_ge; len ⇒ //; try lia.
rewrite subst_consn_compose.
rewrite subst_consn_lt; len; try lia.
unfold subst_fn. rewrite nth_error_map.
destruct (subslet_nth_error hs hnth) as [t [hnths [hty hb]]].
rewrite hnths /=. sigma in hty.
eapply meta_conv in hty.
2:now rewrite skipn_subst ?Upn_0; try lia.
eapply (shift_typing (Δ := subst_context s 0 Δ)) in hty.
2:tas.
2:now len.
rewrite inst_assoc in hty.
rewrite Upn_eq.
eapply meta_conv; eauto.
eapply inst_ext.
rewrite (shift_subst_consn_ge (S x)); len; try lia.
rewrite subst_compose_assoc.
now replace (S x - #|Δ|) with (S (x - #|Δ|)) by lia.
× intros n hnth hn [= ->].
eapply meta_conv_all.
2:reflexivity.
2:{ rewrite Upn_subst_consn_ge; try lia. rewrite compose_ids_l.
instantiate (1 := tRel (x - #|s|)).
rewrite /shiftk. lia_f_equal. }
2:{ econstructor; eauto. }
eapply meta_conv.
{ econstructor; tas.
rewrite nth_error_app_context_ge; len; try lia.
rewrite H. erewrite <- hnth. lia_f_equal. }
rewrite lift0_inst.
rewrite Upn_eq.
rewrite shift_subst_consn_ge; len; try lia.
rewrite subst_consn_compose shift_subst_consn_ge; len; try lia.
rewrite H. rewrite shiftk_compose. lia_f_equal.
}
Qed.
Lemma All_local_env_inst {Γ0 Γ' Δ s} :
All_local_env
(lift_typing
(fun (Σ : global_env_ext) (Γ : context) (t T : term) ⇒
∀ (Δ : PCUICEnvironment.context) (σ : nat → term),
wf_local Σ Δ → well_subst Σ Γ σ Δ → Σ;;; Δ |- t.[σ] : T.[σ]) Σ)
(Γ0,,, Γ',,, Δ) →
wf_local Σ Γ0 →
subslet Σ Γ0 s Γ' →
wf_local Σ (Γ0,,, subst_context s 0 Δ).
Proof using wfΣ.
intros HΓ HΓ0 sub.
rewrite subst_context_inst_context.
eapply (wf_local_app_inst _ (Γ0 ,,, Γ')); eauto.
× now eapply All_local_env_app_inv in HΓ as [].
× eapply (subslet_well_subst (Δ:=[])) in sub;
rewrite ?subst_context_nil in sub |- ×.
+ apply sub.
+ pcuicfo.
Qed.
End SubstitutionLemmas.
Theorem substitution_prop {cf} : env_prop
(fun Σ Γ0 t T ⇒
∀ (Γ Γ' Δ : context) (s : list term)
(sub : subslet Σ Γ s Γ') (eqΓ0 : Γ0 = Γ ,,, Γ' ,,, Δ),
wf_local Σ (Γ ,,, subst_context s 0 Δ) →
Σ ;;; Γ ,,, subst_context s 0 Δ |- subst s #|Δ| t : subst s #|Δ| T)
(fun Σ Γ0 ⇒
∀ (Γ Γ' Δ : context) (s : list term)
(sub : subslet Σ Γ s Γ') (eqΓ0 : Γ0 = Γ ,,, Γ' ,,, Δ),
wf_local Σ (Γ ,,, subst_context s 0 Δ)).
Proof.
intros Σ wfΣ Γ t T HT.
pose proof (type_inst Σ wfΣ Γ t T HT) as [HΣ [HΓ HTy]].
intuition auto.
3:{
subst Γ.
rewrite !subst_inst. eapply HTy ⇒ //.
eapply subslet_well_subst; eauto. }
2:{ subst Γ.
eapply typing_wf_local in HT.
eapply wf_local_app_inv in HT as [HΓ0 _].
eapply wf_local_app_inv in HΓ0 as [HΓ0 _].
eapply All_local_env_inst; eauto. }
unshelve eapply on_wf_global_env_impl ; tea.
clear. intros × HΣ HP HQ Hty.
apply lift_typing_impl with (1 := Hty); clear -HΣ HP.
intros. subst Γ.
rewrite !subst_inst. eapply X ⇒ //.
now unshelve eapply subslet_well_subst.
Qed.
Corollary substitution {cf} {Σ} {wfΣ : wf Σ} {Γ Γ' s Δ t T} :
subslet Σ Γ s Γ' →
Σ ;;; Γ ,,, Γ' ,,, Δ |- t : T →
Σ ;;; Γ ,,, subst_context s 0 Δ |- subst s #|Δ| t : subst s #|Δ| T.
Proof.
intros Hs Ht.
eapply (env_prop_typing substitution_prop); trea.
eapply (env_prop_wf_local substitution_prop); trea.
now eapply typing_wf_local in Ht.
Qed.
Corollary isType_substitution {cf} {Σ} {wfΣ : wf Σ} {Γ Γ' s Δ T} :
subslet Σ Γ s Γ' →
isType Σ (Γ ,,, Γ' ,,, Δ) T →
isType Σ (Γ ,,, subst_context s 0 Δ) (subst s #|Δ| T).
Proof.
intros Hs [s' Ht].
eapply substitution in Ht; tea. now eexists.
Qed.
Corollary substitution_wf_local {cf} {Σ} {wfΣ : wf Σ} {Γ Γ' s Δ} :
subslet Σ Γ s Γ' →
wf_local Σ (Γ ,,, Γ' ,,, Δ) →
wf_local Σ (Γ ,,, subst_context s 0 Δ).
Proof.
intros Hs Ht.
eapply (env_prop_wf_local substitution_prop); trea.
Qed.
Lemma substitution0 {cf} {Σ} {wfΣ : wf Σ} {Γ n u U t T} :
Σ ;;; Γ ,, vass n U |- t : T → Σ ;;; Γ |- u : U →
Σ ;;; Γ |- t {0 := u} : T {0 := u}.
Proof.
intros Ht Hu.
assert (wfΓ : wf_local Σ Γ).
{ apply typing_wf_local in Hu; eauto. }
eapply (substitution (Γ' := [vass n U]) (Δ := [])); tea.
now eapply subslet_ass_tip.
Qed.
Lemma substitution_let {cf} {Σ} {wfΣ : wf Σ} {Γ n u U t T} :
Σ ;;; Γ ,, vdef n u U |- t : T →
Σ ;;; Γ |- t {0 := u} : T {0 := u}.
Proof.
intros Ht.
assert ((wf_local Σ Γ) × (Σ ;;; Γ |- u : U)%type) as [wfΓ tyu].
{ apply typing_wf_local in Ht; eauto with wf.
now depelim Ht; simpl in ×.
}
eapply (substitution (Γ':=[vdef n u U]) (Δ := [])); tea.
now eapply subslet_def_tip.
Qed.
Substitution into a *well-typed* cumulativity/conversion derivation.
Lemma substitution_wt_cumul_pb {cf} {Σ} {wfΣ : wf Σ} {le Γ Γ' Γ'' s M N} :
subslet Σ Γ s Γ' →
wt_cumul_pb le Σ (Γ ,,, Γ' ,,, Γ'') M N →
wt_cumul_pb le Σ (Γ ,,, subst_context s 0 Γ'') (subst s #|Γ''| M) (subst s #|Γ''| N).
Proof.
move⇒ Hs wteq; split.
+ eapply (isType_substitution Hs), wteq.
+ eapply (isType_substitution Hs), wteq.
+ move/wt_cumul_pb_equalityP: wteq; elim.
- intros t u cmp.
constructor. now eapply subst_compare_term.
- move⇒ t u v red cum.
destruct le.
× eapply red_conv_conv.
eapply substitution_let_red; tea; eauto with wf; apply red.
× eapply red_cumul_cumul.
eapply substitution_let_red; tea; eauto with wf; apply red.
- move⇒ t u v red cum red'.
destruct le.
× eapply red_conv_conv_inv; tea.
eapply substitution_let_red; tea; apply red'.
× eapply red_cumul_cumul_inv; tea.
eapply substitution_let_red; tea; apply red'.
Qed.
Lemma substitution_cumul {cf} {Σ} {wfΣ : wf Σ} {Γ Γ' Γ'' s M N} :
subslet Σ Γ s Γ' →
Σ ;;; Γ ,,, Γ' ,,, Γ'' |- M ≤ N ✓ →
Σ ;;; Γ ,,, subst_context s 0 Γ'' |- subst s #|Γ''| M ≤ subst s #|Γ''| N ✓.
Proof. apply substitution_wt_cumul_pb. Qed.
Lemma substitution_conv {cf} {Σ} {wfΣ : wf Σ} {Γ Γ' Γ'' s M N} :
subslet Σ Γ s Γ' →
Σ ;;; Γ ,,, Γ' ,,, Γ'' |- M = N ✓ →
Σ ;;; Γ ,,, subst_context s 0 Γ'' |- subst s #|Γ''| M = subst s #|Γ''| N ✓.
Proof. apply substitution_wt_cumul_pb. Qed.