Mcltt.Core.Completeness.TermStructureCases
From Coq Require Import Morphisms_Relations RelationClasses.
From Mcltt Require Import Base LibTactics.
From Mcltt.Core.Completeness Require Import LogicalRelation UniverseCases.
Import Domain_Notations.
Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},
{{ Δ ⊨ M ≈ M' : A }} ->
{{ Γ ⊨s σ ≈ σ' : Δ }} ->
{{ Γ ⊨ M[σ] ≈ M'[σ'] : A[σ] }}.
Proof with mautosolve.
intros * [env_relΔ] [env_relΓ].
destruct_conjs.
pose env_relΔ.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
assert (env_relΓ ρ' ρ) by (symmetry; eassumption).
assert (env_relΓ ρ ρ) by (etransitivity; eassumption).
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
handle_per_univ_elem_irrel.
match goal with
| _: {{ ⟦ σ ⟧s ρ ↘ ~?ρ0 }},
_: {{ ⟦ σ ⟧s ρ' ↘ ~?ρ'0 }} |- _ =>
rename ρ0 into ρσ;
rename ρ'0 into ρ'σ
end.
assert (env_relΔ ρσ ρ'σ) by (etransitivity; [|symmetry; eassumption]; eassumption).
(on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split...
Qed.
#[export]
Hint Resolve rel_exp_sub_cong : mcltt.
Lemma rel_exp_sub_id : forall {Γ M A},
{{ Γ ⊨ M : A }} ->
{{ Γ ⊨ M[Id] ≈ M : A }}.
Proof with mautosolve.
intros * [env_relΓ].
destruct_conjs.
eexists_rel_exp.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
eexists.
split...
Qed.
#[export]
Hint Resolve rel_exp_sub_id : mcltt.
Lemma rel_exp_sub_compose : forall {Γ τ Γ' σ Γ'' M A},
{{ Γ ⊨s τ : Γ' }} ->
{{ Γ' ⊨s σ : Γ'' }} ->
{{ Γ'' ⊨ M : A }} ->
{{ Γ ⊨ M[σ ∘ τ] ≈ M[σ][τ] : A[σ ∘ τ] }}.
Proof with mautosolve.
intros * [env_relΓ [? [env_relΓ']]] [? [? [env_relΓ'']]] [].
destruct_conjs.
pose env_relΓ'.
pose env_relΓ''.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
assert (env_relΓ ρ' ρ) by (symmetry; eassumption).
assert (env_relΓ ρ ρ) by (etransitivity; eassumption).
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
handle_per_univ_elem_irrel.
(on_all_hyp: destruct_rel_by_assumption env_relΓ').
handle_per_univ_elem_irrel.
(on_all_hyp: destruct_rel_by_assumption env_relΓ'').
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split; econstructor...
Qed.
#[export]
Hint Resolve rel_exp_sub_compose : mcltt.
Lemma rel_exp_conv : forall {Γ M M' A A' i},
{{ Γ ⊨ M ≈ M' : A }} ->
{{ Γ ⊨ A ≈ A' : Type@i }} ->
{{ Γ ⊨ M ≈ M' : A' }}.
Proof with mautosolve.
intros * [env_relΓ] []%rel_exp_of_typ_inversion.
destruct_conjs.
pose env_relΓ.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
assert (env_relΓ ρ ρ) by (etransitivity; [| symmetry]; eassumption).
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head per_univ.
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split; econstructor; mauto.
etransitivity; [symmetry |]...
Qed.
#[export]
Hint Resolve rel_exp_conv : mcltt.
Lemma rel_exp_sym : forall {Γ M M' A},
{{ Γ ⊨ M ≈ M' : A }} ->
{{ Γ ⊨ M' ≈ M : A }}.
Proof with mautosolve.
intros * [env_relΓ].
destruct_conjs.
eexists_rel_exp.
intros.
assert (env_relΓ ρ' ρ) by (symmetry; eauto).
(on_all_hyp: destruct_rel_by_assumption env_relΓ); destruct_conjs.
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split; econstructor; mauto.
symmetry...
Qed.
#[export]
Hint Resolve rel_exp_sym : mcltt.
Lemma rel_exp_trans : forall {Γ M1 M2 M3 A},
{{ Γ ⊨ M1 ≈ M2 : A }} ->
{{ Γ ⊨ M2 ≈ M3 : A }} ->
{{ Γ ⊨ M1 ≈ M3 : A }}.
Proof with mautosolve.
intros * [env_relΓ] [].
destruct_conjs.
pose env_relΓ.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
assert (env_relΓ ρ' ρ) by (symmetry; eauto).
assert (env_relΓ ρ' ρ') by (etransitivity; eauto).
(on_all_hyp: destruct_rel_by_assumption env_relΓ); destruct_conjs.
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split; econstructor; mauto.
etransitivity...
Qed.
#[export]
Hint Resolve rel_exp_trans : mcltt.
#[export]
Instance rel_exp_PER {Γ A} : PER (rel_exp_under_ctx Γ A).
Proof.
split; mauto.
Qed.
Lemma presup_rel_exp : forall {Γ M M' A},
{{ Γ ⊨ M ≈ M' : A }} ->
{{ ⊨ Γ }} /\ {{ Γ ⊨ M : A }} /\ {{ Γ ⊨ M' : A }} /\ exists i, {{ Γ ⊨ A : Type@i }}.
Proof.
intros *.
assert (Hpart : {{ Γ ⊨ M ≈ M' : A }} -> {{ Γ ⊨ M : A }} /\ {{ Γ ⊨ M' : A }})
by (split; unfold valid_exp_under_ctx; etransitivity; [|symmetry|symmetry|]; eassumption).
intros Hrel; repeat split;
try solve [intuition]; clear Hpart;
destruct Hrel as [env_relΓ];
destruct_conjs.
- eexists; eassumption.
- destruct_by_head valid_exp_under_ctx.
destruct_conjs.
eexists.
eexists_rel_exp_of_typ.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
eapply rel_typ_implies_rel_exp; eauto.
Qed.
Lemma rel_exp_eq_subtyp : forall Γ M M' A A',
{{ Γ ⊨ M ≈ M' : A }} ->
{{ Γ ⊨ A ⊆ A' }} ->
{{ Γ ⊨ M ≈ M' : A' }}.
Proof.
intros * [env_relΓ [? [i]]] [? [? [j]]].
pose env_relΓ.
handle_per_ctx_env_irrel.
eexists_rel_exp_with (max i j).
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
simplify_evals.
eexists.
split; econstructor; eauto using per_univ_elem_cumu_max_right.
handle_per_univ_elem_irrel.
eapply per_elem_subtyping_gen with (i := max i j); try eassumption.
- eauto using per_subtyp_cumu_right.
- eauto using per_univ_elem_cumu_max_right.
- symmetry. eauto using per_univ_elem_cumu_max_right.
Qed.
#[export]
Hint Resolve rel_exp_eq_subtyp : mcltt.
From Mcltt Require Import Base LibTactics.
From Mcltt.Core.Completeness Require Import LogicalRelation UniverseCases.
Import Domain_Notations.
Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},
{{ Δ ⊨ M ≈ M' : A }} ->
{{ Γ ⊨s σ ≈ σ' : Δ }} ->
{{ Γ ⊨ M[σ] ≈ M'[σ'] : A[σ] }}.
Proof with mautosolve.
intros * [env_relΔ] [env_relΓ].
destruct_conjs.
pose env_relΔ.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
assert (env_relΓ ρ' ρ) by (symmetry; eassumption).
assert (env_relΓ ρ ρ) by (etransitivity; eassumption).
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
handle_per_univ_elem_irrel.
match goal with
| _: {{ ⟦ σ ⟧s ρ ↘ ~?ρ0 }},
_: {{ ⟦ σ ⟧s ρ' ↘ ~?ρ'0 }} |- _ =>
rename ρ0 into ρσ;
rename ρ'0 into ρ'σ
end.
assert (env_relΔ ρσ ρ'σ) by (etransitivity; [|symmetry; eassumption]; eassumption).
(on_all_hyp: destruct_rel_by_assumption env_relΔ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split...
Qed.
#[export]
Hint Resolve rel_exp_sub_cong : mcltt.
Lemma rel_exp_sub_id : forall {Γ M A},
{{ Γ ⊨ M : A }} ->
{{ Γ ⊨ M[Id] ≈ M : A }}.
Proof with mautosolve.
intros * [env_relΓ].
destruct_conjs.
eexists_rel_exp.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
eexists.
split...
Qed.
#[export]
Hint Resolve rel_exp_sub_id : mcltt.
Lemma rel_exp_sub_compose : forall {Γ τ Γ' σ Γ'' M A},
{{ Γ ⊨s τ : Γ' }} ->
{{ Γ' ⊨s σ : Γ'' }} ->
{{ Γ'' ⊨ M : A }} ->
{{ Γ ⊨ M[σ ∘ τ] ≈ M[σ][τ] : A[σ ∘ τ] }}.
Proof with mautosolve.
intros * [env_relΓ [? [env_relΓ']]] [? [? [env_relΓ'']]] [].
destruct_conjs.
pose env_relΓ'.
pose env_relΓ''.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
assert (env_relΓ ρ' ρ) by (symmetry; eassumption).
assert (env_relΓ ρ ρ) by (etransitivity; eassumption).
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
handle_per_univ_elem_irrel.
(on_all_hyp: destruct_rel_by_assumption env_relΓ').
handle_per_univ_elem_irrel.
(on_all_hyp: destruct_rel_by_assumption env_relΓ'').
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split; econstructor...
Qed.
#[export]
Hint Resolve rel_exp_sub_compose : mcltt.
Lemma rel_exp_conv : forall {Γ M M' A A' i},
{{ Γ ⊨ M ≈ M' : A }} ->
{{ Γ ⊨ A ≈ A' : Type@i }} ->
{{ Γ ⊨ M ≈ M' : A' }}.
Proof with mautosolve.
intros * [env_relΓ] []%rel_exp_of_typ_inversion.
destruct_conjs.
pose env_relΓ.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
assert (env_relΓ ρ ρ) by (etransitivity; [| symmetry]; eassumption).
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head per_univ.
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split; econstructor; mauto.
etransitivity; [symmetry |]...
Qed.
#[export]
Hint Resolve rel_exp_conv : mcltt.
Lemma rel_exp_sym : forall {Γ M M' A},
{{ Γ ⊨ M ≈ M' : A }} ->
{{ Γ ⊨ M' ≈ M : A }}.
Proof with mautosolve.
intros * [env_relΓ].
destruct_conjs.
eexists_rel_exp.
intros.
assert (env_relΓ ρ' ρ) by (symmetry; eauto).
(on_all_hyp: destruct_rel_by_assumption env_relΓ); destruct_conjs.
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split; econstructor; mauto.
symmetry...
Qed.
#[export]
Hint Resolve rel_exp_sym : mcltt.
Lemma rel_exp_trans : forall {Γ M1 M2 M3 A},
{{ Γ ⊨ M1 ≈ M2 : A }} ->
{{ Γ ⊨ M2 ≈ M3 : A }} ->
{{ Γ ⊨ M1 ≈ M3 : A }}.
Proof with mautosolve.
intros * [env_relΓ] [].
destruct_conjs.
pose env_relΓ.
handle_per_ctx_env_irrel.
eexists_rel_exp.
intros.
assert (env_relΓ ρ' ρ) by (symmetry; eauto).
assert (env_relΓ ρ' ρ') by (etransitivity; eauto).
(on_all_hyp: destruct_rel_by_assumption env_relΓ); destruct_conjs.
destruct_by_head rel_typ.
destruct_by_head rel_exp.
handle_per_univ_elem_irrel.
eexists.
split; econstructor; mauto.
etransitivity...
Qed.
#[export]
Hint Resolve rel_exp_trans : mcltt.
#[export]
Instance rel_exp_PER {Γ A} : PER (rel_exp_under_ctx Γ A).
Proof.
split; mauto.
Qed.
Lemma presup_rel_exp : forall {Γ M M' A},
{{ Γ ⊨ M ≈ M' : A }} ->
{{ ⊨ Γ }} /\ {{ Γ ⊨ M : A }} /\ {{ Γ ⊨ M' : A }} /\ exists i, {{ Γ ⊨ A : Type@i }}.
Proof.
intros *.
assert (Hpart : {{ Γ ⊨ M ≈ M' : A }} -> {{ Γ ⊨ M : A }} /\ {{ Γ ⊨ M' : A }})
by (split; unfold valid_exp_under_ctx; etransitivity; [|symmetry|symmetry|]; eassumption).
intros Hrel; repeat split;
try solve [intuition]; clear Hpart;
destruct Hrel as [env_relΓ];
destruct_conjs.
- eexists; eassumption.
- destruct_by_head valid_exp_under_ctx.
destruct_conjs.
eexists.
eexists_rel_exp_of_typ.
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
eapply rel_typ_implies_rel_exp; eauto.
Qed.
Lemma rel_exp_eq_subtyp : forall Γ M M' A A',
{{ Γ ⊨ M ≈ M' : A }} ->
{{ Γ ⊨ A ⊆ A' }} ->
{{ Γ ⊨ M ≈ M' : A' }}.
Proof.
intros * [env_relΓ [? [i]]] [? [? [j]]].
pose env_relΓ.
handle_per_ctx_env_irrel.
eexists_rel_exp_with (max i j).
intros.
(on_all_hyp: destruct_rel_by_assumption env_relΓ).
destruct_by_head rel_typ.
destruct_by_head rel_exp.
simplify_evals.
eexists.
split; econstructor; eauto using per_univ_elem_cumu_max_right.
handle_per_univ_elem_irrel.
eapply per_elem_subtyping_gen with (i := max i j); try eassumption.
- eauto using per_subtyp_cumu_right.
- eauto using per_univ_elem_cumu_max_right.
- symmetry. eauto using per_univ_elem_cumu_max_right.
Qed.
#[export]
Hint Resolve rel_exp_eq_subtyp : mcltt.