greatest_laterable_fixpoint.v 6.23 KB
Newer Older
Ike Mulder's avatar
Ike Mulder committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
From iris.bi Require Export bi telescopes lib.laterable lib.fixpoint.
From iris.proofmode Require Import proofmode environments.
From iris_automation Require Import proofmode_base.

Set Default Proof Using "Type".


Global Instance unit_funs_ne {PROP : bi} (F : unit  PROP) : NonExpansive F.
Proof. move => n1 [] [] //. Qed.


Section greatest_fixpoint_lemmas.
  (* some lemmas that were elucidating to me, about how greatest_fixpoints behave logically *)
  Context {PROP : bi}.

  Section general_ofe.
    Context {A : ofe}.
    Implicit Types a : A.

    Lemma greatest_fixpoint_strong_mono' (F G : (A  PROP)  (A  PROP)) :
      BiMonoPred F 
       ( Φ x, F Φ x - G Φ x) -
       x, bi_greatest_fixpoint F x - bi_greatest_fixpoint G x.
    Proof.
      iIntros (HF) "#Hmon". iApply greatest_fixpoint_coiter.
      iIntros "!>" (y) "IH". rewrite greatest_fixpoint_unfold.
      by iApply "Hmon".
    Qed.

    Lemma bi_gfp_strong (F : (A  PROP)  (A  PROP)) R a :
      BiMonoPred F 
      R  bi_greatest_fixpoint F a
         bi_greatest_fixpoint (λ P u, R  F (λ u', R - P u') u) a.
    Proof.
      move => HF. iRevert (a).
      iApply greatest_fixpoint_coiter; first solve_proper.
      iIntros "!>" (a) "[$ HF]".
      rewrite {1}greatest_fixpoint_unfold.
      iRevert "HF".
      iRevert (a).
      destruct HF.
      iApply bi_mono_pred; first solve_proper.
      iIntros "!>" (x) "$ $".
    Qed.
  End general_ofe.

  Section unit_ofe.
    (* one would expect a similar result would hold for general A, but I got into trouble proving this:
       we seem to need that some functions of which we have too little information are NonExpansive.
       This follows trivially for A = unit, see unit_funs_ne *)
    Lemma bi_gfp_strong_subtract (F : (()  PROP)  (()  PROP)) R :
      BiMonoPred F 
      bi_greatest_fixpoint (λ P u, R - F (λ u', R  P u') u) ()
         R - bi_greatest_fixpoint F ().
    Proof.
      iIntros (HF) "HF HR".
      iCombine "HR HF" as "HF".
      erewrite bi_gfp_strong.
      iRevert "HF".
      generalize () => u.
      iRevert (u).
      iApply greatest_fixpoint_strong_mono'; last first.
      iIntros "!>" (Φ u) "[HR HFR]".
      iSpecialize ("HFR" with "HR").
      iRevert "HFR". iRevert (u).
      destruct HF.
      iApply bi_mono_pred.
      iIntros "!>" (x) "[HR HΦR]".
      by iApply "HΦR".
      all: split; try iSolveTC.
      - move => Φ Ψ _ _.
        iIntros "#HΦΨ" (x) "[$ HF] HR".
        iSpecialize ("HF" with "HR").
        iRevert "HF". iRevert (x).
        destruct HF.
        iApply bi_mono_pred.
        iIntros "!>" (x) "[$ HF] HR".
        iApply "HΦΨ".
        by iApply "HF".
      - move => Φ Ψ _ _.
        iIntros "#HΦΨ" (x) "HF HR".
        iSpecialize ("HF" with "HR").
        iRevert "HF". iRevert (x).
        destruct HF.
        iApply bi_mono_pred.
        iIntros "!>" (x) "[$ HF]".
        by iApply "HΦΨ".
    Qed.
  End unit_ofe.

End greatest_fixpoint_lemmas.


Section glp_lemmas.
  Context {PROP : bi}.

  (* lazy sealing :o *)
  Definition greatest_laterable_fixpoint_wrt (F : PROP  PROP) (R : PROP) : PROP :=
    R - bi_greatest_fixpoint (λ P _, F $ P ()) ().

  Lemma greatest_laterable_fixpoint_wrt_eq : greatest_laterable_fixpoint_wrt = (λ F R, R - bi_greatest_fixpoint (λ P _, F $ P ()) ())%I.
  Proof. reflexivity. Qed.

  Global Instance glfp_proper (F : PROP  PROP) : Proper (() ==> ()) (greatest_laterable_fixpoint_wrt F).
  Proof. solve_proper. Qed.

  Lemma greatest_laterable_fixpoint_wand F P R P' :
    IntoLaterable P P' 
    greatest_laterable_fixpoint_wrt F (R  P')  P - greatest_laterable_fixpoint_wrt F R.
  Proof.
    rewrite /greatest_laterable_fixpoint_wrt => HPP.
    iIntros "HF HP HR".
    iApply "HF". iFrame; iStopProof. apply HPP.
  Qed.

  Lemma run_greatest_laterable_fixpoint F R :
     (R - F R)  greatest_laterable_fixpoint_wrt F R.
  Proof.
    rewrite /greatest_laterable_fixpoint_wrt.
    iIntros "#HF HR".
    iApply (greatest_fixpoint_coiter _ (λ _, R)); last iFrame.
    by iIntros "!>" ([]).
  Qed.

  (* the strategy for automation is now basically: absorb all spatial hypothesis into the argument,
      latering them if necessary, then use run_greatest_..., introduce the □ modality (this is okay,
     since the spatial environment is now empty), then reintroduce all our hypotheses *)

  (* use MergeMod to accomplish this *)

131
132
133
  Global Instance glfp_as_solve_goal F (P : PROP) M :
    IntroducableModality M 
    AsSolveGoal M (greatest_laterable_fixpoint_wrt F P)%I (MergeMod (greatest_laterable_fixpoint_wrt F) P).
134
  Proof. unseal_diaframe; rewrite /AsSolveGoal. eauto. Qed.
Ike Mulder's avatar
Ike Mulder committed
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151

  (* how to eliminate this 'modality'? First, absorb all spatial hypotheses *)

  Global Instance make_laterable_re_intro P' F : ModReIntro (greatest_laterable_fixpoint_wrt F) 
    (λ p P R R', TCAnd (TCEq p false) $ 
                 TCAnd (IntoLaterable P P') $
                        MakeSep P' R R')%I.
  Proof.
    move => p P R R' [-> [HPP HPR]] /=.
    rewrite /MakeSep in HPR.
    rewrite -HPR.
    rewrite comm.
    by apply greatest_laterable_fixpoint_wand.
  Qed.

  (* finally, when the environment is empty, mark the 'modality' as introducable *)

152
153
  (* This should be able to be improved, to require less proof steps: just put only the non-Laterable things in the argument P.
    However, my initial attempts failed. This is because the order matters in which things are put into the goal,
Ike Mulder's avatar
Ike Mulder committed
154
        < order matters because we don't make progress on (∀ a, H) ⊢ (∀ a, H) ∗ R >
155
156
    and the current approach keeps the order currently found in the environment, which seems to be okay. 
    Maybe we need a MakeSep which determines heuristically which goals should be put on the RHS? *)
Ike Mulder's avatar
Ike Mulder committed
157
158
159
  Global Instance intuitionistically_introducable Δ F P :
    TCEq (env_spatial Δ) Enil  IntroducableInAs (PROP := PROP) (greatest_laterable_fixpoint_wrt F) P Δ (IntroduceHyp P (F P))  | 30.
  Proof.
160
    unseal_diaframe; rewrite /IntroducableInAs => HM.
Ike Mulder's avatar
Ike Mulder committed
161
162
163
164
165
166
167
168
169
170
171
172
    rewrite envs_entails_eq.
    rewrite {2}env_spatial_is_nil_intuitionistically; last rewrite /env_spatial_is_nil HM //.
    move => -> //.
    apply run_greatest_laterable_fixpoint.
  Qed.
End glp_lemmas.


Global Opaque greatest_laterable_fixpoint_wrt.