hoare_lifting.v 5.71 KB
Newer Older
1 2
From program_logic Require Export hoare lifting.
From program_logic Require Import ownership.
3
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

5 6
Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
  (default True%I ef (λ e, ht E P e Φ))
7 8
  (at level 20, P, ef, Φ at level 200,
   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : uPred_scope.
9 10
Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
  (True  default True ef (λ e, ht E P e Φ))
11 12
  (at level 20, P, ef, Φ at level 200,
   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14

Section lifting.
15 16
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
17 18
Implicit Types P Q R : iProp Λ Σ.
Implicit Types Ψ : val Λ  iProp Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20

Lemma ht_lift_step E1 E2
21
    (φ : expr Λ  state Λ  option (expr Λ)  Prop) P P' Φ1 Φ2 Ψ e1 σ1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  E1  E2  to_val e1 = None 
23
  reducible e1 σ1 
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  φ e2 σ2 ef) 
25
  ((P ={E2,E1}=> ownP σ1   P')   e2 σ2 ef,
26 27 28 29
    ( φ e2 σ2 ef  ownP σ2  P' ={E1,E2}=> Φ1 e2 σ2 ef  Φ2 e2 σ2 ef) 
    {{ Φ1 e2 σ2 ef }} e2 @ E2 {{ Ψ }} 
    {{ Φ2 e2 σ2 ef }} ef ?@  {{ λ _, True }})
   {{ P }} e1 @ E2 {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Proof.
31
  intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
32
  rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
34
  rewrite always_and_sep_r -assoc; apply sep_mono; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36
  rewrite (later_intro ( _, _)) -later_sep; apply later_mono.
  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
37
  rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
38
  apply wand_intro_l; rewrite !always_and_sep_l.
39
  rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
  rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
  rewrite pvs_frame_r; apply pvs_mono.
42
  rewrite (comm _ (Φ1 _ _ _)) -assoc (assoc _ (Φ1 _ _ _)).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
44
  rewrite assoc (comm _ _ (wp _ _ _)) -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46 47 48 49
  apply sep_mono; first done.
  destruct ef as [e'|]; simpl; [|by apply const_intro].
  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
  by apply const_intro.
Qed.
50

51 52
Lemma ht_lift_atomic_step
    E (φ : expr Λ  state Λ  option (expr Λ)  Prop) P e1 σ1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
53
  atomic e1 
54
  reducible e1 σ1 
Robbert Krebbers's avatar
Robbert Krebbers committed
55
  ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  φ e2 σ2 ef) 
56
  ( e2 σ2 ef, {{  φ e2 σ2 ef  P }} ef ?@  {{ λ _, True }}) 
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58 59 60 61 62
  {{ ownP σ1   P }} e1 @ E {{ λ v,  σ2 ef, ownP σ2   φ (of_val v) σ2 ef }}.
Proof.
  intros ? Hsafe Hstep; set (φ' e σ ef := is_Some (to_val e)  φ e σ ef).
  rewrite -(ht_lift_step E E φ'  _ P
    (λ e2 σ2 ef, ownP σ2   (φ' e2 σ2 ef))%I
    (λ e2 σ2 ef,  φ e2 σ2 ef  P)%I);
63
    try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
65
  apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  apply and_intro; [|apply and_intro; [|done]].
67 68
  - rewrite -vs_impl; apply: always_intro. apply impl_intro_l.
    rewrite and_elim_l !assoc; apply sep_mono; last done.
69
    rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??].
Robbert Krebbers's avatar
Robbert Krebbers committed
70
    by repeat apply and_intro; try apply const_intro.
71
  - apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
72
    rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?].
73
    rewrite -(of_to_val e2 v) // -wp_value'; [].
74
    rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
75
    by rewrite -always_and_sep_r; apply and_intro; try apply const_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
77

78
Lemma ht_lift_pure_step E (φ : expr Λ  option (expr Λ)  Prop) P P' Ψ e1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  to_val e1 = None 
80
  ( σ1, reducible e1 σ1) 
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
  ( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  σ1 = σ2  φ e2 ef) 
  ( e2 ef,
83
    {{  φ e2 ef  P }} e2 @ E {{ Ψ }} 
84
    {{  φ e2 ef  P' }} ef ?@  {{ λ _, True }})
85
   {{ (P  P') }} e1 @ E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Proof.
87
  intros ? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
88 89 90
  rewrite -(wp_lift_pure_step E φ _ e1) //.
  rewrite (later_intro ( _, _)) -later_and; apply later_mono.
  apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
91
  rewrite (forall_elim e2) (forall_elim ef).
92
  rewrite always_and_sep_l !always_and_sep_r {1}(always_sep_dup ( _)).
93 94 95 96
  rewrite {1}(assoc _ (_  _)%I) -(assoc _ ( _)%I).
  rewrite (assoc _ ( _)%I P) -{1}(comm _ P) -(assoc _ P).
  rewrite (assoc _ ( _)%I) assoc -(assoc _ ( _  P))%I.
  rewrite (comm _ ( _  P'))%I assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
98
  rewrite -assoc; apply sep_mono; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100 101 102
  destruct ef as [e'|]; simpl; [|by apply const_intro].
  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
  by apply const_intro.
Qed.
103

104
Lemma ht_lift_pure_det_step
105
    E (φ : expr Λ  option (expr Λ)  Prop) P P' Ψ e1 e2 ef :
Robbert Krebbers's avatar
Robbert Krebbers committed
106
  to_val e1 = None 
107
  ( σ1, reducible e1 σ1) 
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  ( σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef'  σ1 = σ2  e2 = e2'  ef = ef')
109 110
  ({{ P }} e2 @ E {{ Ψ }}  {{ P' }} ef ?@  {{ λ _, True }})
   {{ (P  P') }} e1 @ E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
111 112 113 114
Proof.
  intros ? Hsafe Hdet.
  rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2'  ef = ef')); eauto.
  apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono.
115
  - apply: always_intro. apply impl_intro_l.
116
    rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
    by rewrite /ht always_elim impl_elim_r.
118
  - destruct ef' as [e'|]; simpl; [|by apply const_intro].
119
    apply: always_intro. apply impl_intro_l.
120
    rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122
    by rewrite /= /ht always_elim impl_elim_r.
Qed.
123

Robbert Krebbers's avatar
Robbert Krebbers committed
124
End lifting.