fixpoint.v 3.94 KB
Newer Older
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's avatar
Ralf Jung committed
6
7
(** Least and greatest fixpoint of a monotone function, defined entirely inside
    the logic.  *)
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 Φ)
}.
12
Arguments bi_mono_pred {_ _ _ _} _ _.
13
Local Existing Instance bi_mono_pred_ne.
14

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's avatar
Ralf Jung committed
18

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.
22

Ralf Jung's avatar
Ralf Jung committed
23
Section least.
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's avatar
Ralf Jung committed
28

29
  Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x  uPred_least_fixpoint F x.
Ralf Jung's avatar
Ralf Jung committed
30
  Proof.
31
    iIntros "HF" (Φ) "#Hincl".
32
    iApply "Hincl". iApply (bi_mono_pred _ Φ); last done.
Ralf Jung's avatar
Ralf Jung committed
33
34
35
    iIntros "!#" (y) "Hy". iApply "Hy". done.
  Qed.

36
  Lemma least_fixpoint_unfold_1 x :
Ralf Jung's avatar
Ralf Jung committed
37
38
    uPred_least_fixpoint F x  F (uPred_least_fixpoint F) x.
  Proof.
39
40
    iIntros "HF". iApply ("HF" $! (CofeMor (F (uPred_least_fixpoint F))) with "[#]").
    iIntros "!#" (y) "Hy". iApply bi_mono_pred; last done. iIntros "!#" (z) "?".
41
    by iApply least_fixpoint_unfold_2.
Ralf Jung's avatar
Ralf Jung committed
42
43
  Qed.

44
  Corollary least_fixpoint_unfold x :
Ralf Jung's avatar
Ralf Jung committed
45
46
    uPred_least_fixpoint F x  F (uPred_least_fixpoint F) x.
  Proof.
47
    apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2.
Ralf Jung's avatar
Ralf Jung committed
48
49
  Qed.

50
  Lemma least_fixpoint_ind (Φ : A  uPred M) `{!NonExpansive Φ} :
51
     ( y, F Φ y  Φ y)   x, uPred_least_fixpoint F x  Φ x.
52
53
54
  Proof.
    iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
  Qed.
55
56
57
58
59
60
61
62
63
64
65
66

  Lemma least_fixpoint_strong_ind (Φ : A  uPred M) `{!NonExpansive Φ} :
     ( y, F (λ x, Φ x  uPred_least_fixpoint F x) y  Φ y)
      x, uPred_least_fixpoint F x  Φ x.
  Proof.
    trans ( x, uPred_least_fixpoint F x  Φ x  uPred_least_fixpoint F x)%I.
    { iIntros "#HΦ". iApply least_fixpoint_ind; 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.
Ralf Jung's avatar
Ralf Jung committed
67
68
69
End least.

Section greatest.
70
71
72
73
  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.
74

75
  Lemma greatest_fixpoint_unfold_1 x :
Ralf Jung's avatar
Ralf Jung committed
76
    uPred_greatest_fixpoint F x  F (uPred_greatest_fixpoint F) x.
77
  Proof.
78
    iDestruct 1 as (Φ) "[#Hincl HΦ]".
79
    iApply (bi_mono_pred Φ (uPred_greatest_fixpoint F)).
80
    - iIntros "!#" (y) "Hy". iExists Φ. auto.
81
82
83
    - by iApply "Hincl".
  Qed.

84
  Lemma greatest_fixpoint_unfold_2 x :
Ralf Jung's avatar
Ralf Jung committed
85
    F (uPred_greatest_fixpoint F) x  uPred_greatest_fixpoint F x.
86
  Proof.
87
    iIntros "HF". iExists (CofeMor (F (uPred_greatest_fixpoint F))).
88
    iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[] Hy").
89
    iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
90
91
  Qed.

92
  Corollary greatest_fixpoint_unfold x :
Ralf Jung's avatar
Ralf Jung committed
93
    uPred_greatest_fixpoint F x  F (uPred_greatest_fixpoint F) x.
94
  Proof.
95
    apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
96
97
  Qed.

98
  Lemma greatest_fixpoint_coind (Φ : A  uPred M) `{!NonExpansive Φ} :
99
     ( y, Φ y  F Φ y)   x, Φ x  uPred_greatest_fixpoint F x.
100
  Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). by iIntros "{$Hx} !#". Qed.
Ralf Jung's avatar
Ralf Jung committed
101
End greatest.