fixpoint.v 3.91 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 :=
17
  ( Φ : A -n> PROP, <pers> ( x, F Φ x - Φ x)  Φ x)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
20

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

Section least.
Ralf Jung's avatar
Ralf Jung committed
24
  Context {PROP : bi} {A : ofeT} (F : (A  PROP)  (A  PROP)) `{!BiMonoPred F}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 Φ} :
51
     ( y, F Φ y - Φ y) -  x, bi_least_fixpoint F x - Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54
55
56
  Proof.
    iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
  Qed.

  Lemma least_fixpoint_strong_ind (Φ : A  PROP) `{!NonExpansive Φ} :
57
     ( y, F (λ x, Φ x  bi_least_fixpoint F x) y - Φ y) -
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
70
  Context {PROP : bi} {A : ofeT} (F : (A  PROP)  (A  PROP)) `{!BiMonoPred F}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
    iSplit; last done. iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
91
92
93
94
95
96
97
98
    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 Φ} :
99
     ( y, Φ y - F Φ y) -  x, Φ x - bi_greatest_fixpoint F x.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
  Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). auto. Qed.
End greatest.