finished semantic well-formedness of equality type (#271)

* finished semantic well-formedness of equality type * Closes #272 * proved semantic rule for refl * minor improvement * improve one automation * typo * more tactic setups * to export * revert * Revert "revert" This reverts commit a55fc67. * revert
Beluga-lang · Dec 19, 2024 · 0507289 · 0507289
1 parent 03d5f3b
commit 0507289
Show file tree

Hide file tree

Showing 8 changed files with 249 additions and 40 deletions.
diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
@@ -18,17 +18,76 @@ Lemma glu_rel_eq : forall Γ A i M N,
     {{ Γ ⊩ N : A }} ->
     {{ Γ ⊩ Eq A M N : Type@i }}.
 Proof.
-Admitted.
+  intros * HA HM HN.
+  assert {{ ⊩ Γ }} as [SbΓ] by mauto.
+  saturate_syn_judge.
+  invert_sem_judge.
+
+  eapply glu_rel_exp_of_typ; mauto 3.
+  intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  split; mauto 3.
+  apply_glu_rel_judge.
+  saturate_glu_typ_from_el.
+  unify_glu_univ_lvl i.
+  deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
+  match_by_head per_univ ltac:(fun H => destruct H).
+  do 2 deepexec glu_univ_elem_per_elem ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
+
+  eexists; repeat split; mauto.
+  - eexists. per_univ_elem_econstructor; mauto. reflexivity.
+  - intros.
+    match_by_head1 glu_univ_elem invert_glu_univ_elem.
+    handle_per_univ_elem_irrel.
+    handle_functional_glu_univ_elem.
+    econstructor; mauto 3;
+      intros Δ' τ **;
+      assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
+      assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
+      assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
+      apply_glu_rel_judge;
+      handle_functional_glu_univ_elem;
+      unify_glu_univ_lvl i.
+    + bulky_rewrite.
+    + assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto.
+      bulky_rewrite.
+    + assert {{ Δ' ⊢ N[σ][τ] ≈ N[σ ∘ τ] : A[σ ∘ τ] }} by mauto.
+      bulky_rewrite.
+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.
+  saturate_syn_judge.
+  invert_sem_judge.
+  assert {{ Γ ⊢ A : Type@x }} by mauto.
+  eexists; split; eauto.
+  exists x; intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  apply_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;
+    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;
+    apply_glu_rel_judge;
+    saturate_glu_typ_from_el;
+    bulky_rewrite.
+Qed.
 
 #[export]
   Hint Resolve glu_rel_eq_refl : mctt.

diff --git a/theories/Core/Soundness/FunctionCases.v b/theories/Core/Soundness/FunctionCases.v
@@ -47,12 +47,7 @@ Proof.
   intros.
   assert {{ Δ ⊢s σ : Γ }} by mauto 4.
   split; mauto 3.
-  destruct_glu_rel_exp_with_sub.
-  simplify_evals.
-  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H).
-  handle_functional_glu_univ_elem.
-  unfold univ_glu_exp_pred' in *.
-  destruct_conjs.
+  apply_glu_rel_judge.
   rename m into a.
   assert {{ Γ ⊨ Π A B : Type@i }} as [env_relΓ]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.
   assert {{ Γ, A ⊨ B : Type@i }} as [env_relΓA]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.

diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -415,6 +415,12 @@ Variant glu_rel_sub_with_sub Δ τ (Sb : glu_sub_pred) σ ρ : Prop :=
 Definition glu_rel_ctx Γ : Prop := exists Sb, {{ EG Γ ∈ glu_ctx_env ↘ Sb }}.
 Arguments glu_rel_ctx Γ/.
 
+Definition glu_rel_exp_resp_sub_env i Sb M A :=
+  forall Δ σ ρ,
+    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
+    glu_rel_exp_with_sub i Δ M A σ ρ.
+Arguments glu_rel_exp_resp_sub_env i Sb M A/.
+
 Definition glu_rel_exp Γ M A : Prop :=
   exists Sb,
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} /\
@@ -424,6 +430,13 @@ Definition glu_rel_exp Γ M A : Prop :=
         glu_rel_exp_with_sub i Δ M A σ ρ.
 Arguments glu_rel_exp Γ M A/.
 
+
+Definition glu_rel_sub_resp_sub_env Sb Sb' τ :=
+  forall Δ σ ρ,
+    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
+    glu_rel_sub_with_sub Δ τ Sb' σ ρ.
+Arguments glu_rel_sub_resp_sub_env Sb Sb' τ/.
+
 Definition glu_rel_sub Γ τ Γ' : Prop :=
   exists Sb Sb',
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} /\

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -464,6 +464,19 @@ Proof.
   eapply glu_univ_elem_exp_lower_max_left; mauto.
 Qed.
 
+Lemma glu_univ_elem_exp_conv' : forall {i j a P P' El El' Γ A M m},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Γ ⊢ A ® P' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El' }}.
+Proof.
+  intros.
+  eapply glu_univ_elem_exp_conv; only 2: exact H; eauto.
+  mauto 2.
+Qed.
+
+
 Lemma glu_univ_elem_per_subtyp_typ_escape : forall {i a a' P P' El El' Γ A A'},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -1144,29 +1157,32 @@ Ltac destruct_glu_rel_by_assumption sub_glu_rel H :=
         mark_with H' 1
     end;
   unmark_all_with 1.
+
 Ltac destruct_glu_rel_exp_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_exp_with_sub _ _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
   unmark_all.
+
 Ltac destruct_glu_rel_sub_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_sub_with_sub _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
   unmark_all.
+
 Ltac destruct_glu_rel_typ_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_typ_with_sub _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
@@ -1189,18 +1205,13 @@ Proof.
   mauto.
 Qed.
 
-Definition glu_rel_exp_clean_inversion2_result i Sb M A :=
-  forall Δ σ ρ,
-    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
-    glu_rel_exp_with_sub i Δ M A σ ρ.
-
 Lemma glu_rel_exp_clean_inversion2 : forall {i Γ Sb M A},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ A : Type@i }} ->
     {{ Γ ⊩ M : A }} ->
-    glu_rel_exp_clean_inversion2_result i Sb M A.
+    glu_rel_exp_resp_sub_env i Sb M A.
 Proof.
-  unfold glu_rel_exp_clean_inversion2_result.
+  simpl.
   intros * ? HA HM.
   eapply glu_rel_exp_clean_inversion1 in HA; [| eassumption].
   eapply glu_rel_exp_clean_inversion1 in HM; [| eassumption].
@@ -1216,12 +1227,14 @@ Proof.
   eapply glu_univ_elem_exp_conv; revgoals; mauto 3.
 Qed.
 
+#[global]
 Ltac invert_glu_rel_exp H :=
   (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-   unfold glu_rel_exp_clean_inversion2_result in H)
+   simpl in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [])
-  + (inversion H; subst).
+  + (inversion H as [? [? [? ?]]]; subst).
+
 
 Lemma glu_rel_exp_to_wf_exp : forall {Γ A M},
     {{ Γ ⊩ M : A }} ->
@@ -1279,9 +1292,9 @@ Lemma glu_rel_sub_clean_inversion3 : forall {Γ Sb τ Γ' Sb'},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ EG Γ' ∈ glu_ctx_env ↘ Sb' }} ->
     {{ Γ ⊩s τ : Γ' }} ->
-    forall (Δ : ctx) (σ : sub) (ρ : env), Sb Δ σ ρ -> glu_rel_sub_with_sub Δ τ Sb' σ ρ.
+    glu_rel_sub_resp_sub_env Sb Sb' τ.
 Proof.
-  intros * ? ? Hglu.
+  simpl. intros * ? ? Hglu.
   eapply glu_rel_sub_clean_inversion2 in Hglu; [| eassumption].
   destruct_conjs.
   handle_functional_glu_ctx_env.
@@ -1315,3 +1328,87 @@ Qed.
 
 #[export]
 Hint Resolve glu_rel_sub_wf_sub : mctt.
+
+
+Ltac saturate_glu_typ_from_el1 :=
+  match goal with
+  | H : glu_univ_elem _ _ ?El _, H1 : ?El _ _ _ _ |- _ =>
+      pose proof (glu_univ_elem_trm_typ _ _ _ _ H _ _ _ _ H1);
+      fail_if_dup
+  end.
+
+Ltac saturate_glu_typ_from_el :=
+  fail_if_dup;
+  repeat saturate_glu_typ_from_el1.
+
+Ltac unify_glu_univ_lvl1 i :=
+  match goal with
+  | H1 : glu_univ_elem _ _ ?El _, H2 : glu_univ_elem i ?P _ _, H3 : ?P _ _, H4 : ?El _ _ _ _
+    |- _ =>
+      pose proof (glu_univ_elem_exp_conv' H1 H2 H4 H3);
+      fail_if_dup
+  end.
+
+Ltac unify_glu_univ_lvl i :=
+  fail_if_dup;
+  repeat unify_glu_univ_lvl1 i.
+
+Ltac apply_glu_rel_judge :=
+  destruct_glu_rel_typ_with_sub;
+  destruct_glu_rel_exp_with_sub;
+  destruct_glu_rel_sub_with_sub;
+  simplify_evals;
+  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H);
+  handle_functional_glu_univ_elem;
+  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.
+
+
+
+Ltac saturate_syn_judge1 :=
+  match goal with
+  | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
+      assert {{ Γ ⊢ M : A }} by mauto; fail_if_dup
+  | H : {{ ^?Γ ⊩s ^?τ : ^?Γ' }} |- _ =>
+      assert {{ Γ ⊢s τ : Γ' }} by mauto; fail_if_dup
+  end.
+
+#[global]
+  Ltac saturate_syn_judge :=
+  repeat saturate_syn_judge1.
+
+Ltac invert_sem_judge1 :=
+  match goal with
+  | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
+      invert_glu_rel_exp H
+  | H : {{ ^?Γ ⊩s ^?τ : ^?Γ' }} |- _ =>
+      invert_glu_rel_sub H
+  end.
+
+#[global]
+  Ltac invert_sem_judge :=
+  repeat invert_sem_judge1.
diff --git a/theories/Core/Soundness/NatCases.v b/theories/Core/Soundness/NatCases.v
@@ -51,7 +51,7 @@ Hint Resolve glu_rel_exp_sub_nat : mctt.
 Lemma glu_rel_exp_clean_inversion2'' : forall {Γ Sb M},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ M : ℕ }} ->
-    glu_rel_exp_clean_inversion2_result 0 Sb M {{{ ℕ }}}.
+    glu_rel_exp_resp_sub_env 0 Sb M {{{ ℕ }}}.
 Proof.
   intros * ? HM.
   assert {{ Γ ⊩ ℕ : Type@0 }} by mauto 3.
@@ -60,11 +60,11 @@ Qed.
 
 Ltac invert_glu_rel_exp H ::=
   (unshelve eapply (glu_rel_exp_clean_inversion2'' _) in H; shelve_unifiable; [eassumption |];
-   unfold glu_rel_exp_clean_inversion2_result in H)
+   unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
-     unfold glu_rel_exp_clean_inversion2_result in H)
+     unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-     unfold glu_rel_exp_clean_inversion2_result in H)
+     unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [])
   + (inversion H; subst).