From 77c14c80e30d09a50861da38bfbe6931c5eac5b2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Mar 2016 15:43:50 +0100
Subject: [PATCH] Seal off definition of Banach's fixpoint.

---
 algebra/cofe.v                 | 12 ++++++++----
 program_logic/weakestpre_fix.v |  8 +++-----
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index 14941ef14..dfd10fcbd 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -174,20 +174,25 @@ Next Obligation.
   - apply (contractive_0 f).
   - apply (contractive_S f), IH; auto with omega.
 Qed.
-Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
+
+Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A → A)
   `{!Contractive f} : A := compl (fixpoint_chain f).
+Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed.
+Definition fixpoint {A AiH} f {Hf} := proj1_sig fixpoint_aux A AiH f Hf.
+Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
 
 Section fixpoint.
   Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
   Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
   Proof.
-    apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //.
+    apply equiv_dist=>n.
+    rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
     induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
   Qed.
   Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
     (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
   Proof.
-    intros Hfg. rewrite /fixpoint
+    intros Hfg. rewrite fixpoint_eq /fixpoint_def
       (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
     induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
     rewrite Hfg; apply contractive_S, IH; auto using dist_S.
@@ -196,7 +201,6 @@ Section fixpoint.
     (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g.
   Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
 End fixpoint.
-Global Opaque fixpoint.
 
 (** Function space *)
 Record cofeMor (A B : cofeT) : Type := CofeMor {
diff --git a/program_logic/weakestpre_fix.v b/program_logic/weakestpre_fix.v
index f6f623ccf..d662d6621 100644
--- a/program_logic/weakestpre_fix.v
+++ b/program_logic/weakestpre_fix.v
@@ -117,8 +117,7 @@ Section def.
   Definition wp_fix : coPsetC -n> exprC -n> (valC -n> iProp) -n> iProp := 
     fixpoint pre_wp_mor.
 
-  Lemma wp_fix_unfold E e Φ :
-    pre_wp_mor wp_fix E e Φ ⊣⊢ wp_fix E e Φ.
+  Lemma wp_fix_unfold E e Φ : pre_wp_mor wp_fix E e Φ ⊣⊢ wp_fix E e Φ.
   Proof. rewrite -fixpoint_unfold. done. Qed.
 
   Lemma wp_fix_sound (E : coPset) (e : expr Λ) (Φ : val Λ -> iProp)
@@ -131,6 +130,7 @@ Section def.
     case EQ: (to_val e)=>[v|].
     - rewrite -(of_to_val _ _ EQ) {IH}. constructor. rewrite pvs_eq.
       intros rf k Ef σ ???. destruct k; first (exfalso; omega).
+      apply wp_fix_unfold in Hwp; last done.
       edestruct (Hwp rf k Ef σ); eauto with omega; set_solver.
     - constructor; first done. intros ???? Hk ??.
       apply wp_fix_unfold in Hwp; last done.
@@ -152,8 +152,7 @@ Section def.
     split. rewrite wp_eq /wp_def {1}/uPred_holds.
     intros n. revert E e Φ Hproper.
     induction n as [n IH] using lt_wf_ind=> E e Φ Hproper r1 Hr1 Hwp.
-    (* FIXME: This is *slow* *)
-    apply wp_fix_unfold. { done. }
+    apply wp_fix_unfold; first done.
     intros rf k Ef σ1 ???. split.
     - intros ? Hval. destruct Hwp as [??? Hpvs|]; last by destruct (to_val e1).
       rewrite pvs_eq in Hpvs.
@@ -172,5 +171,4 @@ Section def.
         apply IH, Hef; first omega; last done.
         apply wsat_valid in Hw; last omega. solve_validN.
   Qed.
-
 End def.
-- 
GitLab