fixpoint.v 2.85 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
Class BIMonoPred {M A} (F : (A  uPred M)  (A  uPred M)) :=
  bi_mono_pred Φ Ψ : ((  x, Φ x - Ψ x)   x, F Φ x - F Ψ x)%I.
Arguments bi_mono_pred {_ _ _ _} _ _.
11

12
13
14
Definition uPred_least_fixpoint {M A} (F : (A  uPred M)  (A  uPred M))
    (x : A) : uPred M :=
  ( Φ,  ( x, F Φ x  Φ x)  Φ x)%I.
Ralf Jung's avatar
Ralf Jung committed
15

16
17
18
Definition uPred_greatest_fixpoint {M A} (F : (A  uPred M)  (A  uPred M))
    (x : A) : uPred M :=
  ( Φ,  ( x, Φ x  F Φ x)  Φ x)%I.
19

Ralf Jung's avatar
Ralf Jung committed
20
Section least.
21
  Context {M A} (F : (A  uPred M)  (A  uPred M)) `{!BIMonoPred F}.
Ralf Jung's avatar
Ralf Jung committed
22

23
  Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x  uPred_least_fixpoint F x.
Ralf Jung's avatar
Ralf Jung committed
24
  Proof.
25
    iIntros "HF" (Φ) "#Hincl".
26
    iApply "Hincl". iApply (bi_mono_pred _ Φ); last done.
Ralf Jung's avatar
Ralf Jung committed
27
28
29
    iIntros "!#" (y) "Hy". iApply "Hy". done.
  Qed.

30
  Lemma least_fixpoint_unfold_1 x :
Ralf Jung's avatar
Ralf Jung committed
31
32
33
    uPred_least_fixpoint F x  F (uPred_least_fixpoint F) x.
  Proof.
    iIntros "HF". iApply "HF". iIntros "!#" (y) "Hy".
34
    iApply bi_mono_pred; last done. iIntros "!#" (z) "?".
35
    by iApply least_fixpoint_unfold_2.
Ralf Jung's avatar
Ralf Jung committed
36
37
  Qed.

38
  Corollary least_fixpoint_unfold x :
Ralf Jung's avatar
Ralf Jung committed
39
40
    uPred_least_fixpoint F x  F (uPred_least_fixpoint F) x.
  Proof.
41
    apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2.
Ralf Jung's avatar
Ralf Jung committed
42
43
  Qed.

44
45
46
  Lemma least_fixpoint_ind (Φ : A  uPred M) :
     ( y, F Φ y  Φ y)   x, uPred_least_fixpoint F x  Φ x.
  Proof. iIntros "#HΦ" (x) "HF". iApply "HF". done. Qed.
Ralf Jung's avatar
Ralf Jung committed
47
48
49
End least.

Section greatest.
50
  Context {M A} (F : (A  uPred M)  (A  uPred M)) `{!BIMonoPred F}.
51

52
  Lemma greatest_fixpoint_unfold_1 x :
Ralf Jung's avatar
Ralf Jung committed
53
    uPred_greatest_fixpoint F x  F (uPred_greatest_fixpoint F) x.
54
  Proof.
55
    iDestruct 1 as (Φ) "[#Hincl HΦ]".
56
    iApply (bi_mono_pred Φ (uPred_greatest_fixpoint F)).
57
    - iIntros "!#" (y) "Hy". iExists Φ. auto.
58
59
60
    - by iApply "Hincl".
  Qed.

61
  Lemma greatest_fixpoint_unfold_2 x :
Ralf Jung's avatar
Ralf Jung committed
62
    F (uPred_greatest_fixpoint F) x  uPred_greatest_fixpoint F x.
63
  Proof.
Ralf Jung's avatar
Ralf Jung committed
64
    iIntros "HF". iExists (F (uPred_greatest_fixpoint F)).
65
    iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[] Hy").
66
    iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
67
68
  Qed.

69
  Corollary greatest_fixpoint_unfold x :
Ralf Jung's avatar
Ralf Jung committed
70
    uPred_greatest_fixpoint F x  F (uPred_greatest_fixpoint F) x.
71
  Proof.
72
    apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
73
74
  Qed.

75
76
77
  Lemma greatest_fixpoint_coind (Φ : A  uPred M) :
     ( y, Φ y  F Φ y)   x, Φ x  uPred_greatest_fixpoint F x.
  Proof. iIntros "#HΦ" (x) "Hx". iExists Φ. by iIntros "{$Hx} !#". Qed.
Ralf Jung's avatar
Ralf Jung committed
78
End greatest.