From 8081b69cd7c9ac18f1b62ef12c632af339a2462c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Jul 2022 13:50:52 -0400
Subject: [PATCH] stronger fixpoint unfolding lemmas

---
 theories/typing/examples/fixpoint.v |  7 +++++++
 theories/typing/fixpoint.v          | 15 +++++++--------
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/theories/typing/examples/fixpoint.v b/theories/typing/examples/fixpoint.v
index 17b674c4..e7f8f37c 100644
--- a/theories/typing/examples/fixpoint.v
+++ b/theories/typing/examples/fixpoint.v
@@ -17,4 +17,11 @@ Section fixpoint.
   Qed.
 
   Definition my_list := type_fixpoint my_list_pre.
+
+  Local Lemma my_list_unfold :
+    my_list ≡ my_list_pre my_list.
+  Proof. apply type_fixpoint_unfold. Qed.
+
+  Lemma my_list_size : my_list.(ty_size) = 2%nat.
+  Proof. rewrite my_list_unfold. done. Qed.
 End fixpoint.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 4a151e02..a8df5832 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -46,7 +46,7 @@ Section fixpoint.
   Context `{!typeGS Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
-  Global Instance fixpoint_copy :
+  Global Instance type_fixpoint_copy :
     (∀ `(!Copy ty), Copy (T ty)) → Copy (type_fixpoint T).
   Proof.
     intros ?. unfold type_fixpoint. apply fixpointK_ind.
@@ -65,7 +65,7 @@ Section fixpoint.
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 
-  Global Instance fixpoint_send :
+  Global Instance type_fixpoint_send :
     (∀ `(!Send ty), Send (T ty)) → Send (type_fixpoint T).
   Proof.
     intros ?. unfold type_fixpoint. apply fixpointK_ind.
@@ -77,7 +77,7 @@ Section fixpoint.
       apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
-  Global Instance fixpoint_sync :
+  Global Instance type_fixpoint_sync :
     (∀ `(!Sync ty), Sync (T ty)) → Sync (type_fixpoint T).
   Proof.
     intros ?. unfold type_fixpoint. apply fixpointK_ind.
@@ -89,12 +89,11 @@ Section fixpoint.
       apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
+  Lemma type_fixpoint_unfold : type_fixpoint T ≡ T (type_fixpoint T).
+  Proof. apply fixpointK_unfold. by apply type_contractive_ne. Qed.
+
   Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
-  Proof.
-    unfold eqtype, subtype, type_incl.
-    setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
-    split; iIntros (qmax qL) "_ !> _"; (iSplit; first done); iSplit; iIntros "!>*$".
-  Qed.
+  Proof. apply type_equal_eqtype, type_equal_equiv, type_fixpoint_unfold. Qed.
 End fixpoint.
 
 Section subtyping.
-- 
GitLab