From 2bc4656d4abb965e8bedd7bb620ef0dfa405fef1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 Aug 2017 17:23:27 +0200
Subject: [PATCH] also do least fixpoint; fix naming

---
 theories/base_logic/derived.v |  5 +++
 theories/base_logic/fix.v     | 65 ++++++++++++++++++++++++++---------
 2 files changed, 54 insertions(+), 16 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 01f7366d0..8ec056b86 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -541,6 +541,11 @@ Proof.
   apply always_intro', impl_intro_r.
   by rewrite always_and_sep_l' always_elim wand_elim_l.
 Qed.
+Lemma wand_impl_always P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
+Proof.
+  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
+  apply impl_intro_l. by rewrite always_and_sep_l' wand_elim_r.
+Qed.
 Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
 Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
 Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
diff --git a/theories/base_logic/fix.v b/theories/base_logic/fix.v
index 291de0f97..717845fbc 100644
--- a/theories/base_logic/fix.v
+++ b/theories/base_logic/fix.v
@@ -3,41 +3,74 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 Import uPred.
 
-(** Greatest fixpoint of a monotone function, defined entirely inside
-    the logic.
-    TODO: Also do least fixpoint.
-*)
+(** Least and greatest fixpoint of a monotone function, defined entirely inside
+    the logic.  *)
 
 Definition uPred_mono_pred {M A} (F : (A → uPred M) → (A → uPred M)) :=
   ∀ P Q, ((□ ∀ x, P x -∗ Q x) -∗ ∀ x, F P x -∗ F Q x)%I.
 
-Definition iGFix {M A} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M :=
+Definition uPred_least_fixpoint {M A} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M :=
+  (∀ P, □ (∀ x, F P x -∗ P x) → P x)%I.
+
+Definition uPred_greatest_fixpoint {M A} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M :=
   (∃ P, □ (∀ x, P x -∗ F P x) ∧ P x)%I.
 
-Section iGFix.
+Section least.
+  Context {M : ucmraT} {A} (F : (A → uPred M) → (A → uPred M)) (Hmono : uPred_mono_pred F).
+
+  Lemma F_fix_implies_least_fixpoint x : F (uPred_least_fixpoint F) x ⊢ uPred_least_fixpoint F x.
+  Proof.
+    iIntros "HF" (P). iApply wand_impl_always. iIntros "#Hincl".
+    iApply "Hincl". iApply (Hmono _ P); last done.
+    iIntros "!#" (y) "Hy". iApply "Hy". done.
+  Qed.
+
+  Lemma least_fixpoint_implies_F_fix x :
+    uPred_least_fixpoint F x ⊢ F (uPred_least_fixpoint F) x.
+  Proof.
+    iIntros "HF". iApply "HF". iIntros "!#" (y) "Hy".
+    iApply Hmono; last done. iIntros "!#" (z) "?".
+    by iApply F_fix_implies_least_fixpoint.
+  Qed.
+
+  Corollary uPred_least_fixpoint_unfold x :
+    uPred_least_fixpoint F x ≡ F (uPred_least_fixpoint F) x.
+  Proof.
+    apply (anti_symm _); auto using least_fixpoint_implies_F_fix, F_fix_implies_least_fixpoint.
+  Qed.
+
+  Lemma uPred_least_fixpoint_ind (P : A → uPred M) (x : A) :
+    uPred_least_fixpoint F x -∗ □ (∀ y, F P y -∗ P y) -∗ P x.
+  Proof. iIntros "HF #HP". iApply "HF". done. Qed.
+End least.
+
+Section greatest.
   Context {M : ucmraT} {A} (F : (A → uPred M) → (A → uPred M)) (Hmono : uPred_mono_pred F).
 
-  Lemma iGFix_implies_F_iGFix x : iGFix F x ⊢ F (iGFix F) x.
+  Lemma greatest_fixpoint_implies_F_fix x :
+    uPred_greatest_fixpoint F x ⊢ F (uPred_greatest_fixpoint F) x.
   Proof.
     iDestruct 1 as (P) "[#Hincl HP]".
-    iApply (Hmono P (iGFix F)).
+    iApply (Hmono P (uPred_greatest_fixpoint F)).
     - iAlways. iIntros (y) "Hy". iExists P. by iSplit.
     - by iApply "Hincl".
   Qed.
 
-  Lemma F_iGFix_implies_iGFix x : F (iGFix F) x ⊢ iGFix F x.
+  Lemma F_fix_implies_greatest_fixpoint x :
+    F (uPred_greatest_fixpoint F) x ⊢ uPred_greatest_fixpoint F x.
   Proof.
-    iIntros "HF". iExists (F (iGFix F)).
+    iIntros "HF". iExists (F (uPred_greatest_fixpoint F)).
     iIntros "{$HF} !#"; iIntros (y) "Hy". iApply (Hmono with "[] Hy").
-    iAlways. iIntros (z). by iApply iGFix_implies_F_iGFix.
+    iAlways. iIntros (z). by iApply greatest_fixpoint_implies_F_fix.
   Qed.
 
-  Corollary iGFix_unfold x : iGFix F x ≡ F (iGFix F) x.
+  Corollary uPred_greatest_fixpoint_unfold x :
+    uPred_greatest_fixpoint F x ≡ F (uPred_greatest_fixpoint F) x.
   Proof.
-    apply (anti_symm _); auto using iGFix_implies_F_iGFix, F_iGFix_implies_iGFix.
+    apply (anti_symm _); auto using greatest_fixpoint_implies_F_fix, F_fix_implies_greatest_fixpoint.
   Qed.
 
-  Lemma Fix_coind (P : A → uPred M) (x : A) :
-    □ (∀ y, P y -∗ F P y) -∗ P x -∗ iGFix F x.
+  Lemma uPred_greatest_fixpoint_coind (P : A → uPred M) (x : A) :
+    □ (∀ y, P y -∗ F P y) -∗ P x -∗ uPred_greatest_fixpoint F x.
   Proof. iIntros "#HP Hx". iExists P. by iIntros "{$Hx} !#". Qed.
-End iGFix.
+End greatest.
-- 
GitLab