Library MetaCoq.PCUIC.PCUICContexts
From MetaCoq.Template Require Import config utils.
From Coq Require Import CRelationClasses ProofIrrelevance.
From MetaCoq.Template Require Import config Universes utils BasicAst.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICInduction
PCUICReflect PCUICLiftSubst PCUICUnivSubst PCUICTyping
PCUICEquality PCUICCumulativity PCUICReduction
PCUICContextSubst PCUICUnivSubstitutionConv
PCUICClosed PCUICSigmaCalculus PCUICSubstitution PCUICUnivSubstitutionTyp
PCUICWeakeningTyp PCUICWeakeningConv PCUICGeneration PCUICUtils.
From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.
Require Import Equations.Type.Relation_Properties.
Require Import ssreflect ssrbool.
Implicit Types (cf : checker_flags) (Σ : global_env_ext).
#[global]
Hint Rewrite Nat.add_0_r : len.
Lemma smash_context_subst_empty s n Γ :
smash_context [] (subst_context s n Γ) =
subst_context s n (smash_context [] Γ).
Proof. apply: (smash_context_subst []). Qed.
Lemma conv_context_smash {cf:checker_flags} Σ Γ Δ Δ' :
assumption_context Δ →
All2_fold (fun Δ Δ' ⇒ conv_decls cumulSpec0 Σ (Γ ,,, Δ) (Γ ,,, Δ')) Δ Δ' →
assumption_context Δ'.
Proof.
intros Hass Hconv.
induction Hass in Δ', Hconv |- ×. depelim Hconv. constructor.
depelim Hconv. depelim c; constructor; auto.
Qed.
Lemma smash_context_assumption_context {Γ Δ} :
assumption_context Γ →
assumption_context (smash_context Γ Δ).
Proof.
induction Δ in Γ |- *; simpl; auto.
destruct a as [? [b|] ty]; auto.
intros.
eapply IHΔ. clear -H.
induction H; simpl; auto. constructor.
rewrite subst_context_snoc. constructor; auto.
intros.
eapply IHΔ.
clear -H. induction H; simpl; auto. constructor. constructor.
constructor. auto.
Qed.
#[global]
Hint Resolve smash_context_assumption_context : pcuic.
#[global]
Hint Constructors assumption_context : pcuic.
Lemma smash_assumption_context Γ :
assumption_context Γ →
smash_context [] Γ = Γ.
Proof.
induction Γ using rev_ind.
- now reflexivity.
- destruct x as [na [b|] ty].
intros ass. eapply assumption_context_app in ass as []. elimtype False; depelim a0.
intros ass.
rewrite smash_context_app_ass IHΓ. now eapply assumption_context_app in ass as [].
reflexivity.
Qed.
Lemma smash_context_idempotent Γ :
smash_context [] (smash_context [] Γ) = smash_context [] Γ.
Proof.
rewrite smash_assumption_context //; pcuic.
Qed.
Lemma assumption_context_length ctx : assumption_context ctx →
context_assumptions ctx = #|ctx|.
Proof. induction 1; simpl; auto; lia. Qed.
#[global]
Hint Resolve assumption_context_length : pcuic.
Lemma map_subst_instance_to_extended_list_k u ctx k :
map (subst_instance u) (to_extended_list_k ctx k)
= to_extended_list_k ctx k.
Proof.
pose proof (to_extended_list_k_spec ctx k).
solve_all.
now destruct H as [n [-> _]].
Qed.
Lemma subst_instance_to_extended_list_k u l k
: map (subst_instance u) (to_extended_list_k l k)
= to_extended_list_k (subst_instance u l) k.
Proof.
unfold to_extended_list_k.
change [] with (map (subst_instance u) (@nil term)) at 2.
generalize (@nil term). induction l as [|[aa [ab|] ac] bb] in k |- ×.
+ reflexivity.
+ intros l; cbn. now rewrite IHbb.
+ intros l; cbn. now rewrite IHbb.
Qed.
Lemma context_subst_lift Γ p s n :
context_subst Γ p s →
context_subst (lift_context n 0 Γ) (map (lift0 n) p) (map (lift0 n) s).
Proof.
induction 1 in |- *; try constructor.
rewrite lift_context_snoc map_app /=; constructor; auto.
rewrite lift_context_snoc /= /lift_decl /map_decl /=.
rewrite Nat.add_0_r.
rewrite (context_subst_length X).
rewrite distr_lift_subst Nat.add_0_r.
now constructor.
Qed.
Derive Signature for subslet.
Lemma closedn_ctx_snoc k Γ d : closedn_ctx k (Γ ,, d) = closedn_ctx k Γ && closed_decl (#|Γ| + k) d.
Proof. reflexivity. Qed.
Lemma type_local_ctx_wf_local {cf:checker_flags} Σ Γ Δ s :
wf_local Σ Γ →
type_local_ctx (lift_typing typing) Σ Γ Δ s →
wf_local Σ (Γ ,,, Δ).
Proof.
induction Δ; simpl; auto.
destruct a as [na [b|] ty];
intros wfΓ wfctx; constructor; intuition auto. ∃ s; auto.
Qed.
Lemma sorts_local_ctx_wf_local {cf:checker_flags} Σ Γ Δ s :
wf_local Σ Γ →
sorts_local_ctx (lift_typing typing) Σ Γ Δ s →
wf_local Σ (Γ ,,, Δ).
Proof.
induction Δ in s |- *; simpl; auto.
destruct a as [na [b|] ty];
intros wfΓ wfctx; constructor; intuition auto. pcuic.
destruct s ⇒ //. destruct wfctx; eauto.
destruct s ⇒ //. destruct wfctx. ∃ t; auto.
Qed.
Lemma instantiate_minductive {cf:checker_flags} Σ ind mdecl u Γ t T :
wf Σ.1 →
declared_minductive Σ.1 ind mdecl →
consistent_instance_ext Σ (ind_universes mdecl) u →
(Σ.1, ind_universes mdecl) ;;; Γ |- t : T →
Σ ;;; subst_instance u Γ |- subst_instance u t : subst_instance u T.
Proof.
intros wfΣ isdecl Hu Ht.
red in isdecl. eapply typing_subst_instance_decl in isdecl; eauto.
Qed.
Lemma type_local_ctx_instantiate {cf:checker_flags} Σ ind mdecl Γ Δ u s :
wf Σ.1 →
declared_minductive Σ.1 ind mdecl →
type_local_ctx (lift_typing typing) (Σ.1, ind_universes mdecl) Γ Δ s →
consistent_instance_ext Σ (ind_universes mdecl) u →
type_local_ctx (lift_typing typing) Σ (subst_instance u Γ) (subst_instance u Δ) (subst_instance_univ u s).
Proof.
intros Hctx Hu.
induction Δ; simpl in *; intuition auto.
{ destruct Σ as [Σ univs]. eapply (wf_universe_subst_instance (Σ, ind_universes mdecl)); eauto. }
destruct a as [na [b|] ty]; simpl; [destruct X as (Hwfctx & Ht & Hb) | destruct X as (Hwfctx & Ht)]; repeat split.
- now apply IHΔ.
- eapply infer_typing_sort_impl with _ Ht; intros Hs.
eapply instantiate_minductive in Hs; eauto.
now rewrite subst_instance_app in Hs.
- eapply instantiate_minductive in Hb; eauto.
now rewrite subst_instance_app in Hb.
- now apply IHΔ.
- eapply instantiate_minductive in Ht; eauto.
now rewrite subst_instance_app in Ht.
Qed.
Lemma sorts_local_ctx_instantiate {cf:checker_flags} Σ ind mdecl Γ Δ u s :
wf Σ.1 →
declared_minductive Σ.1 ind mdecl →
sorts_local_ctx (lift_typing typing) (Σ.1, ind_universes mdecl) Γ Δ s →
consistent_instance_ext Σ (ind_universes mdecl) u →
sorts_local_ctx (lift_typing typing) Σ (subst_instance u Γ) (subst_instance u Δ)
(List.map (subst_instance_univ u) s).
Proof.
intros Hctx Hu.
induction Δ in s |- *; simpl in *; intuition auto.
destruct s; simpl; intuition eauto.
destruct a as [na [b|] ty]; simpl. intuition eauto.
- eapply infer_typing_sort_impl with _ a0; intros Hs.
eapply instantiate_minductive in Hs; eauto.
now rewrite subst_instance_app in Hs.
- eapply instantiate_minductive in b1; eauto.
now rewrite subst_instance_app in b1.
- destruct s; simpl; intuition eauto.
eapply instantiate_minductive in b; eauto.
now rewrite subst_instance_app in b.
Qed.
Lemma subst_type_local_ctx {cf:checker_flags} Σ Γ Δ Δ' s ctxs :
wf Σ.1 →
wf_local Σ (Γ ,,, Δ) →
type_local_ctx (lift_typing typing) Σ (Γ ,,, Δ) Δ' ctxs →
subslet Σ Γ s Δ →
type_local_ctx (lift_typing typing) Σ Γ (subst_context s 0 Δ') ctxs.
Proof.
induction Δ'; simpl; auto.
destruct a as [na [b|] ty]; simpl; intuition auto.
+ simpl; rewrite subst_context_snoc /= /subst_decl /map_decl /= Nat.add_0_r;
repeat split; tas.
- apply infer_typing_sort_impl with id a0; intros Hs.
now eapply substitution in Hs.
- now eapply substitution in b1.
+ rewrite subst_context_snoc /= /subst_decl /map_decl /= Nat.add_0_r.
intuition auto.
eapply substitution in b; eauto.
Qed.
Lemma subst_sorts_local_ctx {cf:checker_flags} Σ Γ Δ Δ' s ctxs :
wf Σ.1 →
wf_local Σ (Γ ,,, Δ) →
sorts_local_ctx (lift_typing typing) Σ (Γ ,,, Δ) Δ' ctxs →
subslet Σ Γ s Δ →
sorts_local_ctx (lift_typing typing) Σ Γ (subst_context s 0 Δ') ctxs.
Proof.
induction Δ' in ctxs |- *; simpl; auto.
destruct a as [na [b|] ty]; simpl; intuition auto.
+ simpl; rewrite subst_context_snoc /= /subst_decl /map_decl /= Nat.add_0_r.
repeat split.
- now apply IHΔ'.
- apply infer_typing_sort_impl with id a0; intros Hs.
now eapply substitution in Hs.
- now eapply substitution in b1.
+ rewrite subst_context_snoc /= /subst_decl /map_decl /= Nat.add_0_r.
destruct ctxs; auto.
intuition auto.
eapply substitution in b; eauto.
Qed.
Lemma weaken_type_local_ctx {cf:checker_flags} Σ Γ Γ' Δ ctxs :
wf Σ.1 →
wf_local Σ Γ →
type_local_ctx (lift_typing typing) Σ Γ' Δ ctxs →
type_local_ctx (lift_typing typing) Σ (Γ ,,, Γ') Δ ctxs.
Proof.
induction Δ; simpl; auto.
destruct a as [na [b|] ty]; simpl; intuition auto.
1: apply infer_typing_sort_impl with id a0; intros Hs.
all: rewrite -app_context_assoc.
all: eapply (weaken_ctx Γ); auto.
Qed.
Lemma weaken_sorts_local_ctx {cf:checker_flags} Σ Γ Γ' Δ ctxs :
wf Σ.1 →
wf_local Σ Γ →
sorts_local_ctx (lift_typing typing) Σ Γ' Δ ctxs →
sorts_local_ctx (lift_typing typing) Σ (Γ ,,, Γ') Δ ctxs.
Proof.
induction Δ in ctxs |- *; simpl; auto.
destruct a as [na [b|] ty]; simpl; intuition auto.
1: apply infer_typing_sort_impl with id a0; intros Hs.
all: rewrite -app_context_assoc.
3: destruct ctxs; auto.
3: destruct X1; split; auto.
all: now eapply (weaken_ctx Γ).
Qed.
Lemma reln_app acc Γ Δ k : reln acc k (Γ ++ Δ) =
reln (reln acc k Γ) (#|Γ| + k) Δ.
Proof.
induction Γ in acc, Δ, k |- *; simpl; auto.
destruct a as [na [b|] ty]. rewrite IHΓ. f_equal. lia.
simpl. rewrite IHΓ. f_equal. lia.
Qed.
Lemma reln_acc acc k Γ : reln acc k Γ = reln [] k Γ ++ acc.
Proof.
induction Γ in acc, k |- *; simpl; auto.
destruct a as [na [b|] ty]. rewrite IHΓ. f_equal.
rewrite IHΓ. rewrite [reln [_] _ _]IHΓ.
now rewrite -app_assoc.
Qed.
Lemma to_extended_list_k_app Γ Δ k : to_extended_list_k (Γ ++ Δ) k =
to_extended_list_k Δ (#|Γ| + k) ++ to_extended_list_k Γ k.
Proof.
unfold to_extended_list_k. now rewrite reln_app reln_acc.
Qed.
Lemma to_extended_list_k_fold_context_k f Γ k :
to_extended_list_k (fold_context_k f Γ) k = to_extended_list_k Γ k.
Proof.
rewrite /to_extended_list_k.
generalize (@nil term).
induction Γ in k |- ×.
simpl; auto.
intros.
rewrite fold_context_k_snoc0. simpl.
destruct a as [? [?|] ?] ⇒ /=; now rewrite IHΓ.
Qed.
Lemma to_extended_list_k_lift_context c k n k' :
to_extended_list_k (lift_context n k c) k' = to_extended_list_k c k'.
Proof. now rewrite to_extended_list_k_fold_context_k. Qed.
Lemma reln_lift n k Γ : reln [] (n + k) Γ = map (lift0 n) (reln [] k Γ).
Proof.
induction Γ in n, k |- *; simpl; auto.
destruct a as [? [?|] ?]; simpl.
now rewrite -IHΓ Nat.add_assoc.
rewrite reln_acc [reln [tRel k] _ _]reln_acc map_app /=.
f_equal. now rewrite -IHΓ Nat.add_assoc.
Qed.
Lemma to_extended_list_length Γ : #|to_extended_list Γ| = context_assumptions Γ.
Proof. now rewrite /to_extended_list to_extended_list_k_length. Qed.
#[global]
Hint Rewrite to_extended_list_length : len.
Lemma map_subst_app_to_extended_list_k s s' ctx k :
k = #|s| →
map (subst0 (s ++ s')) (to_extended_list_k ctx k) =
map (subst0 s') (to_extended_list_k ctx 0).
Proof.
intros →.
rewrite /to_extended_list_k.
rewrite -{1}(Nat.add_0_r #|s|) reln_lift map_map_compose.
apply map_ext. intros x; simpl.
rewrite subst_app_decomp.
f_equal. rewrite -{1}(Nat.add_0_r #|s|) simpl_subst' ?lift0_id //.
now rewrite map_length.
Qed.
Lemma subst_context_smash_context s k Γ Δ :
subst_context s k (smash_context Γ Δ) =
smash_context (subst_context s (#|Δ| + k) Γ) (subst_context s k Δ).
Proof.
induction Δ as [|[? [] ?] ?] in Γ |- *; simpl; auto;
rewrite subst_context_snoc; simpl.
- rewrite IHΔ. f_equal.
rewrite !subst_context_alt !mapi_mapi. apply mapi_ext. clear.
intros n x. rewrite /subst_decl !compose_map_decl.
eapply map_decl_ext. intros.
autorewrite with len.
generalize (Nat.pred #|Γ| - n). generalize (#|Δ| + k). clear.
intros. rewrite distr_subst_rec. simpl. now rewrite -Nat.add_assoc.
- rewrite IHΔ. f_equal.
rewrite subst_context_app. simpl. unfold app_context. f_equal.
Qed.
Section WfEnv.
Context {cf} {Σ} {wfΣ : wf Σ}.
Lemma wf_local_rel_smash_context_gen {Γ Δ Δ'} :
wf_local Σ (Δ' ,,, Γ) →
wf_local_rel Σ (Δ' ,,, Γ) Δ →
wf_local_rel Σ Δ' (smash_context Δ Γ).
Proof using wfΣ.
induction Γ in Δ |- *; simpl; auto.
intros wfΓ wfΔ. depelim wfΓ; simpl.
- apply IHΓ; auto. eapply All_local_env_app. split; auto.
repeat constructor; auto.
eapply All_local_env_impl; eauto. simpl; intros.
now rewrite app_context_assoc.
- apply IHΓ. auto. eapply All_local_env_subst; eauto. simpl; intros.
destruct T; simpl in *; pcuicfo auto.
2: apply infer_typing_sort_impl with id X; intros Hs.
1: rename X into Hs.
all: rewrite Nat.add_0_r.
all: eapply (substitution (Γ':=[vdef na b t]) (s := [b])) in Hs; eauto.
all: rewrite -{1}(subst_empty 0 b).
all: repeat constructor.
all: now rewrite !subst_empty.
Qed.
Lemma wf_local_rel_smash_context {Γ Δ} :
wf_local Σ (Δ ,,, Γ) →
wf_local_rel Σ Δ (smash_context [] Γ).
Proof using wfΣ.
intros. eapply wf_local_rel_smash_context_gen; eauto. constructor.
Qed.
Lemma wf_local_smash_end Γ Δ :
wf_local Σ (Γ ,,, Δ) → wf_local Σ (Γ ,,, smash_context [] Δ).
Proof using wfΣ.
intros wf.
apply All_local_env_app. split.
now apply All_local_env_app_inv in wf.
eapply wf_local_rel_smash_context; auto.
Qed.
Lemma wf_local_rel_empty Γ : wf_local_rel Σ [] Γ <~> wf_local Σ Γ.
Proof using Type.
split.
- intros h. eapply (All_local_env_impl _ _ _ h). pcuicfo.
red in X |- ×. now rewrite app_context_nil_l in X.
- intros h. eapply (All_local_env_impl _ _ _ h). pcuicfo.
red in X |- ×. now rewrite app_context_nil_l.
Qed.
Lemma wf_local_smash_context {Γ} :
wf_local Σ Γ → wf_local Σ (smash_context [] Γ).
Proof using wfΣ.
intros; apply wf_local_rel_empty. eapply wf_local_rel_smash_context.
rewrite ?app_context_nil_l; eauto.
Qed.
End WfEnv.
Local Open Scope sigma_scope.
Lemma context_subst_extended_subst Γ args s :
context_subst Γ args s →
s = map (inst (List.rev args ⋅n ids)) (extended_subst Γ 0).
Proof.
induction 1.
- simpl; auto.
- simpl.
rewrite lift_extended_subst.
rewrite map_map_compose.
rewrite List.rev_app_distr. simpl. f_equal.
rewrite IHX. apply map_ext.
intros. autorewrite with sigma.
apply inst_ext.
rewrite subst_consn_subst_cons.
now rewrite subst_cons_shift.
- simpl.
f_equal; auto. len.
rewrite IHX.
autorewrite with sigma.
apply inst_ext. len.
rewrite (Upn_eq _ (List.rev args ⋅n ids)).
rewrite subst_consn_compose.
rewrite PCUICInstConv.map_inst_idsn; len; try lia.
rewrite subst_compose_assoc.
rewrite -(context_subst_length2 X).
rewrite subst_consn_shiftn; len ⇒ //.
sigma. rewrite Upn_eq. sigma.
rewrite PCUICInstConv.map_inst_idsn; len; try lia.
rewrite -subst_compose_assoc shiftk_compose.
rewrite -subst_consn_app.
rewrite subst_consn_shiftn //. now len.
Qed.
Lemma map_subst_app_decomp (l l' : list term) (k : nat) (ts : list term) :
map (subst (l ++ l') k) ts = map (fun x ⇒ subst l' k (subst (map (lift0 #|l'|) l) k x)) ts.
Proof.
apply map_ext. apply subst_app_decomp.
Qed.
Lemma map_reln_ext (f g : term → term) k Γ :
(∀ n, n < #|Γ| → f (tRel (k + n)) = g (tRel (k + n))) →
map f (reln [] k Γ) = map g (reln [] k Γ).
Proof.
intros Hf.
induction Γ as [|[? [] ?] ?] in k, Hf |- *; simpl; auto.
- rewrite reln_acc map_app. simpl.
rewrite map_app /=. rewrite IHΓ //.
intros. simpl in Hf. specialize (Hf (S n)).
forward Hf. lia. rewrite -Nat.add_assoc. apply Hf.
- rewrite reln_acc map_app. simpl.
rewrite map_app /= IHΓ //.
intros. simpl in Hf. specialize (Hf (S n)).
forward Hf. lia. rewrite -Nat.add_assoc. apply Hf.
f_equal. f_equal. specialize (Hf 0). simpl in Hf.
forward Hf by lia. now rewrite Nat.add_0_r in Hf.
Qed.
Lemma extended_subst_to_extended_list_k Γ k :
(map (subst (extended_subst Γ 0) k) (to_extended_list_k Γ k)) =
to_extended_list_k (smash_context [] Γ) k.
Proof.
unfold to_extended_list_k.
induction Γ in k |- ×. simpl. reflexivity.
destruct a as [? [] ?]; simpl.
- rewrite smash_context_acc //.
rewrite reln_app. autorewrite with len. simpl.
rewrite -IHΓ //. rewrite Nat.add_1_r.
rewrite (reln_lift 1).
clear.
rewrite (map_subst_app_decomp [_]).
rewrite -map_map_compose. f_equal.
simpl.
generalize (lift0 #|extended_subst Γ 0|
(subst0 (extended_subst Γ 0) (lift (context_assumptions Γ) #|Γ| t))).
intros t0.
change 1 with #|[t0]|.
generalize [t0]. clear.
intros l. generalize (Nat.le_refl k).
generalize k at 1 3.
induction Γ as [|[? [] ?] ?] in k, l |- *; simpl. reflexivity.
simpl. intros k0 le0. apply IHΓ. lia.
intros k0 lek0. rewrite reln_acc map_app. simpl.
rewrite map_app. simpl.
elim: leb_spec_Set ⇒ Hle. f_equal. apply IHΓ. lia.
f_equal. elim: nth_error_spec ⇒ [x Hx Hl|Hl]. lia.
f_equal. lia. lia.
- rewrite smash_context_acc //.
simpl.
rewrite reln_acc map_app.
rewrite (reln_acc [_] _ (smash_context [] Γ)).
simpl. rewrite Nat.leb_refl Nat.sub_diag /=. f_equal.
rewrite -IHΓ //.
2:{ do 2 f_equal; lia. }
apply map_reln_ext ⇒ n Hn.
rewrite lift_extended_subst //.
replace (k + 1 + n) with (S (k + n)) by lia.
simpl.
elim: leb_spec_Set ⇒ Hle; [|lia].
elim: leb_spec_Set ⇒ Hle'; [|lia].
replace (S (k + n) - k) with (S n) by lia.
replace (S (k + n) - (k + 1)) with n by lia.
simpl.
rewrite nth_error_map.
elim: nth_error_spec ⇒ [x Hx Hlen|Hlen].
simpl. rewrite simpl_lift; try lia. f_equal. simpl.
autorewrite with len in Hlen. lia.
Qed.
Lemma assumption_context_fold f Γ :
assumption_context Γ → assumption_context (fold_context_k f Γ).
Proof.
induction 1; simpl. constructor. rewrite fold_context_k_snoc0.
now constructor.
Qed.
Lemma smash_context_app_expand Γ Δ Δ' :
smash_context Γ (Δ ,,, Δ') =
smash_context [] Δ ,,, expand_lets_ctx Δ (smash_context Γ Δ').
Proof.
rewrite smash_context_app smash_context_acc.
rewrite /expand_lets_k_ctx /app_context. f_equal.
Qed.
Lemma expand_lets_smash_context Γ Δ Δ' :
expand_lets_ctx Γ (smash_context Δ Δ') =
smash_context (expand_lets_k_ctx Γ #|Δ'| Δ) (expand_lets_ctx Γ Δ').
Proof.
rewrite /expand_lets_ctx /expand_lets_k_ctx.
rewrite -smash_context_lift -smash_context_subst /=; len.
Qed.
Lemma expand_lets_k_ctx_nil Γ k : expand_lets_k_ctx Γ k [] = [].
Proof. reflexivity. Qed.
Lemma expand_lets_ctx_nil Γ : expand_lets_ctx Γ [] = [].
Proof. reflexivity. Qed.
#[global]
Hint Rewrite expand_lets_k_ctx_nil expand_lets_ctx_nil : pcuic.
Definition subst_let_expand args Δ T :=
(subst0 args (expand_lets Δ T)).
Definition subst_context_let_expand args Δ Γ :=
(subst_context args 0 (expand_lets_ctx Δ Γ)).
Definition subst_let_expand_tProd args Δ na T s :
subst_let_expand args Δ (tProd na T (tSort s)) =
tProd na (subst_let_expand args Δ T) (tSort s).
Proof.
reflexivity.
Qed.
Definition subst_let_expand_mkApps s Δ f args :
subst_let_expand s Δ (mkApps f args) =
mkApps (subst_let_expand s Δ f) (map (subst_let_expand s Δ) args).
Proof.
rewrite /subst_let_expand.
now rewrite expand_lets_mkApps subst_mkApps map_map_compose.
Qed.
Definition subst_let_expand_tInd s Δ ind u :
subst_let_expand s Δ (tInd ind u) = tInd ind u.
Proof. reflexivity. Qed.
Lemma subst_let_expand_it_mkProd_or_LetIn s Γ Δ u :
subst_let_expand s Γ (it_mkProd_or_LetIn Δ (tSort u)) =
it_mkProd_or_LetIn (subst_context_let_expand s Γ Δ) (tSort u).
Proof.
rewrite /subst_let_expand /expand_lets.
rewrite expand_lets_it_mkProd_or_LetIn /= subst_it_mkProd_or_LetIn /=.
reflexivity.
Qed.
Lemma subst_lift_above s n k x : k = #|s| → subst0 s (lift0 (n + k) x) = lift0 n x.
Proof.
intros. rewrite Nat.add_comm. subst k. now rewrite simpl_subst.
Qed.
Lemma subst_let_expand_lift_id s Δ k x :
k = #|Δ| →
#|s| = context_assumptions Δ →
subst_let_expand s Δ (lift0 k x) = x.
Proof.
intros → hl.
rewrite /subst_let_expand /expand_lets /expand_lets_k.
simpl.
rewrite simpl_lift; len; try lia.
rewrite subst_lift_above. now len.
change (context_assumptions Δ) with (0 + context_assumptions Δ).
rewrite subst_lift_above. len. now rewrite lift0_id.
Qed.
Lemma subslet_lift {cf} {Σ} {wfΣ : wf Σ} (Γ Δ : context) s Δ' :
wf_local Σ (Γ ,,, Δ) →
subslet Σ Γ s Δ' →
subslet Σ (Γ ,,, Δ) (map (lift0 #|Δ|) s) (lift_context #|Δ| 0 Δ').
Proof.
move⇒ wfl.
induction 1; rewrite ?lift_context_snoc /=; try constructor; auto.
simpl.
rewrite -(subslet_length X).
rewrite -distr_lift_subst. apply weakening; eauto.
rewrite -(subslet_length X).
rewrite distr_lift_subst. constructor; auto.
rewrite - !distr_lift_subst. apply weakening; eauto.
Qed.
Lemma untyped_subslet_lift (Γ Δ : context) s Δ' :
untyped_subslet Γ s Δ' →
untyped_subslet (Γ ,,, Δ) (map (lift0 #|Δ|) s) (lift_context #|Δ| 0 Δ').
Proof.
induction 1; rewrite ?lift_context_snoc /=; try constructor; auto.
simpl.
rewrite -(untyped_subslet_length X).
rewrite distr_lift_subst. constructor; auto.
Qed.
Lemma untyped_subslet_extended_subst Γ Δ :
untyped_subslet (Γ ,,, smash_context [] Δ)
(extended_subst Δ 0)
(lift_context (context_assumptions Δ) 0 Δ).
Proof.
induction Δ as [|[na [d|] ?] ?]; simpl; try constructor.
× rewrite lift_context_snoc /lift_decl /= /map_decl /=.
len.
constructor ⇒ //.
× rewrite smash_context_acc. simpl.
rewrite /map_decl /= /map_decl /=. simpl.
rewrite lift_context_snoc /lift_decl /= /map_decl /=.
constructor.
rewrite (lift_extended_subst _ 1).
rewrite -(lift_context_lift_context 1 _).
eapply (untyped_subslet_lift _ [_]); eauto.
Qed.
Lemma subslet_extended_subst {cf} {Σ} {wfΣ : wf Σ} Γ Δ :
wf_local Σ (Γ ,,, Δ) →
subslet Σ (Γ ,,, smash_context [] Δ)
(extended_subst Δ 0)
(lift_context (context_assumptions Δ) 0 Δ).
Proof.
move⇒ wfΔ.
eapply wf_local_app_inv in wfΔ as [wfΓ wfΔ].
induction Δ as [|[na [d|] ?] ?] in wfΔ |- *; simpl; try constructor.
× depelim wfΔ. repeat red in l, l0.
specialize (IHΔ wfΔ).
rewrite lift_context_snoc /lift_decl /= /map_decl /=.
len.
constructor ⇒ //.
eapply (weakening_typing (Γ'' := smash_context [] Δ)) in l0.
len in l0. simpl in l0. simpl.
2:{ eapply wf_local_smash_end; pcuic. }
eapply (substitution (Δ := [])) in l0; tea.
× rewrite smash_context_acc. simpl.
rewrite /map_decl /= /map_decl /=. simpl.
depelim wfΔ.
specialize (IHΔ wfΔ).
rewrite lift_context_snoc /lift_decl /= /map_decl /=.
constructor.
- rewrite (lift_extended_subst _ 1).
rewrite -(lift_context_lift_context 1 _).
eapply (subslet_lift _ [_]); eauto.
constructor.
{ pose proof l.π2. eapply wf_local_smash_end; pcuic. }
apply infer_typing_sort_impl with id l; intros Hs.
eapply (weakening_typing (Γ'' := smash_context [] Δ)) in Hs.
len in Hs. simpl in Hs. simpl.
2:{ eapply wf_local_smash_end; pcuic. }
eapply (substitution (Δ := [])) in Hs; tea.
- eapply meta_conv.
econstructor. constructor. apply wf_local_smash_end; auto.
eapply wf_local_app; eauto.
apply infer_typing_sort_impl with id l; intros Hs.
eapply (weakening_typing (Γ'' := smash_context [] Δ)) in Hs.
len in Hs. simpl in Hs. simpl.
2:{ eapply wf_local_smash_end; pcuic. }
eapply (substitution (Δ := [])) in Hs; tea.
reflexivity.
simpl. rewrite (lift_extended_subst _ 1).
rewrite distr_lift_subst. f_equal. len.
now rewrite simpl_lift; try lia.
Qed.
Lemma typing_expand_lets {cf} {Σ} {wfΣ : wf Σ} Γ Δ t T :
Σ ;;; Γ ,,, Δ |- t : T →
Σ ;;; Γ ,,, smash_context [] Δ |- expand_lets Δ t : expand_lets Δ T.
Proof.
intros Ht.
rewrite /expand_lets /expand_lets_k.
pose proof (typing_wf_local Ht).
eapply (weakening_typing (Γ'' := smash_context [] Δ)) in Ht.
len in Ht. simpl in Ht. simpl.
2:{ eapply wf_local_smash_end; pcuic. }
eapply (substitution (Δ := [])) in Ht; tea.
now eapply subslet_extended_subst.
Qed.
Lemma subst_context_let_expand_length s Γ Δ :
#|subst_context_let_expand s Γ Δ| = #|Δ|.
Proof.
now rewrite /subst_context_let_expand; len.
Qed.
#[global]
Hint Rewrite subst_context_let_expand_length : len.
Lemma to_extended_list_subst_context_let_expand s Γ Δ :
to_extended_list (subst_context_let_expand s Γ Δ) =
to_extended_list Δ.
Proof.
rewrite /subst_context_let_expand /to_extended_list /expand_lets_ctx /expand_lets_k_ctx.
now rewrite !to_extended_list_k_subst to_extended_list_k_lift_context.
Qed.
Lemma map2_set_binder_name_alpha (nas : list aname) (Δ Δ' : context) :
All2 (fun x y ⇒ eq_binder_annot x (decl_name y)) nas Δ →
eq_context_upto_names Δ Δ' →
eq_context_upto_names (map2 set_binder_name nas Δ) Δ'.
Proof.
intros hl. induction 1 in nas, hl |- *; cbn; auto.
destruct nas; cbn; auto.
destruct nas; cbn; auto; depelim hl.
constructor; auto. destruct r; subst; cbn; constructor; auto;
now transitivity na.
Qed.
Notation eq_names := (All2 (fun x y ⇒ x = (decl_name y))).
Lemma eq_names_subst_context nas Γ s k :
eq_names nas Γ →
eq_names nas (subst_context s k Γ).
Proof.
induction 1.
× cbn; auto. constructor.
× rewrite subst_context_snoc. constructor; auto.
Qed.
Lemma eq_names_subst_instance nas Γ u :
eq_names nas Γ →
eq_names nas (subst_instance u Γ).
Proof.
induction 1.
× cbn; auto.
× rewrite /subst_instance /=. constructor; auto.
Qed.
Lemma map2_set_binder_name_alpha_eq (nas : list aname) (Δ Δ' : context) :
eq_names nas Δ' →
eq_context_upto_names Δ Δ' →
(map2 set_binder_name nas Δ) = Δ'.
Proof.
intros hl. induction 1 in nas, hl |- *; cbn; auto.
destruct nas; cbn; auto.
destruct nas; cbn; auto; depelim hl.
f_equal; auto. destruct r; subst; cbn; auto.
Qed.
From Coq Require Import CRelationClasses ProofIrrelevance.
From MetaCoq.Template Require Import config Universes utils BasicAst.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICInduction
PCUICReflect PCUICLiftSubst PCUICUnivSubst PCUICTyping
PCUICEquality PCUICCumulativity PCUICReduction
PCUICContextSubst PCUICUnivSubstitutionConv
PCUICClosed PCUICSigmaCalculus PCUICSubstitution PCUICUnivSubstitutionTyp
PCUICWeakeningTyp PCUICWeakeningConv PCUICGeneration PCUICUtils.
From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.
Require Import Equations.Type.Relation_Properties.
Require Import ssreflect ssrbool.
Implicit Types (cf : checker_flags) (Σ : global_env_ext).
#[global]
Hint Rewrite Nat.add_0_r : len.
Lemma smash_context_subst_empty s n Γ :
smash_context [] (subst_context s n Γ) =
subst_context s n (smash_context [] Γ).
Proof. apply: (smash_context_subst []). Qed.
Lemma conv_context_smash {cf:checker_flags} Σ Γ Δ Δ' :
assumption_context Δ →
All2_fold (fun Δ Δ' ⇒ conv_decls cumulSpec0 Σ (Γ ,,, Δ) (Γ ,,, Δ')) Δ Δ' →
assumption_context Δ'.
Proof.
intros Hass Hconv.
induction Hass in Δ', Hconv |- ×. depelim Hconv. constructor.
depelim Hconv. depelim c; constructor; auto.
Qed.
Lemma smash_context_assumption_context {Γ Δ} :
assumption_context Γ →
assumption_context (smash_context Γ Δ).
Proof.
induction Δ in Γ |- *; simpl; auto.
destruct a as [? [b|] ty]; auto.
intros.
eapply IHΔ. clear -H.
induction H; simpl; auto. constructor.
rewrite subst_context_snoc. constructor; auto.
intros.
eapply IHΔ.
clear -H. induction H; simpl; auto. constructor. constructor.
constructor. auto.
Qed.
#[global]
Hint Resolve smash_context_assumption_context : pcuic.
#[global]
Hint Constructors assumption_context : pcuic.
Lemma smash_assumption_context Γ :
assumption_context Γ →
smash_context [] Γ = Γ.
Proof.
induction Γ using rev_ind.
- now reflexivity.
- destruct x as [na [b|] ty].
intros ass. eapply assumption_context_app in ass as []. elimtype False; depelim a0.
intros ass.
rewrite smash_context_app_ass IHΓ. now eapply assumption_context_app in ass as [].
reflexivity.
Qed.
Lemma smash_context_idempotent Γ :
smash_context [] (smash_context [] Γ) = smash_context [] Γ.
Proof.
rewrite smash_assumption_context //; pcuic.
Qed.
Lemma assumption_context_length ctx : assumption_context ctx →
context_assumptions ctx = #|ctx|.
Proof. induction 1; simpl; auto; lia. Qed.
#[global]
Hint Resolve assumption_context_length : pcuic.
Lemma map_subst_instance_to_extended_list_k u ctx k :
map (subst_instance u) (to_extended_list_k ctx k)
= to_extended_list_k ctx k.
Proof.
pose proof (to_extended_list_k_spec ctx k).
solve_all.
now destruct H as [n [-> _]].
Qed.
Lemma subst_instance_to_extended_list_k u l k
: map (subst_instance u) (to_extended_list_k l k)
= to_extended_list_k (subst_instance u l) k.
Proof.
unfold to_extended_list_k.
change [] with (map (subst_instance u) (@nil term)) at 2.
generalize (@nil term). induction l as [|[aa [ab|] ac] bb] in k |- ×.
+ reflexivity.
+ intros l; cbn. now rewrite IHbb.
+ intros l; cbn. now rewrite IHbb.
Qed.
Lemma context_subst_lift Γ p s n :
context_subst Γ p s →
context_subst (lift_context n 0 Γ) (map (lift0 n) p) (map (lift0 n) s).
Proof.
induction 1 in |- *; try constructor.
rewrite lift_context_snoc map_app /=; constructor; auto.
rewrite lift_context_snoc /= /lift_decl /map_decl /=.
rewrite Nat.add_0_r.
rewrite (context_subst_length X).
rewrite distr_lift_subst Nat.add_0_r.
now constructor.
Qed.
Derive Signature for subslet.
Lemma closedn_ctx_snoc k Γ d : closedn_ctx k (Γ ,, d) = closedn_ctx k Γ && closed_decl (#|Γ| + k) d.
Proof. reflexivity. Qed.
Lemma type_local_ctx_wf_local {cf:checker_flags} Σ Γ Δ s :
wf_local Σ Γ →
type_local_ctx (lift_typing typing) Σ Γ Δ s →
wf_local Σ (Γ ,,, Δ).
Proof.
induction Δ; simpl; auto.
destruct a as [na [b|] ty];
intros wfΓ wfctx; constructor; intuition auto. ∃ s; auto.
Qed.
Lemma sorts_local_ctx_wf_local {cf:checker_flags} Σ Γ Δ s :
wf_local Σ Γ →
sorts_local_ctx (lift_typing typing) Σ Γ Δ s →
wf_local Σ (Γ ,,, Δ).
Proof.
induction Δ in s |- *; simpl; auto.
destruct a as [na [b|] ty];
intros wfΓ wfctx; constructor; intuition auto. pcuic.
destruct s ⇒ //. destruct wfctx; eauto.
destruct s ⇒ //. destruct wfctx. ∃ t; auto.
Qed.
Lemma instantiate_minductive {cf:checker_flags} Σ ind mdecl u Γ t T :
wf Σ.1 →
declared_minductive Σ.1 ind mdecl →
consistent_instance_ext Σ (ind_universes mdecl) u →
(Σ.1, ind_universes mdecl) ;;; Γ |- t : T →
Σ ;;; subst_instance u Γ |- subst_instance u t : subst_instance u T.
Proof.
intros wfΣ isdecl Hu Ht.
red in isdecl. eapply typing_subst_instance_decl in isdecl; eauto.
Qed.
Lemma type_local_ctx_instantiate {cf:checker_flags} Σ ind mdecl Γ Δ u s :
wf Σ.1 →
declared_minductive Σ.1 ind mdecl →
type_local_ctx (lift_typing typing) (Σ.1, ind_universes mdecl) Γ Δ s →
consistent_instance_ext Σ (ind_universes mdecl) u →
type_local_ctx (lift_typing typing) Σ (subst_instance u Γ) (subst_instance u Δ) (subst_instance_univ u s).
Proof.
intros Hctx Hu.
induction Δ; simpl in *; intuition auto.
{ destruct Σ as [Σ univs]. eapply (wf_universe_subst_instance (Σ, ind_universes mdecl)); eauto. }
destruct a as [na [b|] ty]; simpl; [destruct X as (Hwfctx & Ht & Hb) | destruct X as (Hwfctx & Ht)]; repeat split.
- now apply IHΔ.
- eapply infer_typing_sort_impl with _ Ht; intros Hs.
eapply instantiate_minductive in Hs; eauto.
now rewrite subst_instance_app in Hs.
- eapply instantiate_minductive in Hb; eauto.
now rewrite subst_instance_app in Hb.
- now apply IHΔ.
- eapply instantiate_minductive in Ht; eauto.
now rewrite subst_instance_app in Ht.
Qed.
Lemma sorts_local_ctx_instantiate {cf:checker_flags} Σ ind mdecl Γ Δ u s :
wf Σ.1 →
declared_minductive Σ.1 ind mdecl →
sorts_local_ctx (lift_typing typing) (Σ.1, ind_universes mdecl) Γ Δ s →
consistent_instance_ext Σ (ind_universes mdecl) u →
sorts_local_ctx (lift_typing typing) Σ (subst_instance u Γ) (subst_instance u Δ)
(List.map (subst_instance_univ u) s).
Proof.
intros Hctx Hu.
induction Δ in s |- *; simpl in *; intuition auto.
destruct s; simpl; intuition eauto.
destruct a as [na [b|] ty]; simpl. intuition eauto.
- eapply infer_typing_sort_impl with _ a0; intros Hs.
eapply instantiate_minductive in Hs; eauto.
now rewrite subst_instance_app in Hs.
- eapply instantiate_minductive in b1; eauto.
now rewrite subst_instance_app in b1.
- destruct s; simpl; intuition eauto.
eapply instantiate_minductive in b; eauto.
now rewrite subst_instance_app in b.
Qed.
Lemma subst_type_local_ctx {cf:checker_flags} Σ Γ Δ Δ' s ctxs :
wf Σ.1 →
wf_local Σ (Γ ,,, Δ) →
type_local_ctx (lift_typing typing) Σ (Γ ,,, Δ) Δ' ctxs →
subslet Σ Γ s Δ →
type_local_ctx (lift_typing typing) Σ Γ (subst_context s 0 Δ') ctxs.
Proof.
induction Δ'; simpl; auto.
destruct a as [na [b|] ty]; simpl; intuition auto.
+ simpl; rewrite subst_context_snoc /= /subst_decl /map_decl /= Nat.add_0_r;
repeat split; tas.
- apply infer_typing_sort_impl with id a0; intros Hs.
now eapply substitution in Hs.
- now eapply substitution in b1.
+ rewrite subst_context_snoc /= /subst_decl /map_decl /= Nat.add_0_r.
intuition auto.
eapply substitution in b; eauto.
Qed.
Lemma subst_sorts_local_ctx {cf:checker_flags} Σ Γ Δ Δ' s ctxs :
wf Σ.1 →
wf_local Σ (Γ ,,, Δ) →
sorts_local_ctx (lift_typing typing) Σ (Γ ,,, Δ) Δ' ctxs →
subslet Σ Γ s Δ →
sorts_local_ctx (lift_typing typing) Σ Γ (subst_context s 0 Δ') ctxs.
Proof.
induction Δ' in ctxs |- *; simpl; auto.
destruct a as [na [b|] ty]; simpl; intuition auto.
+ simpl; rewrite subst_context_snoc /= /subst_decl /map_decl /= Nat.add_0_r.
repeat split.
- now apply IHΔ'.
- apply infer_typing_sort_impl with id a0; intros Hs.
now eapply substitution in Hs.
- now eapply substitution in b1.
+ rewrite subst_context_snoc /= /subst_decl /map_decl /= Nat.add_0_r.
destruct ctxs; auto.
intuition auto.
eapply substitution in b; eauto.
Qed.
Lemma weaken_type_local_ctx {cf:checker_flags} Σ Γ Γ' Δ ctxs :
wf Σ.1 →
wf_local Σ Γ →
type_local_ctx (lift_typing typing) Σ Γ' Δ ctxs →
type_local_ctx (lift_typing typing) Σ (Γ ,,, Γ') Δ ctxs.
Proof.
induction Δ; simpl; auto.
destruct a as [na [b|] ty]; simpl; intuition auto.
1: apply infer_typing_sort_impl with id a0; intros Hs.
all: rewrite -app_context_assoc.
all: eapply (weaken_ctx Γ); auto.
Qed.
Lemma weaken_sorts_local_ctx {cf:checker_flags} Σ Γ Γ' Δ ctxs :
wf Σ.1 →
wf_local Σ Γ →
sorts_local_ctx (lift_typing typing) Σ Γ' Δ ctxs →
sorts_local_ctx (lift_typing typing) Σ (Γ ,,, Γ') Δ ctxs.
Proof.
induction Δ in ctxs |- *; simpl; auto.
destruct a as [na [b|] ty]; simpl; intuition auto.
1: apply infer_typing_sort_impl with id a0; intros Hs.
all: rewrite -app_context_assoc.
3: destruct ctxs; auto.
3: destruct X1; split; auto.
all: now eapply (weaken_ctx Γ).
Qed.
Lemma reln_app acc Γ Δ k : reln acc k (Γ ++ Δ) =
reln (reln acc k Γ) (#|Γ| + k) Δ.
Proof.
induction Γ in acc, Δ, k |- *; simpl; auto.
destruct a as [na [b|] ty]. rewrite IHΓ. f_equal. lia.
simpl. rewrite IHΓ. f_equal. lia.
Qed.
Lemma reln_acc acc k Γ : reln acc k Γ = reln [] k Γ ++ acc.
Proof.
induction Γ in acc, k |- *; simpl; auto.
destruct a as [na [b|] ty]. rewrite IHΓ. f_equal.
rewrite IHΓ. rewrite [reln [_] _ _]IHΓ.
now rewrite -app_assoc.
Qed.
Lemma to_extended_list_k_app Γ Δ k : to_extended_list_k (Γ ++ Δ) k =
to_extended_list_k Δ (#|Γ| + k) ++ to_extended_list_k Γ k.
Proof.
unfold to_extended_list_k. now rewrite reln_app reln_acc.
Qed.
Lemma to_extended_list_k_fold_context_k f Γ k :
to_extended_list_k (fold_context_k f Γ) k = to_extended_list_k Γ k.
Proof.
rewrite /to_extended_list_k.
generalize (@nil term).
induction Γ in k |- ×.
simpl; auto.
intros.
rewrite fold_context_k_snoc0. simpl.
destruct a as [? [?|] ?] ⇒ /=; now rewrite IHΓ.
Qed.
Lemma to_extended_list_k_lift_context c k n k' :
to_extended_list_k (lift_context n k c) k' = to_extended_list_k c k'.
Proof. now rewrite to_extended_list_k_fold_context_k. Qed.
Lemma reln_lift n k Γ : reln [] (n + k) Γ = map (lift0 n) (reln [] k Γ).
Proof.
induction Γ in n, k |- *; simpl; auto.
destruct a as [? [?|] ?]; simpl.
now rewrite -IHΓ Nat.add_assoc.
rewrite reln_acc [reln [tRel k] _ _]reln_acc map_app /=.
f_equal. now rewrite -IHΓ Nat.add_assoc.
Qed.
Lemma to_extended_list_length Γ : #|to_extended_list Γ| = context_assumptions Γ.
Proof. now rewrite /to_extended_list to_extended_list_k_length. Qed.
#[global]
Hint Rewrite to_extended_list_length : len.
Lemma map_subst_app_to_extended_list_k s s' ctx k :
k = #|s| →
map (subst0 (s ++ s')) (to_extended_list_k ctx k) =
map (subst0 s') (to_extended_list_k ctx 0).
Proof.
intros →.
rewrite /to_extended_list_k.
rewrite -{1}(Nat.add_0_r #|s|) reln_lift map_map_compose.
apply map_ext. intros x; simpl.
rewrite subst_app_decomp.
f_equal. rewrite -{1}(Nat.add_0_r #|s|) simpl_subst' ?lift0_id //.
now rewrite map_length.
Qed.
Lemma subst_context_smash_context s k Γ Δ :
subst_context s k (smash_context Γ Δ) =
smash_context (subst_context s (#|Δ| + k) Γ) (subst_context s k Δ).
Proof.
induction Δ as [|[? [] ?] ?] in Γ |- *; simpl; auto;
rewrite subst_context_snoc; simpl.
- rewrite IHΔ. f_equal.
rewrite !subst_context_alt !mapi_mapi. apply mapi_ext. clear.
intros n x. rewrite /subst_decl !compose_map_decl.
eapply map_decl_ext. intros.
autorewrite with len.
generalize (Nat.pred #|Γ| - n). generalize (#|Δ| + k). clear.
intros. rewrite distr_subst_rec. simpl. now rewrite -Nat.add_assoc.
- rewrite IHΔ. f_equal.
rewrite subst_context_app. simpl. unfold app_context. f_equal.
Qed.
Section WfEnv.
Context {cf} {Σ} {wfΣ : wf Σ}.
Lemma wf_local_rel_smash_context_gen {Γ Δ Δ'} :
wf_local Σ (Δ' ,,, Γ) →
wf_local_rel Σ (Δ' ,,, Γ) Δ →
wf_local_rel Σ Δ' (smash_context Δ Γ).
Proof using wfΣ.
induction Γ in Δ |- *; simpl; auto.
intros wfΓ wfΔ. depelim wfΓ; simpl.
- apply IHΓ; auto. eapply All_local_env_app. split; auto.
repeat constructor; auto.
eapply All_local_env_impl; eauto. simpl; intros.
now rewrite app_context_assoc.
- apply IHΓ. auto. eapply All_local_env_subst; eauto. simpl; intros.
destruct T; simpl in *; pcuicfo auto.
2: apply infer_typing_sort_impl with id X; intros Hs.
1: rename X into Hs.
all: rewrite Nat.add_0_r.
all: eapply (substitution (Γ':=[vdef na b t]) (s := [b])) in Hs; eauto.
all: rewrite -{1}(subst_empty 0 b).
all: repeat constructor.
all: now rewrite !subst_empty.
Qed.
Lemma wf_local_rel_smash_context {Γ Δ} :
wf_local Σ (Δ ,,, Γ) →
wf_local_rel Σ Δ (smash_context [] Γ).
Proof using wfΣ.
intros. eapply wf_local_rel_smash_context_gen; eauto. constructor.
Qed.
Lemma wf_local_smash_end Γ Δ :
wf_local Σ (Γ ,,, Δ) → wf_local Σ (Γ ,,, smash_context [] Δ).
Proof using wfΣ.
intros wf.
apply All_local_env_app. split.
now apply All_local_env_app_inv in wf.
eapply wf_local_rel_smash_context; auto.
Qed.
Lemma wf_local_rel_empty Γ : wf_local_rel Σ [] Γ <~> wf_local Σ Γ.
Proof using Type.
split.
- intros h. eapply (All_local_env_impl _ _ _ h). pcuicfo.
red in X |- ×. now rewrite app_context_nil_l in X.
- intros h. eapply (All_local_env_impl _ _ _ h). pcuicfo.
red in X |- ×. now rewrite app_context_nil_l.
Qed.
Lemma wf_local_smash_context {Γ} :
wf_local Σ Γ → wf_local Σ (smash_context [] Γ).
Proof using wfΣ.
intros; apply wf_local_rel_empty. eapply wf_local_rel_smash_context.
rewrite ?app_context_nil_l; eauto.
Qed.
End WfEnv.
Local Open Scope sigma_scope.
Lemma context_subst_extended_subst Γ args s :
context_subst Γ args s →
s = map (inst (List.rev args ⋅n ids)) (extended_subst Γ 0).
Proof.
induction 1.
- simpl; auto.
- simpl.
rewrite lift_extended_subst.
rewrite map_map_compose.
rewrite List.rev_app_distr. simpl. f_equal.
rewrite IHX. apply map_ext.
intros. autorewrite with sigma.
apply inst_ext.
rewrite subst_consn_subst_cons.
now rewrite subst_cons_shift.
- simpl.
f_equal; auto. len.
rewrite IHX.
autorewrite with sigma.
apply inst_ext. len.
rewrite (Upn_eq _ (List.rev args ⋅n ids)).
rewrite subst_consn_compose.
rewrite PCUICInstConv.map_inst_idsn; len; try lia.
rewrite subst_compose_assoc.
rewrite -(context_subst_length2 X).
rewrite subst_consn_shiftn; len ⇒ //.
sigma. rewrite Upn_eq. sigma.
rewrite PCUICInstConv.map_inst_idsn; len; try lia.
rewrite -subst_compose_assoc shiftk_compose.
rewrite -subst_consn_app.
rewrite subst_consn_shiftn //. now len.
Qed.
Lemma map_subst_app_decomp (l l' : list term) (k : nat) (ts : list term) :
map (subst (l ++ l') k) ts = map (fun x ⇒ subst l' k (subst (map (lift0 #|l'|) l) k x)) ts.
Proof.
apply map_ext. apply subst_app_decomp.
Qed.
Lemma map_reln_ext (f g : term → term) k Γ :
(∀ n, n < #|Γ| → f (tRel (k + n)) = g (tRel (k + n))) →
map f (reln [] k Γ) = map g (reln [] k Γ).
Proof.
intros Hf.
induction Γ as [|[? [] ?] ?] in k, Hf |- *; simpl; auto.
- rewrite reln_acc map_app. simpl.
rewrite map_app /=. rewrite IHΓ //.
intros. simpl in Hf. specialize (Hf (S n)).
forward Hf. lia. rewrite -Nat.add_assoc. apply Hf.
- rewrite reln_acc map_app. simpl.
rewrite map_app /= IHΓ //.
intros. simpl in Hf. specialize (Hf (S n)).
forward Hf. lia. rewrite -Nat.add_assoc. apply Hf.
f_equal. f_equal. specialize (Hf 0). simpl in Hf.
forward Hf by lia. now rewrite Nat.add_0_r in Hf.
Qed.
Lemma extended_subst_to_extended_list_k Γ k :
(map (subst (extended_subst Γ 0) k) (to_extended_list_k Γ k)) =
to_extended_list_k (smash_context [] Γ) k.
Proof.
unfold to_extended_list_k.
induction Γ in k |- ×. simpl. reflexivity.
destruct a as [? [] ?]; simpl.
- rewrite smash_context_acc //.
rewrite reln_app. autorewrite with len. simpl.
rewrite -IHΓ //. rewrite Nat.add_1_r.
rewrite (reln_lift 1).
clear.
rewrite (map_subst_app_decomp [_]).
rewrite -map_map_compose. f_equal.
simpl.
generalize (lift0 #|extended_subst Γ 0|
(subst0 (extended_subst Γ 0) (lift (context_assumptions Γ) #|Γ| t))).
intros t0.
change 1 with #|[t0]|.
generalize [t0]. clear.
intros l. generalize (Nat.le_refl k).
generalize k at 1 3.
induction Γ as [|[? [] ?] ?] in k, l |- *; simpl. reflexivity.
simpl. intros k0 le0. apply IHΓ. lia.
intros k0 lek0. rewrite reln_acc map_app. simpl.
rewrite map_app. simpl.
elim: leb_spec_Set ⇒ Hle. f_equal. apply IHΓ. lia.
f_equal. elim: nth_error_spec ⇒ [x Hx Hl|Hl]. lia.
f_equal. lia. lia.
- rewrite smash_context_acc //.
simpl.
rewrite reln_acc map_app.
rewrite (reln_acc [_] _ (smash_context [] Γ)).
simpl. rewrite Nat.leb_refl Nat.sub_diag /=. f_equal.
rewrite -IHΓ //.
2:{ do 2 f_equal; lia. }
apply map_reln_ext ⇒ n Hn.
rewrite lift_extended_subst //.
replace (k + 1 + n) with (S (k + n)) by lia.
simpl.
elim: leb_spec_Set ⇒ Hle; [|lia].
elim: leb_spec_Set ⇒ Hle'; [|lia].
replace (S (k + n) - k) with (S n) by lia.
replace (S (k + n) - (k + 1)) with n by lia.
simpl.
rewrite nth_error_map.
elim: nth_error_spec ⇒ [x Hx Hlen|Hlen].
simpl. rewrite simpl_lift; try lia. f_equal. simpl.
autorewrite with len in Hlen. lia.
Qed.
Lemma assumption_context_fold f Γ :
assumption_context Γ → assumption_context (fold_context_k f Γ).
Proof.
induction 1; simpl. constructor. rewrite fold_context_k_snoc0.
now constructor.
Qed.
Lemma smash_context_app_expand Γ Δ Δ' :
smash_context Γ (Δ ,,, Δ') =
smash_context [] Δ ,,, expand_lets_ctx Δ (smash_context Γ Δ').
Proof.
rewrite smash_context_app smash_context_acc.
rewrite /expand_lets_k_ctx /app_context. f_equal.
Qed.
Lemma expand_lets_smash_context Γ Δ Δ' :
expand_lets_ctx Γ (smash_context Δ Δ') =
smash_context (expand_lets_k_ctx Γ #|Δ'| Δ) (expand_lets_ctx Γ Δ').
Proof.
rewrite /expand_lets_ctx /expand_lets_k_ctx.
rewrite -smash_context_lift -smash_context_subst /=; len.
Qed.
Lemma expand_lets_k_ctx_nil Γ k : expand_lets_k_ctx Γ k [] = [].
Proof. reflexivity. Qed.
Lemma expand_lets_ctx_nil Γ : expand_lets_ctx Γ [] = [].
Proof. reflexivity. Qed.
#[global]
Hint Rewrite expand_lets_k_ctx_nil expand_lets_ctx_nil : pcuic.
Definition subst_let_expand args Δ T :=
(subst0 args (expand_lets Δ T)).
Definition subst_context_let_expand args Δ Γ :=
(subst_context args 0 (expand_lets_ctx Δ Γ)).
Definition subst_let_expand_tProd args Δ na T s :
subst_let_expand args Δ (tProd na T (tSort s)) =
tProd na (subst_let_expand args Δ T) (tSort s).
Proof.
reflexivity.
Qed.
Definition subst_let_expand_mkApps s Δ f args :
subst_let_expand s Δ (mkApps f args) =
mkApps (subst_let_expand s Δ f) (map (subst_let_expand s Δ) args).
Proof.
rewrite /subst_let_expand.
now rewrite expand_lets_mkApps subst_mkApps map_map_compose.
Qed.
Definition subst_let_expand_tInd s Δ ind u :
subst_let_expand s Δ (tInd ind u) = tInd ind u.
Proof. reflexivity. Qed.
Lemma subst_let_expand_it_mkProd_or_LetIn s Γ Δ u :
subst_let_expand s Γ (it_mkProd_or_LetIn Δ (tSort u)) =
it_mkProd_or_LetIn (subst_context_let_expand s Γ Δ) (tSort u).
Proof.
rewrite /subst_let_expand /expand_lets.
rewrite expand_lets_it_mkProd_or_LetIn /= subst_it_mkProd_or_LetIn /=.
reflexivity.
Qed.
Lemma subst_lift_above s n k x : k = #|s| → subst0 s (lift0 (n + k) x) = lift0 n x.
Proof.
intros. rewrite Nat.add_comm. subst k. now rewrite simpl_subst.
Qed.
Lemma subst_let_expand_lift_id s Δ k x :
k = #|Δ| →
#|s| = context_assumptions Δ →
subst_let_expand s Δ (lift0 k x) = x.
Proof.
intros → hl.
rewrite /subst_let_expand /expand_lets /expand_lets_k.
simpl.
rewrite simpl_lift; len; try lia.
rewrite subst_lift_above. now len.
change (context_assumptions Δ) with (0 + context_assumptions Δ).
rewrite subst_lift_above. len. now rewrite lift0_id.
Qed.
Lemma subslet_lift {cf} {Σ} {wfΣ : wf Σ} (Γ Δ : context) s Δ' :
wf_local Σ (Γ ,,, Δ) →
subslet Σ Γ s Δ' →
subslet Σ (Γ ,,, Δ) (map (lift0 #|Δ|) s) (lift_context #|Δ| 0 Δ').
Proof.
move⇒ wfl.
induction 1; rewrite ?lift_context_snoc /=; try constructor; auto.
simpl.
rewrite -(subslet_length X).
rewrite -distr_lift_subst. apply weakening; eauto.
rewrite -(subslet_length X).
rewrite distr_lift_subst. constructor; auto.
rewrite - !distr_lift_subst. apply weakening; eauto.
Qed.
Lemma untyped_subslet_lift (Γ Δ : context) s Δ' :
untyped_subslet Γ s Δ' →
untyped_subslet (Γ ,,, Δ) (map (lift0 #|Δ|) s) (lift_context #|Δ| 0 Δ').
Proof.
induction 1; rewrite ?lift_context_snoc /=; try constructor; auto.
simpl.
rewrite -(untyped_subslet_length X).
rewrite distr_lift_subst. constructor; auto.
Qed.
Lemma untyped_subslet_extended_subst Γ Δ :
untyped_subslet (Γ ,,, smash_context [] Δ)
(extended_subst Δ 0)
(lift_context (context_assumptions Δ) 0 Δ).
Proof.
induction Δ as [|[na [d|] ?] ?]; simpl; try constructor.
× rewrite lift_context_snoc /lift_decl /= /map_decl /=.
len.
constructor ⇒ //.
× rewrite smash_context_acc. simpl.
rewrite /map_decl /= /map_decl /=. simpl.
rewrite lift_context_snoc /lift_decl /= /map_decl /=.
constructor.
rewrite (lift_extended_subst _ 1).
rewrite -(lift_context_lift_context 1 _).
eapply (untyped_subslet_lift _ [_]); eauto.
Qed.
Lemma subslet_extended_subst {cf} {Σ} {wfΣ : wf Σ} Γ Δ :
wf_local Σ (Γ ,,, Δ) →
subslet Σ (Γ ,,, smash_context [] Δ)
(extended_subst Δ 0)
(lift_context (context_assumptions Δ) 0 Δ).
Proof.
move⇒ wfΔ.
eapply wf_local_app_inv in wfΔ as [wfΓ wfΔ].
induction Δ as [|[na [d|] ?] ?] in wfΔ |- *; simpl; try constructor.
× depelim wfΔ. repeat red in l, l0.
specialize (IHΔ wfΔ).
rewrite lift_context_snoc /lift_decl /= /map_decl /=.
len.
constructor ⇒ //.
eapply (weakening_typing (Γ'' := smash_context [] Δ)) in l0.
len in l0. simpl in l0. simpl.
2:{ eapply wf_local_smash_end; pcuic. }
eapply (substitution (Δ := [])) in l0; tea.
× rewrite smash_context_acc. simpl.
rewrite /map_decl /= /map_decl /=. simpl.
depelim wfΔ.
specialize (IHΔ wfΔ).
rewrite lift_context_snoc /lift_decl /= /map_decl /=.
constructor.
- rewrite (lift_extended_subst _ 1).
rewrite -(lift_context_lift_context 1 _).
eapply (subslet_lift _ [_]); eauto.
constructor.
{ pose proof l.π2. eapply wf_local_smash_end; pcuic. }
apply infer_typing_sort_impl with id l; intros Hs.
eapply (weakening_typing (Γ'' := smash_context [] Δ)) in Hs.
len in Hs. simpl in Hs. simpl.
2:{ eapply wf_local_smash_end; pcuic. }
eapply (substitution (Δ := [])) in Hs; tea.
- eapply meta_conv.
econstructor. constructor. apply wf_local_smash_end; auto.
eapply wf_local_app; eauto.
apply infer_typing_sort_impl with id l; intros Hs.
eapply (weakening_typing (Γ'' := smash_context [] Δ)) in Hs.
len in Hs. simpl in Hs. simpl.
2:{ eapply wf_local_smash_end; pcuic. }
eapply (substitution (Δ := [])) in Hs; tea.
reflexivity.
simpl. rewrite (lift_extended_subst _ 1).
rewrite distr_lift_subst. f_equal. len.
now rewrite simpl_lift; try lia.
Qed.
Lemma typing_expand_lets {cf} {Σ} {wfΣ : wf Σ} Γ Δ t T :
Σ ;;; Γ ,,, Δ |- t : T →
Σ ;;; Γ ,,, smash_context [] Δ |- expand_lets Δ t : expand_lets Δ T.
Proof.
intros Ht.
rewrite /expand_lets /expand_lets_k.
pose proof (typing_wf_local Ht).
eapply (weakening_typing (Γ'' := smash_context [] Δ)) in Ht.
len in Ht. simpl in Ht. simpl.
2:{ eapply wf_local_smash_end; pcuic. }
eapply (substitution (Δ := [])) in Ht; tea.
now eapply subslet_extended_subst.
Qed.
Lemma subst_context_let_expand_length s Γ Δ :
#|subst_context_let_expand s Γ Δ| = #|Δ|.
Proof.
now rewrite /subst_context_let_expand; len.
Qed.
#[global]
Hint Rewrite subst_context_let_expand_length : len.
Lemma to_extended_list_subst_context_let_expand s Γ Δ :
to_extended_list (subst_context_let_expand s Γ Δ) =
to_extended_list Δ.
Proof.
rewrite /subst_context_let_expand /to_extended_list /expand_lets_ctx /expand_lets_k_ctx.
now rewrite !to_extended_list_k_subst to_extended_list_k_lift_context.
Qed.
Lemma map2_set_binder_name_alpha (nas : list aname) (Δ Δ' : context) :
All2 (fun x y ⇒ eq_binder_annot x (decl_name y)) nas Δ →
eq_context_upto_names Δ Δ' →
eq_context_upto_names (map2 set_binder_name nas Δ) Δ'.
Proof.
intros hl. induction 1 in nas, hl |- *; cbn; auto.
destruct nas; cbn; auto.
destruct nas; cbn; auto; depelim hl.
constructor; auto. destruct r; subst; cbn; constructor; auto;
now transitivity na.
Qed.
Notation eq_names := (All2 (fun x y ⇒ x = (decl_name y))).
Lemma eq_names_subst_context nas Γ s k :
eq_names nas Γ →
eq_names nas (subst_context s k Γ).
Proof.
induction 1.
× cbn; auto. constructor.
× rewrite subst_context_snoc. constructor; auto.
Qed.
Lemma eq_names_subst_instance nas Γ u :
eq_names nas Γ →
eq_names nas (subst_instance u Γ).
Proof.
induction 1.
× cbn; auto.
× rewrite /subst_instance /=. constructor; auto.
Qed.
Lemma map2_set_binder_name_alpha_eq (nas : list aname) (Δ Δ' : context) :
eq_names nas Δ' →
eq_context_upto_names Δ Δ' →
(map2 set_binder_name nas Δ) = Δ'.
Proof.
intros hl. induction 1 in nas, hl |- *; cbn; auto.
destruct nas; cbn; auto.
destruct nas; cbn; auto; depelim hl.
f_equal; auto. destruct r; subst; cbn; auto.
Qed.