fundamental.v 11.7 KB
Newer Older
1
2
3
4
5
6
7
8
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import F_mu_ref.lang F_mu_ref.typing F_mu_ref.rules F_mu_ref.logrel.
From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Amin Timany's avatar
Amin Timany committed
9
Require Import prelude.Vlist.
10
11
12
13
14
15
16
17
18
19
20
Import uPred.

Section typed_interp.
  Context
    {Σ : gFunctors}
    `{i : heapG Σ}
    `{L : namespace}.
  
  Implicit Types P Q R : iPropG lang Σ.
  Notation "# v" := (of_val v) (at level 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
  Local Ltac ipropsimpl :=
    repeat
      match goal with
      | [|- (_  (_  _))%I] => eapply and_intro
      | [|- ( _   _)%I] => apply later_mono
      | [|- (_   _, _)%I] => rewrite -exist_intro
      | [|- (( _, _)  _)%I] => let v := fresh "v" in rewrite exist_elim; [|intros v]
      end.

  Local Hint Extern 1 => progress ipropsimpl.

  Local Tactic Notation "smart_wp_bind" uconstr(ctx) uconstr(t) ident(v) :=
    rewrite -(@wp_bind _ _ _ [ctx]) /= -wp_impl_l; apply and_intro; [
    apply (@always_intro _ _ _ t), forall_intro=> v /=; apply impl_intro_l| eauto with itauto].

  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) :=
    rewrite -(@wp_bind _ _ _ [ctx]) /= -wp_mono; eauto; intros v; cbn.

  Create HintDb itauto.

  Local Hint Extern 3 ((_  _)  _)%I => rewrite and_elim_r : itauto.
  Local Hint Extern 3 ((_  _)  _)%I => rewrite and_elim_l : itauto.
  Local Hint Extern 3 (_  (_  _))%I => rewrite -or_intro_l : itauto.
  Local Hint Extern 3 (_  (_  _))%I => rewrite -or_intro_r : itauto.
  Local Hint Extern 2 (_   _)%I => etransitivity; [|rewrite -later_intro] : itauto.
  
  Local Ltac value_case := rewrite -wp_value/= ?to_of_val //; auto 2.
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
*)

  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
        _ : ?A, _) => let W := fresh "W" in evar (W : A); iExists W; unfold W; clear W
  end : itauto.

  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
        _) => iNext
  end : itauto.

  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
       (_  _)) => iSplit
  end : itauto.
  
  
  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
    iApply (@wp_bind _ _ _ [ctx]);
    iApply wp_impl_l;
    iSplit; [| iApply Hp; trivial];
    [apply (always_intro _ _); iIntros {v} Hv|iSplit; trivial]; cbn.
              
  Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.

  Lemma later_exist_turnstile (M : cmraT) (A : Type) :
    Inhabited A   Φ : A  uPred M, ( ( a : A, Φ a))%I  ( a : A,  Φ a)%I.
  Proof. intros H Φ. rewrite later_exist; trivial. Qed.
87
88
89
90
91
92
93

  Lemma typed_interp N k Δ Γ vs e τ
        (HNLdisj :  l : loc, N  L .@ l)
        (Htyped : typed k Γ e τ)
        (Hctx : closed_ctx k Γ)
        (HC : closed_type k τ)
        (HΔ : VlistAlwaysStable Δ)
94
    : List.length Γ = List.length vs 
95
96
97
98
      (heap_ctx N  Π∧ zip_with (λ τ v, (@interp Σ i L) k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I 
                  WP (e.[env_subst vs]) @  {{ λ v, (@interp Σ i L) k τ HC Δ v }}.
  Proof.
    revert Hctx HC HΔ vs.
99
    induction Htyped; intros Hctx HC HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
100
101
102
    - (* var *)
      destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
      { by rewrite -Hlen; apply lookup_lt_Some with τ. }
103
      rewrite /env_subst Hv; value_case.
104
      edestruct (zipwith_Forall_lookup _ Hctx) as [Hτ' Hτ'eq]; eauto.
105
106
107
      iApply interp_closed_irrel_turnstile.
      iApply big_and_elem_of "HΓ"; eauto.
      apply elem_of_list_lookup_2 with x.
108
109
110
      rewrite lookup_zip_with; simplify_option_eq; trivial.
    - (* unit *) value_case.
    - (* pair *)
111
112
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
113
114
      value_case; eauto 10 with itauto.
    - (* fst *)
115
116
117
118
119
      smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
      iApply double_exists; [|trivial].
      intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
      iApply wp_fst; eauto using to_of_val; cbn.
      iNext; iApply interp_closed_irrel_turnstile; trivial.
120
    - (* snd *)
121
122
123
124
125
126
127
128
129
130
131
      smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
      iApply double_exists; [|trivial].
      intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
      iApply wp_snd; eauto using to_of_val; cbn.
      iNext; iApply interp_closed_irrel_turnstile; trivial.
    - (* injl *)
      smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
      value_case; iLeft; auto with itauto.
    - (* injr *)
      smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn.
      value_case; iRight; auto with itauto.
132
    - (* case *)
133
134
135
136
137
138
139
140
141
142
143
144
145
      smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
      iDestruct "Hv" as "[Hv|Hv]"; eauto; iRevert "HΓ"; iRevert "Hheap";
        iApply exist_elim; eauto; cbn;
          iIntros {w} "#[% Hw2] #HΓ #Hheap"; rewrite H; cbn;
            [iApply wp_case_inl|iApply wp_case_inr];
            auto 1 using to_of_val;
            asimpl;
            [specialize (IHHtyped2 Δ (typed_closed_ctx _ _ _ _ Htyped2) HC HΔ (w::vs)) |
             specialize (IHHtyped3 Δ (typed_closed_ctx _ _ _ _ Htyped3) HC HΔ (w::vs))];
              erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
                [iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto;
                  (iSplit; [trivial|iSplit]; [iApply interp_closed_irrel_turnstile|
                            iApply type_context_closed_irrel_turnstile]; trivial).
146
    - (* lam *)
147
148
149
150
151
152
153
      value_case; apply (always_intro _ _); iIntros {w} "#Hw".
      iApply wp_lam; auto 1 using to_of_val.
      asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
      iNext; iApply (IHHtyped Δ (typed_closed_ctx _ _ _ _ Htyped) (closed_type_arrow_2 HC)
                              HΔ (w :: vs)); cbn; auto.
      (iSplit; [trivial|iSplit]; [iApply interp_closed_irrel_turnstile|
                iApply type_context_closed_irrel_turnstile]; trivial).
154
    - (* app *)
155
156
157
158
      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
      smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
      iApply wp_mono; [|iApply "Hv"; auto with itauto].
      intros; apply interp_closed_irrel_turnstile.
159
    - (* TLam *)
160
161
162
163
164
165
166
167
168
      value_case; iApply exist_intro; iSplit; trivial.
      iIntros {τi}; destruct τi as [τi τiPr].
      iRevert "Hheap".
      iPoseProof always_intro "HΓ" as "HP"; try typeclasses eauto;
        try (iApply always_impl; iExact "HP").
      iIntros "#HΓ #Hheap"; iNext.
      iApply IHHtyped; [rewrite map_length|]; trivial.
      iSplit; trivial.
      iRevert "HΓ". rewrite zip_with_closed_ctx_list_subst. iIntros "#HΓ"; trivial.
169
    - (* TApp *)
170
171
172
173
174
175
176
177
178
      smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
      iApply exist_elim; [|iExact "Hv"]; cbn.
      iIntros {e'} "[% #He']"; rewrite H0.
      iApply wp_TLam.
      iSpecialize "He'" {((interp k τ' H Δ)  _)}; cbn.
      iApply always_elim. iApply always_mono; [|trivial].
      iIntros "He'"; iNext.
      iApply wp_mono; [|trivial].
      intros w; cbn; rewrite -interp_subst; trivial.
179
180
    - (* Fold *)
      rewrite map_length in IHHtyped.
181
182
183
184
185
186
187
188
189
190
191
192
193
194
      iApply (@wp_bind _ _ _ [FoldCtx]);
        iApply wp_impl_l;
        iSplit; [eapply (@always_intro _ _ _ _)|
                 iApply (IHHtyped _ _ (closed_type_rec HC)); trivial]; cbn.
      + iIntros {v} "#Hv".
        value_case. rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
        eapply (@always_intro _ _ _ _).
        iApply exist_intro; iSplit; trivial.
        iNext.
        change (fixpoint (interp_rec_pre
                            (Vlist_cons_apply Δ (interp (S k) τ (closed_type_rec HC)))))
        with ((@interp _ _ L k (TRec τ) HC) Δ); trivial.
      + iRevert "HΓ"; rewrite zip_with_closed_ctx_list_subst; iIntros "#HΓ";
          iSplit; trivial.
195
    - (* Unfold *)
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
      iApply (@wp_bind _ _ _ [UnfoldCtx]);
        iApply wp_impl_l;
        iSplit; [eapply (@always_intro _ _ _ _)|
                 iApply (IHHtyped _ _ (typed_closed_type _ _ _ _ Htyped)); trivial];
        [|iSplit; trivial]; cbn.
      iIntros {v}.
      rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
      iIntros "#Hv".
      iApply exist_elim; [|iAssumption].
      iIntros {w}; cbn.
      change (fixpoint (interp_rec_pre
                          (Vlist_cons_apply
                             Δ
                             (interp
                                (S k) τ
                                (closed_type_rec
                                   (typed_closed_type k Γ e (TRec τ) Htyped))))))
      with ((@interp _ _ L k (TRec τ) (typed_closed_type k Γ e (TRec τ) Htyped)) Δ);
        trivial.
      iIntros "[% #Hw]"; rewrite H.
      iApply wp_Fold; cbn; auto using to_of_val.
      iRevert "Hw". rewrite -interp_subst. iIntros "#Hw". trivial.
218
    - (* Alloc *)
219
220
221
222
223
224
225
226
227
228
229
230
      smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
      iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
      iApply pvs_intro.
      iApply wp_alloc; [| | | |iSplit;[iExact "Hheap"|iExact "Hv"]];
        [|iIntros "#[Hheap Hv]"| |]; auto using to_of_val.
      iIntros "#[Hheap Hv]". iNext.
      iIntros {l} "Hl".
      iApply exist_intro.
      iApply and_intro; [| trivial |]; auto.
      iApply inv_alloc; trivial. iNext.
      iApply exist_intro.
      iSplit; trivial.
231
    - (* Load *)
232
233
234
235
236
237
238
239
240
241
242
243
244
245
      smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
      iRevert "Hheap". iApply exist_elim; [|iExact "Hv"].
      iIntros {l} "[% #Hv] #Hheap"; rewrite H.
      iApply wp_atomic; cbn; eauto using to_of_val.
      iApply wp_inv; [auto using to_of_val| trivial
                      | apply and_elim_r | apply and_elim_l | ].
      iApply pvs_intro. iSplit; trivial.
      iIntros "Hl".
      iPoseProof later_exist_turnstile "Hl" as "Hl'"; [typeclasses eauto|].
      iRevert "Hheap".
      iApply exist_elim; [|iExact "Hl'"].
      iIntros {w} "[Hl1 #Hl2] #Hheap".
      iApply (wp_load _ _ _ 1);
        [apply and_elim_r| trivial | apply and_elim_l | iSplit; trivial].
246
      specialize (HNLdisj l); set_solver_ndisj.
247
248
249
250
251
252
      iNext.
      iSplitL; trivial.
      iIntros "Hl".
      iSplitL.
      + iNext. iApply exist_intro; iSplitL; trivial.
      + iApply pvs_intro; iApply interp_closed_irrel_turnstile; trivial.
253
    - (* Store *)
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
      smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
      smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ".
      iRevert "Hheap Hw". iApply exist_elim; [|iExact "Hv"].
      iIntros {l} "#[% Hl] #Hheap #Hw"; rewrite H.
      iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |].
      iApply wp_inv; [cbn; rewrite ?to_of_val; auto| trivial
                      | apply and_elim_r | apply and_elim_l | ].
      iApply pvs_intro. iSplit; trivial.
      iClear "Hl". iIntros "Hl".
      iPoseProof later_exist_turnstile "Hl" as "Hl'"; [typeclasses eauto|].
      iRevert "Hheap Hw".
      iApply exist_elim; [|iExact "Hl'"].
      iIntros {u} "[Hl1 #Hl2] #Hheap #Hw".
      iApply wp_store;
        [rewrite to_of_val; trivial | apply and_elim_r
         | | apply and_elim_l | iSplit; trivial]. 
270
      specialize (HNLdisj l); set_solver_ndisj.
271
272
273
274
275
      iSplitL; trivial.
      iNext. iIntros "Hl".
      iSplitL; [|iApply pvs_intro; trivial].
      iNext. iApply exist_intro; iSplitL; trivial.
      iApply interp_closed_irrel_turnstile; trivial.
276
277
      (* unshelving *)
      Unshelve.
278
279
      all: cbn; solve [eauto 2 using closed_ctx_map_S_back,
                       typed_closed_type | try typeclasses eauto].
280
281
282
  Qed.
  
End typed_interp.