Amber rule for subtyping of rec. types.

theories/logrel/examples/rec_subtyping.v

@@ -44,7 +44,7 @@ Section basics.
       iApply (lty_le_trans with "H1").
       iIntros (X' Y'). iExists X', Y'. iIntros "!>!>!>".
       iApply "IH". }
-    iApply lty_le_rec.
+    iApply lty_le_rec_internal.
     iIntros (S1 S2) "#Hrec".
     iIntros (X). iExists X, lty_bool. iIntros "!> !>" (Y).
     iApply (lty_le_trans _ (<??> TY lty_bool; <!!> TY Y ⊸ lty_int;

theories/logrel/subtyping_rules.v

@@ -41,8 +41,8 @@ Section subtyping_rules.
     - rewrite {2}/lty_rec fixpoint_unfold. iApply lty_le_refl.
   Qed.
 
-  Lemma lty_le_rec {k} (C1 C2 : lty Σ k → lty Σ k)
-        `{Contractive C1, Contractive C2} :
+  Lemma lty_le_rec_internal {k} (C1 C2 : lty Σ k → lty Σ k)
+      `{Contractive C1, Contractive C2} :
     (∀ K1 K2, ▷ (K1 <: K2) -∗ C1 K1 <: C2 K2) -∗
     lty_rec C1 <: lty_rec C2.
   Proof.
@@ -51,6 +51,17 @@ Section subtyping_rules.
     iApply lty_le_r; [|iApply lty_bi_le_sym; iApply lty_le_rec_unfold].
     by iApply "Hle".
   Qed.
+  Lemma lty_le_rec_external {k} (C1 C2 : lty Σ k → lty Σ k)
+      `{Contractive C1, Contractive C2} :
+    (∀ K1 K2, (K1 <: K2) → C1 K1 <: C2 K2) →
+    lty_rec C1 <: lty_rec C2.
+  Proof.
+    intros IH. rewrite /lty_rec. apply fixpoint_ind.
+    - by intros K1' K2' -> ?.
+    - exists (fixpoint C2). iApply lty_le_refl.
+    - intros K' ?. rewrite (fixpoint_unfold C2). by apply IH.
+    - apply bi.limit_preserving_entails; [done|solve_proper].
+  Qed.
 
   (** Term subtyping *)
   Lemma lty_le_any A : A <: any.