fixpoint.v 3.39 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.
Ralf Jung's avatar
Ralf Jung committed
55
56
57
End least.

Section greatest.
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.
62

63
  Lemma greatest_fixpoint_unfold_1 x :
Ralf Jung's avatar
Ralf Jung committed
64
    uPred_greatest_fixpoint F x  F (uPred_greatest_fixpoint F) x.
65
  Proof.
66
    iDestruct 1 as (Φ) "[#Hincl HΦ]".
67
    iApply (bi_mono_pred Φ (uPred_greatest_fixpoint F)).
68
    - iIntros "!#" (y) "Hy". iExists Φ. auto.
69
70
71
    - by iApply "Hincl".
  Qed.

72
  Lemma greatest_fixpoint_unfold_2 x :
Ralf Jung's avatar
Ralf Jung committed
73
    F (uPred_greatest_fixpoint F) x  uPred_greatest_fixpoint F x.
74
  Proof.
75
    iIntros "HF". iExists (CofeMor (F (uPred_greatest_fixpoint F))).
76
    iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[] Hy").
77
    iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
78
79
  Qed.

80
  Corollary greatest_fixpoint_unfold x :
Ralf Jung's avatar
Ralf Jung committed
81
    uPred_greatest_fixpoint F x  F (uPred_greatest_fixpoint F) x.
82
  Proof.
83
    apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
84
85
  Qed.

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