fixpoint.v 3.39 KB
 Ralf Jung committed Aug 22, 2017 1 2 3 4 5 ``````From iris.base_logic Require Import base_logic. From iris.proofmode Require Import tactics. Set Default Proof Using "Type*". Import uPred. `````` Ralf Jung committed Aug 23, 2017 6 7 ``````(** Least and greatest fixpoint of a monotone function, defined entirely inside the logic. *) `````` Robbert Krebbers committed Sep 21, 2017 8 9 10 11 ``````Class BIMonoPred {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) := { bi_mono_pred Φ Ψ : ((□ ∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I; bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ) }. `````` Robbert Krebbers committed Sep 19, 2017 12 ``````Arguments bi_mono_pred {_ _ _ _} _ _. `````` Robbert Krebbers committed Sep 21, 2017 13 ``````Local Existing Instance bi_mono_pred_ne. `````` Ralf Jung committed Aug 22, 2017 14 `````` `````` Robbert Krebbers committed Sep 21, 2017 15 16 17 ``````Definition uPred_least_fixpoint {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M := (∀ Φ : A -n> uPredC M, □ (∀ x, F Φ x → Φ x) → Φ x)%I. `````` Ralf Jung committed Aug 23, 2017 18 `````` `````` Robbert Krebbers committed Sep 21, 2017 19 20 21 ``````Definition uPred_greatest_fixpoint {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M := (∃ Φ : A -n> uPredC M, □ (∀ x, Φ x → F Φ x) ∧ Φ x)%I. `````` Ralf Jung committed Aug 22, 2017 22 `````` `````` Ralf Jung committed Aug 23, 2017 23 ``````Section least. `````` Robbert Krebbers committed Sep 21, 2017 24 25 26 27 `````` Context {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) `{!BIMonoPred F}. Global Instance least_fixpoint_ne : NonExpansive (uPred_least_fixpoint F). Proof. solve_proper. Qed. `````` Ralf Jung committed Aug 23, 2017 28 `````` `````` Robbert Krebbers committed Aug 28, 2017 29 `````` Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x ⊢ uPred_least_fixpoint F x. `````` Ralf Jung committed Aug 23, 2017 30 `````` Proof. `````` Robbert Krebbers committed Aug 28, 2017 31 `````` iIntros "HF" (Φ) "#Hincl". `````` Robbert Krebbers committed Sep 19, 2017 32 `````` iApply "Hincl". iApply (bi_mono_pred _ Φ); last done. `````` Ralf Jung committed Aug 23, 2017 33 34 35 `````` iIntros "!#" (y) "Hy". iApply "Hy". done. Qed. `````` Robbert Krebbers committed Aug 28, 2017 36 `````` Lemma least_fixpoint_unfold_1 x : `````` Ralf Jung committed Aug 23, 2017 37 38 `````` uPred_least_fixpoint F x ⊢ F (uPred_least_fixpoint F) x. Proof. `````` Robbert Krebbers committed Sep 21, 2017 39 40 `````` iIntros "HF". iApply ("HF" \$! (CofeMor (F (uPred_least_fixpoint F))) with "[#]"). iIntros "!#" (y) "Hy". iApply bi_mono_pred; last done. iIntros "!#" (z) "?". `````` Robbert Krebbers committed Aug 28, 2017 41 `````` by iApply least_fixpoint_unfold_2. `````` Ralf Jung committed Aug 23, 2017 42 43 `````` Qed. `````` Robbert Krebbers committed Aug 28, 2017 44 `````` Corollary least_fixpoint_unfold x : `````` Ralf Jung committed Aug 23, 2017 45 46 `````` uPred_least_fixpoint F x ≡ F (uPred_least_fixpoint F) x. Proof. `````` Robbert Krebbers committed Aug 28, 2017 47 `````` apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2. `````` Ralf Jung committed Aug 23, 2017 48 49 `````` Qed. `````` Robbert Krebbers committed Sep 21, 2017 50 `````` Lemma least_fixpoint_ind (Φ : A → uPred M) `{!NonExpansive Φ} : `````` Robbert Krebbers committed Aug 28, 2017 51 `````` □ (∀ y, F Φ y → Φ y) ⊢ ∀ x, uPred_least_fixpoint F x → Φ x. `````` Robbert Krebbers committed Sep 21, 2017 52 53 54 `````` Proof. iIntros "#HΦ" (x) "HF". by iApply ("HF" \$! (CofeMor Φ) with "[#]"). Qed. `````` Ralf Jung committed Aug 23, 2017 55 56 57 ``````End least. Section greatest. `````` Robbert Krebbers committed Sep 21, 2017 58 59 60 61 `````` Context {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) `{!BIMonoPred F}. Global Instance greatest_fixpoint_ne : NonExpansive (uPred_greatest_fixpoint F). Proof. solve_proper. Qed. `````` Ralf Jung committed Aug 22, 2017 62 `````` `````` Robbert Krebbers committed Aug 28, 2017 63 `````` Lemma greatest_fixpoint_unfold_1 x : `````` Ralf Jung committed Aug 23, 2017 64 `````` uPred_greatest_fixpoint F x ⊢ F (uPred_greatest_fixpoint F) x. `````` Ralf Jung committed Aug 22, 2017 65 `````` Proof. `````` Robbert Krebbers committed Aug 28, 2017 66 `````` iDestruct 1 as (Φ) "[#Hincl HΦ]". `````` Robbert Krebbers committed Sep 19, 2017 67 `````` iApply (bi_mono_pred Φ (uPred_greatest_fixpoint F)). `````` Robbert Krebbers committed Aug 28, 2017 68 `````` - iIntros "!#" (y) "Hy". iExists Φ. auto. `````` Ralf Jung committed Aug 22, 2017 69 70 71 `````` - by iApply "Hincl". Qed. `````` Robbert Krebbers committed Aug 28, 2017 72 `````` Lemma greatest_fixpoint_unfold_2 x : `````` Ralf Jung committed Aug 23, 2017 73 `````` F (uPred_greatest_fixpoint F) x ⊢ uPred_greatest_fixpoint F x. `````` Ralf Jung committed Aug 22, 2017 74 `````` Proof. `````` Robbert Krebbers committed Sep 21, 2017 75 `````` iIntros "HF". iExists (CofeMor (F (uPred_greatest_fixpoint F))). `````` Robbert Krebbers committed Sep 19, 2017 76 `````` iIntros "{\$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[] Hy"). `````` Robbert Krebbers committed Aug 28, 2017 77 `````` iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1. `````` Ralf Jung committed Aug 22, 2017 78 79 `````` Qed. `````` Robbert Krebbers committed Aug 28, 2017 80 `````` Corollary greatest_fixpoint_unfold x : `````` Ralf Jung committed Aug 23, 2017 81 `````` uPred_greatest_fixpoint F x ≡ F (uPred_greatest_fixpoint F) x. `````` Ralf Jung committed Aug 22, 2017 82 `````` Proof. `````` Robbert Krebbers committed Aug 28, 2017 83 `````` apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2. `````` Ralf Jung committed Aug 22, 2017 84 85 `````` Qed. `````` Robbert Krebbers committed Sep 21, 2017 86 `````` Lemma greatest_fixpoint_coind (Φ : A → uPred M) `{!NonExpansive Φ} : `````` Robbert Krebbers committed Aug 28, 2017 87 `````` □ (∀ y, Φ y → F Φ y) ⊢ ∀ x, Φ x → uPred_greatest_fixpoint F x. `````` Robbert Krebbers committed Sep 21, 2017 88 `````` Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). by iIntros "{\$Hx} !#". Qed. `````` Ralf Jung committed Aug 23, 2017 89 ``End greatest.``