From 9e429c46d485c755e40a0bc79602121993ef94b5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Sep 2017 01:05:31 +0200
Subject: [PATCH] Make sure that the fixpoints are non-expansive.

In order to do that, we need to quantify over non-expansive
predicates instead of arbitrary predicates.
---
 theories/base_logic/fixpoint.v | 45 +++++++++++++++++++++-------------
 1 file changed, 28 insertions(+), 17 deletions(-)

diff --git a/theories/base_logic/fixpoint.v b/theories/base_logic/fixpoint.v
index 3f6f806f5..36a69473d 100644
--- a/theories/base_logic/fixpoint.v
+++ b/theories/base_logic/fixpoint.v
@@ -5,20 +5,26 @@ Import uPred.
 
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
-Class BIMonoPred {M A} (F : (A → uPred M) → (A → uPred M)) :=
-  bi_mono_pred Φ Ψ : ((□ ∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I.
+Class BIMonoPred {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) := {
+  bi_mono_pred Φ Ψ : ((□ ∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I;
+  bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
+}.
 Arguments bi_mono_pred {_ _ _ _} _ _.
+Local Existing Instance bi_mono_pred_ne.
 
-Definition uPred_least_fixpoint {M A} (F : (A → uPred M) → (A → uPred M))
-    (x : A) : uPred M :=
-  (∀ Φ, □ (∀ x, F Φ x → Φ x) → Φ x)%I.
+Definition uPred_least_fixpoint {M} {A : ofeT}
+    (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M :=
+  (∀ Φ : A -n> uPredC M, □ (∀ x, F Φ x → Φ x) → Φ x)%I.
 
-Definition uPred_greatest_fixpoint {M A} (F : (A → uPred M) → (A → uPred M))
-    (x : A) : uPred M :=
-  (∃ Φ, □ (∀ x, Φ x → F Φ x) ∧ Φ x)%I.
+Definition uPred_greatest_fixpoint {M} {A : ofeT}
+    (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M :=
+  (∃ Φ : A -n> uPredC M, □ (∀ x, Φ x → F Φ x) ∧ Φ x)%I.
 
 Section least.
-  Context {M A} (F : (A → uPred M) → (A → uPred M)) `{!BIMonoPred F}.
+  Context {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) `{!BIMonoPred F}.
+
+  Global Instance least_fixpoint_ne : NonExpansive (uPred_least_fixpoint F).
+  Proof. solve_proper. Qed.
 
   Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x ⊢ uPred_least_fixpoint F x.
   Proof.
@@ -30,8 +36,8 @@ Section least.
   Lemma least_fixpoint_unfold_1 x :
     uPred_least_fixpoint F x ⊢ F (uPred_least_fixpoint F) x.
   Proof.
-    iIntros "HF". iApply "HF". iIntros "!#" (y) "Hy".
-    iApply bi_mono_pred; last done. iIntros "!#" (z) "?".
+    iIntros "HF". iApply ("HF" $! (CofeMor (F (uPred_least_fixpoint F))) with "[#]").
+    iIntros "!#" (y) "Hy". iApply bi_mono_pred; last done. iIntros "!#" (z) "?".
     by iApply least_fixpoint_unfold_2.
   Qed.
 
@@ -41,13 +47,18 @@ Section least.
     apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2.
   Qed.
 
-  Lemma least_fixpoint_ind (Φ : A → uPred M) :
+  Lemma least_fixpoint_ind (Φ : A → uPred M) `{!NonExpansive Φ} :
     □ (∀ y, F Φ y → Φ y) ⊢ ∀ x, uPred_least_fixpoint F x → Φ x.
-  Proof. iIntros "#HΦ" (x) "HF". iApply "HF". done. Qed.
+  Proof.
+    iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
+  Qed.
 End least.
 
 Section greatest.
-  Context {M A} (F : (A → uPred M) → (A → uPred M)) `{!BIMonoPred F}.
+  Context {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) `{!BIMonoPred F}.
+
+  Global Instance greatest_fixpoint_ne : NonExpansive (uPred_greatest_fixpoint F).
+  Proof. solve_proper. Qed.
 
   Lemma greatest_fixpoint_unfold_1 x :
     uPred_greatest_fixpoint F x ⊢ F (uPred_greatest_fixpoint F) x.
@@ -61,7 +72,7 @@ Section greatest.
   Lemma greatest_fixpoint_unfold_2 x :
     F (uPred_greatest_fixpoint F) x ⊢ uPred_greatest_fixpoint F x.
   Proof.
-    iIntros "HF". iExists (F (uPred_greatest_fixpoint F)).
+    iIntros "HF". iExists (CofeMor (F (uPred_greatest_fixpoint F))).
     iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[] Hy").
     iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
   Qed.
@@ -72,7 +83,7 @@ Section greatest.
     apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
   Qed.
 
-  Lemma greatest_fixpoint_coind (Φ : A → uPred M) :
+  Lemma greatest_fixpoint_coind (Φ : A → uPred M) `{!NonExpansive Φ} :
     □ (∀ y, Φ y → F Φ y) ⊢ ∀ x, Φ x → uPred_greatest_fixpoint F x.
-  Proof. iIntros "#HΦ" (x) "Hx". iExists Φ. by iIntros "{$Hx} !#". Qed.
+  Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). by iIntros "{$Hx} !#". Qed.
 End greatest.
-- 
GitLab