pure.v 1.92 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris.program_logic Require Import lifting language ectx_language.
3
4
Set Default Proof Using "Type".

5
6
7
8
9
Section pure_language.
Context `{irisG Λ Σ}.
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types φ : Prop.
Implicit Types e : expr Λ.
10

11
Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
12
  pure_exec_safe : 
13
    P ->  σ, language.reducible e1 σ;
14
  pure_exec_puredet : 
15
    P ->  σ1 e2' σ2 efs, language.prim_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs;
16
17
  }.

18
Lemma wp_pure `{Inhabited (state Λ)} E E' e1 e2 φ Φ :
19
20
  PureExec φ e1 e2 
  φ 
21
  (|={E,E'}=> WP e2 @ E {{ Φ }})  WP e1 @ E {{ Φ }}.
22
23
Proof.
  iIntros (? Hφ) "HWP".
24
  iApply (wp_lift_pure_det_step with "[HWP]").
25
26
  { apply (pure_exec_safe Hφ). }
  { apply (pure_exec_puredet Hφ). }
27
  rewrite big_sepL_nil right_id //.
28
29
Qed.

30
Lemma wp_pure' `{Inhabited (state Λ)} E e1 e2 φ Φ :
31
32
  PureExec φ e1 e2 
  φ 
33
  ( WP e2 @ E {{ Φ }})  WP e1 @ E {{ Φ }}.
34
35
36
37
38
39
Proof. 
  intros ? ?.
  rewrite -wp_pure //.
  rewrite -step_fupd_intro //.
Qed.

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
Lemma hoist_pred_pureexec (P : Prop) (e1 e2 : expr Λ) :
  (P  PureExec True e1 e2) 
  PureExec P e1 e2.
Proof.
  intros HPE.
  split; intros HP; destruct (HPE HP); eauto.
Qed.

End pure_language.

Section pure_ectx_language.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.

Lemma det_head_step_pureexec (e1 e2 : expr) :
  ( σ, head_reducible e1 σ) 
  ( σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs) 
  PureExec True e1 e2.
Proof.
  intros Hp1 Hp2.
  split; intros _.
  - intros σ. destruct (Hp1 σ) as (? & ? & ? & ?).
    do 3 eexists. simpl.
    eapply (Ectx_step _ _ _ _ _ empty_ectx); eauto using fill_empty.
  - move => σ1 e2' σ2 efs /=.
    intros ?%head_reducible_prim_step; eauto.
Qed.

End pure_ectx_language.