fixpoint.v 5.12 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Ralf Jung committed
8
Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A  PROP)  (A  PROP)) := {
9
  bi_mono_pred Φ Ψ : (<pers> ( x, Φ x - Ψ x)   x, F Φ x - F Ψ x)%I;
Robbert Krebbers's avatar
Robbert Krebbers committed
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 :=
Ralf Jung's avatar
Ralf Jung committed
17 18
  tc_opaque ( Φ : A -n> PROP, <pers> ( x, F Φ x - Φ x)  Φ x)%I.
Arguments bi_least_fixpoint : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21

Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
    (F : (A  PROP)  (A  PROP)) (x : A) : PROP :=
Ralf Jung's avatar
Ralf Jung committed
22 23
  tc_opaque ( Φ : A -n> PROP, <pers> ( x, Φ x - F Φ x)  Φ x)%I.
Arguments bi_greatest_fixpoint : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
24

25 26 27
Global Instance least_fixpoint_ne {PROP : bi} {A : ofeT} n :
  Proper (pointwise_relation (A  PROP) (pointwise_relation A (dist n)) ==>
          dist n ==> dist n) bi_least_fixpoint.
Ralf Jung's avatar
Ralf Jung committed
28
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30 31 32
Global Instance least_fixpoint_proper {PROP : bi} {A : ofeT} :
  Proper (pointwise_relation (A  PROP) (pointwise_relation A ()) ==>
          () ==> ()) bi_least_fixpoint.
Proof. solve_proper. Qed.
33

Robbert Krebbers's avatar
Robbert Krebbers committed
34
Section least.
Ralf Jung's avatar
Ralf Jung committed
35
  Context {PROP : bi} {A : ofeT} (F : (A  PROP)  (A  PROP)) `{!BiMonoPred F}.
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38

  Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x  bi_least_fixpoint F x.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
39
    rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
    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 Φ} :
59
     ( y, F Φ y - Φ y) -  x, bi_least_fixpoint F x - Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61 62 63 64
  Proof.
    iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
  Qed.

  Lemma least_fixpoint_strong_ind (Φ : A  PROP) `{!NonExpansive Φ} :
65
     ( y, F (λ x, Φ x  bi_least_fixpoint F x) y - Φ y) -
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68 69 70 71 72 73 74 75 76
     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.

77 78 79 80 81 82 83 84 85 86 87 88 89 90
Lemma greatest_fixpoint_ne_outer {PROP : bi} {A : ofeT}
  (F1 : (A  PROP)  (A  PROP))
  (F2 : (A  PROP)  (A  PROP)):
  ( Φ x n, F1 Φ x {n} F2 Φ x)   x1 x2 n,
  (dist n) x1 x2  (dist n) (bi_greatest_fixpoint F1 x1) (bi_greatest_fixpoint F2 x2).
Proof.
  intros HF ??? Hx. rewrite /bi_greatest_fixpoint /=.
  f_equiv. f_equiv. f_equiv. 2: solve_proper.
  f_equiv. f_equiv. f_equiv. f_equiv. apply HF.
Qed.

Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofeT} n :
  Proper (pointwise_relation (A  PROP) (pointwise_relation A (dist n)) ==>
          dist n ==> dist n) bi_greatest_fixpoint.
Ralf Jung's avatar
Ralf Jung committed
91
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93 94 95
Global Instance greatest_fixpoint_proper {PROP : bi} {A : ofeT} :
  Proper (pointwise_relation (A  PROP) (pointwise_relation A ()) ==>
          () ==> ()) bi_greatest_fixpoint.
Proof. solve_proper. Qed.
96

Robbert Krebbers's avatar
Robbert Krebbers committed
97
Section greatest.
98
  Context {PROP : bi} {A : ofeT} (F : (A  PROP)  (A  PROP)) `{!BiMonoPred F}.
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100 101 102 103 104 105 106 107 108 109 110 111 112

  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))).
113
    iSplit; last done. iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116 117 118 119 120 121 122 123
    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 Φ} :
124
     ( y, Φ y - F Φ y) -  x, Φ x - bi_greatest_fixpoint F x.
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
  Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). auto. Qed.
End greatest.