Commit 2bc4656d authored by Ralf Jung's avatar Ralf Jung

also do least fixpoint; fix naming

parent 90ef23f7
......@@ -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.
......
......@@ -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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment