Commit ee6a9043 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

integrate some of the comments

parent 8b91a56a
Pipeline #51226 passed with stage
in 18 minutes and 45 seconds
......@@ -141,30 +141,35 @@ Section greatest.
iIntros "#HΦ". iApply (greatest_fixpoint_coind with "[]"); first solve_proper.
iIntros "!>" (y) "[H|H]"; first by iApply "HΦ".
iApply (bi_mono_pred (bi_greatest_fixpoint F) with "[#] [H]"); first solve_proper.
- iModIntro. iIntros (x) "H". iRight. iApply "H".
- iIntros "!>" (x) "H". iRight. iApply "H".
- by iApply greatest_fixpoint_unfold_1.
Qed.
End greatest.
Local Instance greatest_fixpoint_paco_mono {PROP : bi} {A : ofe} (F : (A PROP) (A PROP)) `{!BiMonoPred F} Φ:
NonExpansive Φ
BiMonoPred (λ (Ψ : A PROP) (a : A), Φ a F Ψ a)%I.
Proof.
split.
- intros Ψ Ψ' Hne Hne'. iIntros "#Mon" (x) "[H1|H2]"; first by iLeft.
iRight. iApply (bi_mono_pred with "[] H2"). by iModIntro.
- iIntros (Ψ Hne). solve_proper.
Qed.
(* "parameterized coinduction" principle for accumulating knowledge in the coinduction hypothesis. *)
(**
This lemma allows for parameterized coinduction, a stronger coinduction principle:
it allows to prove the hypothesis [Φ] not just after one step
(like [greatest_fixpoint_strong_coind]),
but after any number of unfoldings of the greatest fixpoint, by integrating it into
the predicate the fixpoint is taken of.
This encodes a way of accumulating "knowledge" in the coinduction hypothesis:
if you return to the "initial point" [Φ] of the coinduction after some number of
unfoldings (not just one), the proof is done.
*)
Lemma greatest_fixpoint_paco {PROP : bi} {A : ofe}
(F : (A PROP) (A PROP)) `{!BiMonoPred F} (Φ : A PROP) `{!NonExpansive Φ} :
( y, Φ y - F (bi_greatest_fixpoint (λ Ψ a, Φ a F Ψ a)) y) -
x, Φ x - bi_greatest_fixpoint F x.
Proof using Type*.
assert (Hmon : BiMonoPred (λ (Ψ : A PROP) (a : A), Φ a F Ψ a)%I).
{ split.
- intros Ψ Ψ' Hne Hne'. iIntros "#Mon" (x) "[H1|H2]"; first by iLeft.
iRight. iApply (bi_mono_pred with "[] H2"). by iModIntro.
- iIntros (Ψ Hne). solve_proper.
}
iIntros "#Hmon" (x) "HΦ". iDestruct ("Hmon" with "HΦ") as "HF".
rewrite greatest_fixpoint_unfold. iApply (bi_mono_pred with "[] HF").
iModIntro. iIntros (y) "HG". iApply (greatest_fixpoint_coind with "[] HG").
iModIntro. iIntros (z) "Hf". rewrite greatest_fixpoint_unfold.
iIntros "!>" (y) "HG". iApply (greatest_fixpoint_coind with "[] HG").
iIntros "!>" (z) "Hf". rewrite greatest_fixpoint_unfold.
iDestruct "Hf" as "[HΦ|$]". by iApply "Hmon".
Qed.
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