Commit 8b91a56a by Lennard Gäher

### fixpoint lemmas

parent 259f36a6
Pipeline #51144 failed with stage
in 0 seconds
 ... ... @@ -25,6 +25,9 @@ Definition bi_greatest_fixpoint {PROP : bi} {A : ofe} tc_opaque (∃ Φ : A -n> PROP, □ (∀ x, Φ x -∗ F Φ x) ∗ Φ x)%I. Global Arguments bi_greatest_fixpoint : simpl never. Lemma least_fixpoint_ne' {PROP : bi} {A : ofe} (F: (A → PROP) → (A → PROP)): (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F). Proof. solve_proper. Qed. Global Instance least_fixpoint_ne {PROP : bi} {A : ofe} n : Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==> dist n ==> dist n) bi_least_fixpoint. ... ... @@ -87,6 +90,9 @@ Proof. do 3 f_equiv; last solve_proper. repeat f_equiv. apply HF. Qed. Lemma greatest_fixpoint_ne' {PROP : bi} {A : ofe} (F: (A → PROP) → (A → PROP)): (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F). Proof. solve_proper. Qed. Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofe} n : Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==> dist n ==> dist n) bi_greatest_fixpoint. ... ... @@ -125,4 +131,40 @@ Section greatest. Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} : □ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x. Proof. iIntros "#HΦ" (x) "Hx". iExists (OfeMor Φ). auto. Qed. Lemma greatest_fixpoint_strong_coind (Φ : A → PROP) `{!NonExpansive Φ} : □ (∀ y, Φ y -∗ F (λ x, Φ x ∨ bi_greatest_fixpoint F x) y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x. Proof using Type*. trans (∀ x, Φ x ∨ bi_greatest_fixpoint F x -∗ bi_greatest_fixpoint F x)%I; last first. { iIntros "H" (x) "Φ". iApply "H". by iLeft. } 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". - 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. *) 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*. 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. 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!