Revert "remove contra-variant subtyping (#127)"

This reverts commit cfe379e.
Beluga-lang · Jun 27, 2024 · 0a2770e · 0a2770e
1 parent cfe379e
commit 0a2770e
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 21 deletions.
diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
@@ -309,10 +309,10 @@ with wf_subtyping : ctx -> typ -> typ -> Prop :=
      {{ Γ ⊢ Type@i ⊆ Type@j }} )
 | wf_subtyp_pi :
   `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ A' : Type@i }} ->
-     {{ Γ ⊢ A ≈ A' : Type@i }} ->
      {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ A' : Type@i }} ->
      {{ Γ , A' ⊢ B' : Type@i }} ->
+     {{ Γ ⊢ A' ⊆ A }} ->
      {{ Γ , A' ⊢ B ⊆ B' }} ->
      {{ Γ ⊢ Π A B ⊆ Π A' B' }} )
 where "Γ ⊢ A ⊆ A'" := (wf_subtyping Γ A A') (in custom judg) : type_scope.

diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
@@ -818,7 +818,7 @@ Proof.
   induction 1; intros; mauto 4.
   - transitivity {{{ Type@i}}}; [mauto |].
     transitivity {{{ Type@j}}}; [| mauto].
-    mauto 3.
+    mauto.
   - transitivity {{{ Π (A[σ]) (B [ q σ ]) }}}; [ mauto |].
     transitivity {{{ Π (A'[σ]) (B' [ q σ ]) }}}; [ | mauto].
     eapply wf_subtyp_pi with (i := i); mauto 4.

diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v
@@ -267,21 +267,3 @@ Qed.
 Hint Resolve wf_exp_eq_pi_eta' : mcltt.
 #[export]
 Remove Hints wf_exp_eq_pi_eta : mcltt.
-
-
-Lemma wf_subtyp_pi' : forall Γ A A' B B' i,
-    {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ Γ , A' ⊢ B ⊆ B' }} ->
-    {{ Γ ⊢ Π A B ⊆ Π A' B' }}.
-Proof.
-  intros. gen_presups.
-  eapply wf_subtyp_pi with (i := max i i0);
-    mauto 3 using lift_exp_max_left, lift_exp_max_right, lift_exp_eq_max_left.
-  eapply ctxeq_exp; [ | mauto 3 using lift_exp_max_right].
-  mauto 4.
-Qed.
-
-#[export]
-Hint Resolve wf_subtyp_pi' : mcltt.
-#[export]
-Remove Hints wf_subtyp_pi : mcltt.