Closes #272

Beluga-lang · Dec 15, 2024 · 0243510 · 0243510
1 parent 6b95ab2
commit 0243510
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 15 deletions.
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 }} /\

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1205,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].
@@ -1234,7 +1229,7 @@ Qed.
 
 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).

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).

diff --git a/theories/Core/Soundness/UniverseCases.v b/theories/Core/Soundness/UniverseCases.v
@@ -46,7 +46,7 @@ Hint Resolve glu_rel_exp_typ : mctt.
 Lemma glu_rel_exp_clean_inversion2' : forall {i Γ Sb M},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ M : Type@i }} ->
-    glu_rel_exp_clean_inversion2_result (S i) Sb M {{{ Type@i }}}.
+    glu_rel_exp_resp_sub_env (S i) Sb M {{{ Type@i }}}.
 Proof.
   intros * ? HM.
   assert {{ Γ ⊩ Type@i : Type@(S i) }} by mauto 3.
@@ -55,9 +55,9 @@ 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)
+   simpl in 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).