Mcltt.Core.Soundness.Realizability
From Coq Require Import Nat.
From Mcltt Require Import Base LibTactics.
From Mcltt.Core.Syntactic Require Import CtxSub Corollaries.
From Mcltt.Core.Semantic Require Import Realizability.
From Mcltt.Core.Soundness Require Export LogicalRelation.Core Weakening.
Import Domain_Notations.
Open Scope list_scope.
Lemma wf_ctx_sub_ctx_lookup : forall n A Γ,
{{ #n : A ∈ Γ }} ->
forall Δ,
{{ ⊢ Δ ⊆ Γ}} ->
exists Δ1 A0 Δ2 A',
Δ = Δ1 ++ A0 :: Δ2 /\
n = length Δ1 /\
A' = iter (S n) (fun A => {{{ A[Wk] }}}) A0 /\
{{ #n : A' ∈ Δ }} /\
{{ Δ ⊢ A' ⊆ A }}.
Proof.
induction 1; intros; progressive_inversion.
- exists nil.
repeat eexists; mauto 4.
- edestruct IHctx_lookup as [Δ1 [? [? [? [? [? [? []]]]]]]]; eauto 3.
exists (A0 :: Δ1). subst.
repeat eexists; mauto 4.
Qed.
Lemma var_arith : forall Γ1 Γ2 (A : typ),
length (Γ1 ++ A :: Γ2) - length Γ2 - 1 = length Γ1.
Proof.
intros.
rewrite List.length_app. simpl.
lia.
Qed.
Lemma var_weaken_gen : forall Δ σ Γ,
{{ Δ ⊢w σ : Γ }} ->
forall Γ1 Γ2 A0,
Γ = Γ1 ++ A0 :: Γ2 ->
{{ Δ ⊢ #(length Γ1)[σ] ≈ #(length Δ - length Γ2 - 1) : ~(iter (S (length Γ1)) (fun A => {{{ A[Wk] }}}) A0)[σ] }}.
Proof.
induction 1; intros; subst; gen_presups.
- pose proof (app_ctx_vlookup _ _ _ _ HΔ eq_refl) as Hvar.
gen_presup Hvar.
clear_dups.
apply wf_sub_id_inversion in Hτ.
pose proof (wf_ctx_sub_length _ _ Hτ).
transitivity {{{ #(length Γ1)[Id] }}}; [mauto 3 |].
replace (length Γ) with (length (Γ1 ++ {{{ Γ2, A0 }}})) by lia.
rewrite var_arith, H.
bulky_rewrite.
- pose proof (app_ctx_vlookup _ _ _ _ HΔ0 eq_refl) as Hvar.
pose proof (app_ctx_lookup Γ1 A0 Γ2 _ eq_refl).
gen_presup Hvar.
clear_dups.
assert {{ ⊢ Δ', A }} by mauto 3.
assert {{ Δ', A ⊢s Wk : ~ (Γ1 ++ {{{ Γ2, A0 }}}) }} by mauto 3.
transitivity {{{ #(length Γ1)[Wk∘τ] }}}; [mauto 3 |].
rewrite H1.
etransitivity; [eapply wf_exp_eq_sub_compose; mauto 3 |].
pose proof (wf_ctx_sub_length _ _ H0).
rewrite <- @exp_eq_sub_compose_typ; mauto 2.
deepexec wf_ctx_sub_ctx_lookup ltac:(fun H => destruct H as [Γ1' [? [Γ2' [? [-> [? [-> []]]]]]]]).
repeat rewrite List.length_app in *.
replace (length Γ1) with (length Γ1') in * by lia.
clear_refl_eqs.
replace (length Γ2) with (length Γ2') by (simpl in *; lia).
etransitivity.
+ eapply wf_exp_eq_sub_cong; [ |mauto 3].
eapply wf_exp_eq_subtyp'.
* eapply wf_exp_eq_var_weaken; [mauto 3|]; eauto.
* mauto 4.
+ eapply wf_exp_eq_subtyp'.
* eapply IHweakening with (Γ1 := A :: _).
reflexivity.
* eapply wf_subtyp_subst; [ |mauto 3].
simpl. eapply wf_subtyp_subst; mauto 3.
Qed.
Lemma var_glu_elem_bot : forall a i P El Γ A,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
{{ Γ ⊢ A ® P }} ->
{{ Γ, A ⊢ #0 : A[Wk] ® !(length Γ) ∈ glu_elem_bot i a }}.
Proof.
intros. saturate_glu_info.
econstructor; mauto 4.
- eapply glu_univ_elem_typ_monotone; eauto.
mauto 4.
- intros. progressive_inversion.
exact (var_weaken_gen _ _ _ H2 nil _ _ eq_refl).
Qed.
#[local]
Hint Rewrite -> wf_sub_eq_extend_compose using mauto 4 : mcltt.
Theorem realize_glu_univ_elem_gen : forall a i P El,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
(forall Γ A R,
{{ DF a ≈ a ∈ per_univ_elem i ↘ R }} ->
{{ Γ ⊢ A ® P }} ->
{{ Γ ⊢ A ® glu_typ_top i a }}) /\
(forall Γ M A m,
From Mcltt Require Import Base LibTactics.
From Mcltt.Core.Syntactic Require Import CtxSub Corollaries.
From Mcltt.Core.Semantic Require Import Realizability.
From Mcltt.Core.Soundness Require Export LogicalRelation.Core Weakening.
Import Domain_Notations.
Open Scope list_scope.
Lemma wf_ctx_sub_ctx_lookup : forall n A Γ,
{{ #n : A ∈ Γ }} ->
forall Δ,
{{ ⊢ Δ ⊆ Γ}} ->
exists Δ1 A0 Δ2 A',
Δ = Δ1 ++ A0 :: Δ2 /\
n = length Δ1 /\
A' = iter (S n) (fun A => {{{ A[Wk] }}}) A0 /\
{{ #n : A' ∈ Δ }} /\
{{ Δ ⊢ A' ⊆ A }}.
Proof.
induction 1; intros; progressive_inversion.
- exists nil.
repeat eexists; mauto 4.
- edestruct IHctx_lookup as [Δ1 [? [? [? [? [? [? []]]]]]]]; eauto 3.
exists (A0 :: Δ1). subst.
repeat eexists; mauto 4.
Qed.
Lemma var_arith : forall Γ1 Γ2 (A : typ),
length (Γ1 ++ A :: Γ2) - length Γ2 - 1 = length Γ1.
Proof.
intros.
rewrite List.length_app. simpl.
lia.
Qed.
Lemma var_weaken_gen : forall Δ σ Γ,
{{ Δ ⊢w σ : Γ }} ->
forall Γ1 Γ2 A0,
Γ = Γ1 ++ A0 :: Γ2 ->
{{ Δ ⊢ #(length Γ1)[σ] ≈ #(length Δ - length Γ2 - 1) : ~(iter (S (length Γ1)) (fun A => {{{ A[Wk] }}}) A0)[σ] }}.
Proof.
induction 1; intros; subst; gen_presups.
- pose proof (app_ctx_vlookup _ _ _ _ HΔ eq_refl) as Hvar.
gen_presup Hvar.
clear_dups.
apply wf_sub_id_inversion in Hτ.
pose proof (wf_ctx_sub_length _ _ Hτ).
transitivity {{{ #(length Γ1)[Id] }}}; [mauto 3 |].
replace (length Γ) with (length (Γ1 ++ {{{ Γ2, A0 }}})) by lia.
rewrite var_arith, H.
bulky_rewrite.
- pose proof (app_ctx_vlookup _ _ _ _ HΔ0 eq_refl) as Hvar.
pose proof (app_ctx_lookup Γ1 A0 Γ2 _ eq_refl).
gen_presup Hvar.
clear_dups.
assert {{ ⊢ Δ', A }} by mauto 3.
assert {{ Δ', A ⊢s Wk : ~ (Γ1 ++ {{{ Γ2, A0 }}}) }} by mauto 3.
transitivity {{{ #(length Γ1)[Wk∘τ] }}}; [mauto 3 |].
rewrite H1.
etransitivity; [eapply wf_exp_eq_sub_compose; mauto 3 |].
pose proof (wf_ctx_sub_length _ _ H0).
rewrite <- @exp_eq_sub_compose_typ; mauto 2.
deepexec wf_ctx_sub_ctx_lookup ltac:(fun H => destruct H as [Γ1' [? [Γ2' [? [-> [? [-> []]]]]]]]).
repeat rewrite List.length_app in *.
replace (length Γ1) with (length Γ1') in * by lia.
clear_refl_eqs.
replace (length Γ2) with (length Γ2') by (simpl in *; lia).
etransitivity.
+ eapply wf_exp_eq_sub_cong; [ |mauto 3].
eapply wf_exp_eq_subtyp'.
* eapply wf_exp_eq_var_weaken; [mauto 3|]; eauto.
* mauto 4.
+ eapply wf_exp_eq_subtyp'.
* eapply IHweakening with (Γ1 := A :: _).
reflexivity.
* eapply wf_subtyp_subst; [ |mauto 3].
simpl. eapply wf_subtyp_subst; mauto 3.
Qed.
Lemma var_glu_elem_bot : forall a i P El Γ A,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
{{ Γ ⊢ A ® P }} ->
{{ Γ, A ⊢ #0 : A[Wk] ® !(length Γ) ∈ glu_elem_bot i a }}.
Proof.
intros. saturate_glu_info.
econstructor; mauto 4.
- eapply glu_univ_elem_typ_monotone; eauto.
mauto 4.
- intros. progressive_inversion.
exact (var_weaken_gen _ _ _ H2 nil _ _ eq_refl).
Qed.
#[local]
Hint Rewrite -> wf_sub_eq_extend_compose using mauto 4 : mcltt.
Theorem realize_glu_univ_elem_gen : forall a i P El,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
(forall Γ A R,
{{ DF a ≈ a ∈ per_univ_elem i ↘ R }} ->
{{ Γ ⊢ A ® P }} ->
{{ Γ ⊢ A ® glu_typ_top i a }}) /\
(forall Γ M A m,
We repeat this to get the relation between a and P
more easily after applying induction 1.
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
{{ Γ ⊢ M : A ® m ∈ glu_elem_bot i a }} ->
{{ Γ ⊢ M : A ® ⇑ a m ∈ El }}) /\
(forall Γ M A m R,
{{ Γ ⊢ M : A ® m ∈ glu_elem_bot i a }} ->
{{ Γ ⊢ M : A ® ⇑ a m ∈ El }}) /\
(forall Γ M A m R,
We repeat this to get the relation between a and P
more easily after applying induction 1.
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
{{ Γ ⊢ M : A ® m ∈ El }} ->
{{ DF a ≈ a ∈ per_univ_elem i ↘ R }} ->
{{ Dom m ≈ m ∈ R }} ->
{{ Γ ⊢ M : A ® m ∈ glu_elem_top i a }}).
Proof.
simpl. induction 1 using glu_univ_elem_ind.
all:split; [| split]; intros;
apply_equiv_left;
gen_presups;
try match_by_head1 per_univ_elem ltac:(fun H => pose proof (per_univ_then_per_top_typ H));
match_by_head glu_elem_bot ltac:(fun H => destruct H as []);
destruct_all.
- econstructor; eauto; intros.
progressive_inversion.
transitivity {{{ Type@j[σ] }}}; mauto 4.
- handle_functional_glu_univ_elem.
match_by_head glu_univ_elem invert_glu_univ_elem.
clear_dups.
apply_equiv_left.
repeat split; eauto.
repeat eexists.
+ glu_univ_elem_econstructor; eauto; reflexivity.
+ simpl. repeat split.
* rewrite <- H5. trivial.
* intros.
saturate_weakening_escape.
rewrite <- wf_exp_eq_typ_sub; try eassumption.
rewrite <- H5.
firstorder.
- deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
firstorder.
specialize (H _ _ _ H10) as [? []].
econstructor; mauto 3.
+ apply_equiv_left. trivial.
+ intros.
saturate_weakening_escape.
deepexec H ltac:(fun H => destruct H).
progressive_invert H16.
deepexec H20 ltac:(fun H => pose proof H).
functional_read_rewrite_clear.
bulky_rewrite.
- econstructor; eauto; intros.
progressive_inversion.
transitivity {{{ ℕ[σ] }}}; mauto 3.
- handle_functional_glu_univ_elem.
match_by_head glu_univ_elem invert_glu_univ_elem.
apply_equiv_left.
repeat split; eauto.
econstructor; trivial.
intros.
saturate_weakening_escape.
assert {{ Δ ⊢ A[σ] ≈ ℕ[σ] : Type @ i }} by mauto 3.
rewrite <- wf_exp_eq_nat_sub; try eassumption.
mauto 3.
- econstructor; mauto 3.
+ bulky_rewrite. mauto 3.
+ apply_equiv_left. trivial.
+ intros.
saturate_weakening_escape.
bulky_rewrite.
mauto using glu_nat_readback.
- match_by_head pi_glu_typ_pred progressive_invert.
handle_per_univ_elem_irrel.
invert_per_univ_elem H6.
econstructor; eauto; intros.
+ gen_presups. trivial.
+ saturate_weakening_escape.
assert {{ Γ ⊢w Id : Γ }} by mauto 4.
assert {{ Δ ⊢ IT[σ] ® IP }} by mauto 3.
assert (IP Γ {{{ IT[Id] }}}) as HITId by mauto 3.
bulky_rewrite_in HITId.
assert {{ Γ ⊢ IT[Id] ≈ IT : Type@i }} by mauto 3.
dir_inversion_clear_by_head read_typ.
assert {{ Γ ⊢ IT ® glu_typ_top i a }} as [] by mauto 3.
bulky_rewrite.
simpl. apply wf_exp_eq_pi_cong'; [firstorder |].
pose proof (var_per_elem (length Δ) H0).
destruct_rel_mod_eval.
simplify_evals.
destruct (H2 _ ltac:(eassumption) _ ltac:(eassumption)) as [? []].
assert (IEl {{{ Δ, IT[σ] }}} {{{ IT[σ][Wk] }}} {{{ #0 }}} d{{{ ⇑! a (length Δ) }}}) by mauto 3 using var_glu_elem_bot.
autorewrite with mcltt in H31.
specialize (H14 {{{ Δ, IT[σ] }}} {{{ σ∘Wk }}} _ _ ltac:(mauto) ltac:(eassumption) ltac:(eassumption)).
specialize (H8 _ _ _ ltac:(eassumption) ltac:(eassumption)) as [].
etransitivity; [| eapply H33]; mauto 3.
- handle_functional_glu_univ_elem.
apply_equiv_left.
invert_glu_rel1.
econstructor; try eapply per_bot_then_per_elem; eauto.
intros.
saturate_weakening_escape.
saturate_glu_info.
match_by_head1 per_univ_elem invert_per_univ_elem.
destruct_rel_mod_eval.
simplify_evals.
eexists; repeat split; mauto 3.
eapply H2; eauto.
assert {{ Δ ⊢ M[σ] : A[σ] }} by mauto 3.
bulky_rewrite_in H23.
unshelve (econstructor; eauto).
+ trivial.
+ eassert {{ Δ ⊢ M[σ] N : ~_ }} by (eapply wf_app'; eassumption).
autorewrite with mcltt in H25.
trivial.
+ mauto using domain_app_per.
+ intros.
saturate_weakening_escape.
progressive_invert H26.
destruct (H15 _ _ _ _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption) equiv_n).
handle_functional_glu_univ_elem.
autorewrite with mcltt.
etransitivity.
* rewrite sub_decompose_q_typ; mauto 4.
* simpl.
rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
rewrite <- @exp_eq_sub_compose_typ; mauto 3;
[eapply wf_exp_eq_app_cong' |].
-- specialize (H12 _ {{{σ ∘ σ0}}} _ ltac:(mauto 3) ltac:(eassumption)).
rewrite wf_exp_eq_sub_compose with (M := M) in H12; mauto 3.
bulky_rewrite_in H12.
-- rewrite <- @exp_eq_sub_compose_typ; mauto 3.
-- econstructor; mauto 3.
autorewrite with mcltt.
rewrite <- @exp_eq_sub_compose_typ; mauto 3.
- handle_functional_glu_univ_elem.
handle_per_univ_elem_irrel.
pose proof H8.
invert_per_univ_elem H8.
econstructor; mauto 3.
+ invert_glu_rel1. trivial.
+ eapply glu_univ_elem_trm_typ; eauto.
+ intros.
saturate_weakening_escape.
invert_glu_rel1. clear_dups.
progressive_invert H20.
assert {{ Γ ⊢w Id : Γ }} by mauto 4.
pose proof (H10 _ _ H24).
specialize (H10 _ _ H19).
assert {{ Γ ⊢ IT[Id] ≈ IT : Type@i }} by mauto 3.
bulky_rewrite_in H25.
destruct (H11 _ _ _ ltac:(eassumption) ltac:(eassumption)) as [].
specialize (H29 _ _ _ H19 H9).
rewrite H5 in *.
autorewrite with mcltt.
eassert {{ Δ ⊢ M[σ] : ~_ }} by (mauto 2).
autorewrite with mcltt in H30.
rewrite @wf_exp_eq_pi_eta' with (M := {{{ M[σ] }}}); [| trivial].
cbn [nf_to_exp].
eapply wf_exp_eq_fn_cong'; eauto.
pose proof (var_per_elem (length Δ) H0).
destruct_rel_mod_eval.
simplify_evals.
destruct (H2 _ ltac:(eassumption) _ ltac:(eassumption)) as [? []].
specialize (H12 _ _ _ _ ltac:(trivial) (var_glu_elem_bot _ _ _ _ _ _ H H10)).
autorewrite with mcltt in H12.
specialize (H14 {{{Δ, IT[σ]}}} {{{σ ∘ Wk}}} _ _ ltac:(mauto) ltac:(eassumption) ltac:(eassumption)) as [? []].
apply_equiv_left.
destruct_rel_mod_app.
simplify_evals.
deepexec H1 ltac:(fun H => pose proof H).
specialize (H33 _ _ _ _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption) ltac:(eassumption)) as [].
specialize (H40 _ {{{Id}}} _ ltac:(mauto 3) ltac:(eassumption)).
do 2 (rewrite wf_exp_eq_sub_id in H40; mauto 3).
etransitivity; [|eassumption].
simpl.
assert {{ Δ, IT[σ] ⊢ #0 : IT[σ∘Wk] }} by (rewrite <- @exp_eq_sub_compose_typ; mauto 3).
rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
rewrite <- @exp_eq_sub_compose_typ; mauto 2.
2:eapply sub_q; mauto 4.
2:gen_presup H41; econstructor; mauto 3.
eapply wf_exp_eq_app_cong'; [| mauto 3].
symmetry.
rewrite <- wf_exp_eq_pi_sub; mauto 4.
- econstructor; eauto.
intros.
progressive_inversion.
firstorder.
- handle_functional_glu_univ_elem.
apply_equiv_left.
econstructor; eauto.
- handle_functional_glu_univ_elem.
invert_glu_rel1.
econstructor; eauto.
+ intros s. destruct (H3 s) as [? []].
mauto.
+ intros.
progressive_inversion.
specialize (H11 (length Δ)) as [? []].
firstorder.
Qed.
Corollary realize_glu_typ_top : forall a i P El,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
forall Γ A,
{{ Γ ⊢ A ® P }} ->
{{ Γ ⊢ A ® glu_typ_top i a }}.
Proof.
intros.
pose proof H.
eapply glu_univ_elem_per_univ in H.
simpl in *. destruct_all.
eapply realize_glu_univ_elem_gen; eauto.
Qed.
Theorem realize_glu_elem_bot : forall a i P El,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
forall Γ A M m,
{{ Γ ⊢ M : A ® m ∈ glu_elem_bot i a }} ->
{{ Γ ⊢ M : A ® ⇑ a m ∈ El }}.
Proof.
intros.
eapply realize_glu_univ_elem_gen; eauto.
Qed.
Theorem realize_glu_elem_top : forall a i P El,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
forall Γ A M m,
{{ Γ ⊢ M : A ® m ∈ El }} ->
{{ Γ ⊢ M : A ® m ∈ glu_elem_top i a }}.
Proof.
intros.
pose proof H.
eapply glu_univ_elem_per_univ in H.
simpl in *. destruct_all.
eapply realize_glu_univ_elem_gen; eauto.
eapply glu_univ_elem_per_elem; eauto.
Qed.
#[export]
Hint Resolve realize_glu_typ_top realize_glu_elem_top : mcltt.
Corollary var0_glu_elem : forall {i a P El Γ A},
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
{{ Γ ⊢ A ® P }} ->
{{ Γ, A ⊢ #0 : A[Wk] ® ⇑! a (length Γ) ∈ El }}.
Proof.
intros.
eapply realize_glu_elem_bot; mauto 4.
eauto using var_glu_elem_bot.
Qed.
{{ Γ ⊢ M : A ® m ∈ El }} ->
{{ DF a ≈ a ∈ per_univ_elem i ↘ R }} ->
{{ Dom m ≈ m ∈ R }} ->
{{ Γ ⊢ M : A ® m ∈ glu_elem_top i a }}).
Proof.
simpl. induction 1 using glu_univ_elem_ind.
all:split; [| split]; intros;
apply_equiv_left;
gen_presups;
try match_by_head1 per_univ_elem ltac:(fun H => pose proof (per_univ_then_per_top_typ H));
match_by_head glu_elem_bot ltac:(fun H => destruct H as []);
destruct_all.
- econstructor; eauto; intros.
progressive_inversion.
transitivity {{{ Type@j[σ] }}}; mauto 4.
- handle_functional_glu_univ_elem.
match_by_head glu_univ_elem invert_glu_univ_elem.
clear_dups.
apply_equiv_left.
repeat split; eauto.
repeat eexists.
+ glu_univ_elem_econstructor; eauto; reflexivity.
+ simpl. repeat split.
* rewrite <- H5. trivial.
* intros.
saturate_weakening_escape.
rewrite <- wf_exp_eq_typ_sub; try eassumption.
rewrite <- H5.
firstorder.
- deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
firstorder.
specialize (H _ _ _ H10) as [? []].
econstructor; mauto 3.
+ apply_equiv_left. trivial.
+ intros.
saturate_weakening_escape.
deepexec H ltac:(fun H => destruct H).
progressive_invert H16.
deepexec H20 ltac:(fun H => pose proof H).
functional_read_rewrite_clear.
bulky_rewrite.
- econstructor; eauto; intros.
progressive_inversion.
transitivity {{{ ℕ[σ] }}}; mauto 3.
- handle_functional_glu_univ_elem.
match_by_head glu_univ_elem invert_glu_univ_elem.
apply_equiv_left.
repeat split; eauto.
econstructor; trivial.
intros.
saturate_weakening_escape.
assert {{ Δ ⊢ A[σ] ≈ ℕ[σ] : Type @ i }} by mauto 3.
rewrite <- wf_exp_eq_nat_sub; try eassumption.
mauto 3.
- econstructor; mauto 3.
+ bulky_rewrite. mauto 3.
+ apply_equiv_left. trivial.
+ intros.
saturate_weakening_escape.
bulky_rewrite.
mauto using glu_nat_readback.
- match_by_head pi_glu_typ_pred progressive_invert.
handle_per_univ_elem_irrel.
invert_per_univ_elem H6.
econstructor; eauto; intros.
+ gen_presups. trivial.
+ saturate_weakening_escape.
assert {{ Γ ⊢w Id : Γ }} by mauto 4.
assert {{ Δ ⊢ IT[σ] ® IP }} by mauto 3.
assert (IP Γ {{{ IT[Id] }}}) as HITId by mauto 3.
bulky_rewrite_in HITId.
assert {{ Γ ⊢ IT[Id] ≈ IT : Type@i }} by mauto 3.
dir_inversion_clear_by_head read_typ.
assert {{ Γ ⊢ IT ® glu_typ_top i a }} as [] by mauto 3.
bulky_rewrite.
simpl. apply wf_exp_eq_pi_cong'; [firstorder |].
pose proof (var_per_elem (length Δ) H0).
destruct_rel_mod_eval.
simplify_evals.
destruct (H2 _ ltac:(eassumption) _ ltac:(eassumption)) as [? []].
assert (IEl {{{ Δ, IT[σ] }}} {{{ IT[σ][Wk] }}} {{{ #0 }}} d{{{ ⇑! a (length Δ) }}}) by mauto 3 using var_glu_elem_bot.
autorewrite with mcltt in H31.
specialize (H14 {{{ Δ, IT[σ] }}} {{{ σ∘Wk }}} _ _ ltac:(mauto) ltac:(eassumption) ltac:(eassumption)).
specialize (H8 _ _ _ ltac:(eassumption) ltac:(eassumption)) as [].
etransitivity; [| eapply H33]; mauto 3.
- handle_functional_glu_univ_elem.
apply_equiv_left.
invert_glu_rel1.
econstructor; try eapply per_bot_then_per_elem; eauto.
intros.
saturate_weakening_escape.
saturate_glu_info.
match_by_head1 per_univ_elem invert_per_univ_elem.
destruct_rel_mod_eval.
simplify_evals.
eexists; repeat split; mauto 3.
eapply H2; eauto.
assert {{ Δ ⊢ M[σ] : A[σ] }} by mauto 3.
bulky_rewrite_in H23.
unshelve (econstructor; eauto).
+ trivial.
+ eassert {{ Δ ⊢ M[σ] N : ~_ }} by (eapply wf_app'; eassumption).
autorewrite with mcltt in H25.
trivial.
+ mauto using domain_app_per.
+ intros.
saturate_weakening_escape.
progressive_invert H26.
destruct (H15 _ _ _ _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption) equiv_n).
handle_functional_glu_univ_elem.
autorewrite with mcltt.
etransitivity.
* rewrite sub_decompose_q_typ; mauto 4.
* simpl.
rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
rewrite <- @exp_eq_sub_compose_typ; mauto 3;
[eapply wf_exp_eq_app_cong' |].
-- specialize (H12 _ {{{σ ∘ σ0}}} _ ltac:(mauto 3) ltac:(eassumption)).
rewrite wf_exp_eq_sub_compose with (M := M) in H12; mauto 3.
bulky_rewrite_in H12.
-- rewrite <- @exp_eq_sub_compose_typ; mauto 3.
-- econstructor; mauto 3.
autorewrite with mcltt.
rewrite <- @exp_eq_sub_compose_typ; mauto 3.
- handle_functional_glu_univ_elem.
handle_per_univ_elem_irrel.
pose proof H8.
invert_per_univ_elem H8.
econstructor; mauto 3.
+ invert_glu_rel1. trivial.
+ eapply glu_univ_elem_trm_typ; eauto.
+ intros.
saturate_weakening_escape.
invert_glu_rel1. clear_dups.
progressive_invert H20.
assert {{ Γ ⊢w Id : Γ }} by mauto 4.
pose proof (H10 _ _ H24).
specialize (H10 _ _ H19).
assert {{ Γ ⊢ IT[Id] ≈ IT : Type@i }} by mauto 3.
bulky_rewrite_in H25.
destruct (H11 _ _ _ ltac:(eassumption) ltac:(eassumption)) as [].
specialize (H29 _ _ _ H19 H9).
rewrite H5 in *.
autorewrite with mcltt.
eassert {{ Δ ⊢ M[σ] : ~_ }} by (mauto 2).
autorewrite with mcltt in H30.
rewrite @wf_exp_eq_pi_eta' with (M := {{{ M[σ] }}}); [| trivial].
cbn [nf_to_exp].
eapply wf_exp_eq_fn_cong'; eauto.
pose proof (var_per_elem (length Δ) H0).
destruct_rel_mod_eval.
simplify_evals.
destruct (H2 _ ltac:(eassumption) _ ltac:(eassumption)) as [? []].
specialize (H12 _ _ _ _ ltac:(trivial) (var_glu_elem_bot _ _ _ _ _ _ H H10)).
autorewrite with mcltt in H12.
specialize (H14 {{{Δ, IT[σ]}}} {{{σ ∘ Wk}}} _ _ ltac:(mauto) ltac:(eassumption) ltac:(eassumption)) as [? []].
apply_equiv_left.
destruct_rel_mod_app.
simplify_evals.
deepexec H1 ltac:(fun H => pose proof H).
specialize (H33 _ _ _ _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption) ltac:(eassumption)) as [].
specialize (H40 _ {{{Id}}} _ ltac:(mauto 3) ltac:(eassumption)).
do 2 (rewrite wf_exp_eq_sub_id in H40; mauto 3).
etransitivity; [|eassumption].
simpl.
assert {{ Δ, IT[σ] ⊢ #0 : IT[σ∘Wk] }} by (rewrite <- @exp_eq_sub_compose_typ; mauto 3).
rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
rewrite <- @exp_eq_sub_compose_typ; mauto 2.
2:eapply sub_q; mauto 4.
2:gen_presup H41; econstructor; mauto 3.
eapply wf_exp_eq_app_cong'; [| mauto 3].
symmetry.
rewrite <- wf_exp_eq_pi_sub; mauto 4.
- econstructor; eauto.
intros.
progressive_inversion.
firstorder.
- handle_functional_glu_univ_elem.
apply_equiv_left.
econstructor; eauto.
- handle_functional_glu_univ_elem.
invert_glu_rel1.
econstructor; eauto.
+ intros s. destruct (H3 s) as [? []].
mauto.
+ intros.
progressive_inversion.
specialize (H11 (length Δ)) as [? []].
firstorder.
Qed.
Corollary realize_glu_typ_top : forall a i P El,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
forall Γ A,
{{ Γ ⊢ A ® P }} ->
{{ Γ ⊢ A ® glu_typ_top i a }}.
Proof.
intros.
pose proof H.
eapply glu_univ_elem_per_univ in H.
simpl in *. destruct_all.
eapply realize_glu_univ_elem_gen; eauto.
Qed.
Theorem realize_glu_elem_bot : forall a i P El,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
forall Γ A M m,
{{ Γ ⊢ M : A ® m ∈ glu_elem_bot i a }} ->
{{ Γ ⊢ M : A ® ⇑ a m ∈ El }}.
Proof.
intros.
eapply realize_glu_univ_elem_gen; eauto.
Qed.
Theorem realize_glu_elem_top : forall a i P El,
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
forall Γ A M m,
{{ Γ ⊢ M : A ® m ∈ El }} ->
{{ Γ ⊢ M : A ® m ∈ glu_elem_top i a }}.
Proof.
intros.
pose proof H.
eapply glu_univ_elem_per_univ in H.
simpl in *. destruct_all.
eapply realize_glu_univ_elem_gen; eauto.
eapply glu_univ_elem_per_elem; eauto.
Qed.
#[export]
Hint Resolve realize_glu_typ_top realize_glu_elem_top : mcltt.
Corollary var0_glu_elem : forall {i a P El Γ A},
{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
{{ Γ ⊢ A ® P }} ->
{{ Γ, A ⊢ #0 : A[Wk] ® ⇑! a (length Γ) ∈ El }}.
Proof.
intros.
eapply realize_glu_elem_bot; mauto 4.
eauto using var_glu_elem_bot.
Qed.