fixpoint.v 3.99 KB
 Robbert Krebbers committed Oct 31, 2017 1 2 3 4 5 6 7 ``````From iris.bi Require Export bi. From iris.proofmode Require Import tactics. Set Default Proof Using "Type*". Import bi. (** Least and greatest fixpoint of a monotone function, defined entirely inside the logic. *) `````` Ralf Jung committed Dec 20, 2017 8 ``````Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := { `````` Robbert Krebbers committed Mar 04, 2018 9 `````` bi_mono_pred Φ Ψ : ( (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I; `````` Robbert Krebbers committed Oct 31, 2017 10 11 12 13 14 15 16 `````` bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ) }. Arguments bi_mono_pred {_ _ _ _} _ _. Local Existing Instance bi_mono_pred_ne. Definition bi_least_fixpoint {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) (x : A) : PROP := `````` Robbert Krebbers committed Mar 04, 2018 17 `````` (∀ Φ : A -n> PROP, (∀ x, F Φ x -∗ Φ x) → Φ x)%I. `````` Robbert Krebbers committed Oct 31, 2017 18 19 20 `````` Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) (x : A) : PROP := `````` Robbert Krebbers committed Mar 04, 2018 21 `````` (∃ Φ : A -n> PROP, (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I. `````` Robbert Krebbers committed Oct 31, 2017 22 23 `````` Section least. `````` Ralf Jung committed Dec 20, 2017 24 `````` Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}. `````` Robbert Krebbers committed Oct 31, 2017 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 `````` Global Instance least_fixpoint_ne : NonExpansive (bi_least_fixpoint F). Proof. solve_proper. Qed. Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x. Proof. iIntros "HF" (Φ) "#Hincl". iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#]"); last done. iIntros "!#" (y) "Hy". iApply ("Hy" with "[# //]"). Qed. Lemma least_fixpoint_unfold_1 x : bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x. Proof. iIntros "HF". iApply ("HF" \$! (CofeMor (F (bi_least_fixpoint F))) with "[#]"). iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#]"); last done. iIntros "!#" (z) "?". by iApply least_fixpoint_unfold_2. Qed. Corollary least_fixpoint_unfold x : bi_least_fixpoint F x ≡ F (bi_least_fixpoint F) x. Proof. apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2. Qed. Lemma least_fixpoint_ind (Φ : A → PROP) `{!NonExpansive Φ} : `````` Jacques-Henri Jourdan committed Nov 02, 2017 51 `````` □ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x. `````` Robbert Krebbers committed Oct 31, 2017 52 53 54 55 56 `````` Proof. iIntros "#HΦ" (x) "HF". by iApply ("HF" \$! (CofeMor Φ) with "[#]"). Qed. Lemma least_fixpoint_strong_ind (Φ : A → PROP) `{!NonExpansive Φ} : `````` Jacques-Henri Jourdan committed Nov 02, 2017 57 `````` □ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗ `````` Robbert Krebbers committed Oct 31, 2017 58 59 60 61 62 63 64 65 66 67 68 69 `````` ∀ x, bi_least_fixpoint F x -∗ Φ x. Proof. trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I. { iIntros "#HΦ". iApply (least_fixpoint_ind with "[]"); first solve_proper. iIntros "!#" (y) "H". iSplit; first by iApply "HΦ". iApply least_fixpoint_unfold_2. iApply (bi_mono_pred with "[#] H"). by iIntros "!# * [_ ?]". } by setoid_rewrite and_elim_l. Qed. End least. Section greatest. `````` Jacques-Henri Jourdan committed Dec 21, 2017 70 `````` Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}. `````` Robbert Krebbers committed Oct 31, 2017 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 `````` Global Instance greatest_fixpoint_ne : NonExpansive (bi_greatest_fixpoint F). Proof. solve_proper. Qed. Lemma greatest_fixpoint_unfold_1 x : bi_greatest_fixpoint F x ⊢ F (bi_greatest_fixpoint F) x. Proof. iDestruct 1 as (Φ) "[#Hincl HΦ]". iApply (bi_mono_pred Φ (bi_greatest_fixpoint F) with "[#]"). - iIntros "!#" (y) "Hy". iExists Φ. auto. - by iApply "Hincl". Qed. Lemma greatest_fixpoint_unfold_2 x : F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x. Proof. iIntros "HF". iExists (CofeMor (F (bi_greatest_fixpoint F))). `````` 88 89 `````` (* FIXME: The framing here adds an modality that we have to introduce. *) iIntros "{\$HF} !# !#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy"). `````` Robbert Krebbers committed Oct 31, 2017 90 91 92 93 94 95 96 97 98 99 `````` iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1. Qed. Corollary greatest_fixpoint_unfold x : bi_greatest_fixpoint F x ≡ F (bi_greatest_fixpoint F) x. Proof. apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2. Qed. Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} : `````` Jacques-Henri Jourdan committed Nov 02, 2017 100 `````` □ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x. `````` Robbert Krebbers committed Oct 31, 2017 101 102 `````` Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). auto. Qed. End greatest.``````