Skip to content

Commit

Permalink
proved semantic rule for refl
Browse files Browse the repository at this point in the history
  • Loading branch information
HuStmpHrrr committed Dec 15, 2024
1 parent 0243510 commit c049895
Show file tree
Hide file tree
Showing 2 changed files with 51 additions and 3 deletions.
30 changes: 27 additions & 3 deletions theories/Core/Soundness/EqualityCases.v
Original file line number Diff line number Diff line change
Expand Up @@ -62,12 +62,36 @@ Qed.
#[export]
Hint Resolve glu_rel_eq : mctt.

Lemma glu_rel_eq_refl : forall Γ A i M,
{{ Γ ⊩ A : Type@i }} ->
Lemma glu_rel_eq_refl : forall Γ A M,
{{ Γ ⊩ M : A }} ->
{{ Γ ⊩ refl A M : Eq A M M }}.
Proof.
Admitted.
intros * HM.
assert {{ ⊩ Γ }} as [SbΓ] by mauto.
assert {{ Γ ⊢ M : A }} by mauto.
invert_glu_rel_exp HM.
assert {{ Γ ⊢ A : Type@x }} by mauto.
eexists; split; eauto.
exists x; intros.
assert {{ Δ ⊢s σ : Γ }} by mauto 4.
applying_glu_rel_judge.
saturate_glu_typ_from_el.
deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
match_by_head per_univ ltac:(fun H => destruct H).
deepexec glu_univ_elem_per_elem ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
saturate_glu_info.
eexists; repeat split; mauto.
- glu_univ_elem_econstructor; mauto 3; reflexivity.
- do 2 try econstructor; mauto 3;
try (intros Δ' τ **;
assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto;
applying_glu_rel_judge;
saturate_glu_typ_from_el;
bulky_rewrite).
Qed.

#[export]
Hint Resolve glu_rel_eq_refl : mctt.
Expand Down
24 changes: 24 additions & 0 deletions theories/Core/Soundness/LogicalRelation/Lemmas.v
Original file line number Diff line number Diff line change
Expand Up @@ -1234,6 +1234,7 @@ Ltac invert_glu_rel_exp H :=
destruct H as [])
+ (inversion H; subst).


Lemma glu_rel_exp_to_wf_exp : forall {Γ A M},
{{ Γ ⊩ M : A }} ->
{{ Γ ⊢ M : A }}.
Expand Down Expand Up @@ -1360,3 +1361,26 @@ Ltac applying_glu_rel_judge :=
unfold univ_glu_exp_pred' in *;
destruct_conjs;
clear_dups.


Lemma glu_rel_exp_preserves_lvl : forall Γ Sb M A i,
{{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
(forall Δ σ ρ,
{{ Δ ⊢s σ ® ρ ∈ Sb }} ->
glu_rel_exp_with_sub i Δ M A σ ρ) ->
{{ Γ ⊢ A : Type@i }}.
Proof.
intros.
assert (exists env_relΓ, {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_relΓ }}) as [env_relΓ] by mauto 3.
assert (exists ρ ρ', initial_env Γ ρ /\ initial_env Γ ρ' /\ {{ Dom ρ ≈ ρ' ∈ env_relΓ }}) as [ρ] by mauto 3 using per_ctx_then_per_env_initial_env.
destruct_conjs.
functional_initial_env_rewrite_clear.
assert {{ Γ ⊢s Id ® ρ ∈ Sb }} by (eapply initial_env_glu_rel_exp; mauto 3).
destruct_glu_rel_exp_with_sub.
saturate_glu_typ_from_el.
saturate_glu_info.
mauto 3.
Qed.

#[export]
Hint Resolve glu_rel_exp_preserves_lvl : mctt.

0 comments on commit c049895

Please sign in to comment.