Commit cf888992 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Misc tweaking of consistency of coding style.

parent ef7ea67f
Require Import prelude.gmap program_logic.lifting.
Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
Import uPred.
Import heap_lang.
Import uPred heap_lang.
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
Section lifting.
......@@ -9,6 +8,7 @@ Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val iProp heap_lang Σ.
Implicit Types K : ectx.
Implicit Types ef : option expr.
(** Bind. *)
Lemma wp_bind {E e} K Q :
......@@ -26,7 +26,8 @@ Lemma wp_alloc_pst E σ e v Q :
wp E (Alloc e) Q.
Proof.
(* TODO RJ: This works around ssreflect bug #22. *)
intros. set (φ v' σ' ef := l, ef = @None expr v' = LocV l σ' = <[l:=v]>σ σ !! l = None).
intros. set (φ v' σ' ef := l,
ef = None v' = LocV l σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
last by intros; inv_step; eauto 8.
apply sep_mono, later_mono; first done.
......@@ -41,24 +42,23 @@ Lemma wp_load_pst E σ l v Q :
σ !! l = Some v
(ownP σ (ownP σ - Q v)) wp E (Load (Loc l)) Q.
Proof.
intros; rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
last (by intros; inv_step; eauto).
intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
last by intros; inv_step; eauto using to_of_val.
Qed.
Lemma wp_store_pst E σ l e v v' Q :
to_val e = Some v σ !! l = Some v'
(ownP σ (ownP (<[l:=v]>σ) - Q LitUnitV)) wp E (Store (Loc l) e) Q.
Proof.
intros.
rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ) None) ?right_id //;
last by intros; inv_step; eauto.
intros. rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ) None)
?right_id //; last by intros; inv_step; eauto.
Qed.
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v' v' v1
(ownP σ (ownP σ - Q LitFalseV)) wp E (Cas (Loc l) e1 e2) Q.
Proof.
intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ None) ?right_id //;
intros. rewrite -(wp_lift_atomic_det_step σ LitFalseV σ None) ?right_id //;
last by intros; inv_step; eauto.
Qed.
......@@ -66,9 +66,8 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v1
(ownP σ (ownP (<[l:=v2]>σ) - Q LitTrueV)) wp E (Cas (Loc l) e1 e2) Q.
Proof.
intros.
rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ) None) ?right_id //;
last by intros; inv_step; eauto.
intros. rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ) None)
?right_id //; last by intros; inv_step; eauto.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
......@@ -81,20 +80,19 @@ Proof.
by rewrite -(wp_value' _ _ LitUnit) //; apply const_intro.
Qed.
Lemma wp_rec E ef e v Q :
Lemma wp_rec E erec e v Q :
to_val e = Some v
wp E ef.[Rec ef, e /] Q wp E (App (Rec ef) e) Q.
wp E erec.[Rec erec, e /] Q wp E (App (Rec erec) e) Q.
Proof.
intros; rewrite -(wp_lift_pure_det_step (App _ _) ef.[Rec ef, e /] None)
?right_id //=;
last by intros; inv_step; eauto.
intros. rewrite -(wp_lift_pure_det_step (App _ _) erec.[Rec erec, e /] None)
?right_id //=; last by intros; inv_step; eauto.
Qed.
Lemma wp_plus E n1 n2 Q :
Q (LitNatV (n1 + n2)) wp E (Plus (LitNat n1) (LitNat n2)) Q.
Proof.
rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2)) None) ?right_id //;
last by intros; inv_step; eauto.
rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2)) None)
?right_id //; last by intros; inv_step; eauto.
by rewrite -wp_value'.
Qed.
......@@ -102,7 +100,7 @@ Lemma wp_le_true E n1 n2 Q :
n1 n2
Q LitTrueV wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof.
intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
intros. rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
last by intros; inv_step; eauto with omega.
by rewrite -wp_value'.
Qed.
......@@ -111,7 +109,7 @@ Lemma wp_le_false E n1 n2 Q :
n1 > n2
Q LitFalseV wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof.
intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
intros. rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
last by intros; inv_step; eauto with omega.
by rewrite -wp_value'.
Qed.
......@@ -120,7 +118,7 @@ Lemma wp_fst E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2
Q v1 wp E (Fst (Pair e1 e2)) Q.
Proof.
intros; rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
last by intros; inv_step; eauto.
by rewrite -wp_value'.
Qed.
......@@ -129,7 +127,7 @@ Lemma wp_snd E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2
Q v2 wp E (Snd (Pair e1 e2)) Q.
Proof.
intros; rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
last by intros; inv_step; eauto.
by rewrite -wp_value'.
Qed.
......@@ -138,16 +136,16 @@ Lemma wp_case_inl E e0 v0 e1 e2 Q :
to_val e0 = Some v0
wp E e1.[e0/] Q wp E (Case (InjL e0) e1 e2) Q.
Proof.
intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/] None) ?right_id //;
last by intros; inv_step; eauto.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/] None)
?right_id //; last by intros; inv_step; eauto.
Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Q :
to_val e0 = Some v0
wp E e2.[e0/] Q wp E (Case (InjR e0) e1 e2) Q.
Proof.
intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/] None) ?right_id //;
last by intros; inv_step; eauto.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/] None)
?right_id //; last by intros; inv_step; eauto.
Qed.
(** Some derived stateless axioms *)
......
Require Export program_logic.hoare program_logic.lifting.
Import uPred.
Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
(default True%I ef (λ e, ht E P e Q))
......@@ -12,7 +13,6 @@ Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
Implicit Types P : iProp Λ Σ.
Implicit Types R : val Λ iProp Λ Σ.
Import uPred.
Lemma ht_lift_step E1 E2
(φ : expr Λ state Λ option (expr Λ) Prop) P P' Q1 Q2 R e1 σ1 :
......
......@@ -14,13 +14,15 @@ Implicit Types σ : state Λ.
Implicit Types Q : val Λ iProp Λ Σ.
Transparent uPred_holds.
Notation wp_fork ef := (default True ef (flip (wp coPset_all) (λ _, True)))%I.
Lemma wp_lift_step E1 E2
(φ : expr Λ state Λ option (expr Λ) Prop) Q e1 σ1 :
E1 E2 to_val e1 = None
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
pvs E2 E1 (ownP σ1 e2 σ2 ef, ( φ e2 σ2 ef ownP σ2) -
pvs E1 E2 (wp E2 e2 Q default True ef (flip (wp coPset_all) (λ _, True))))
pvs E2 E1 (ownP σ1 e2 σ2 ef,
( φ e2 σ2 ef ownP σ2) - pvs E1 E2 (wp E2 e2 Q wp_fork ef))
wp E2 e1 Q.
Proof.
intros ? He Hsafe Hstep r n ? Hvs; constructor; auto.
......@@ -41,9 +43,7 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 :
to_val e1 = None
( σ1, reducible e1 σ1)
( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
( e2 ef, φ e2 ef
wp E e2 Q default True ef (flip (wp coPset_all) (λ _, True)))
wp E e1 Q.
( e2 ef, φ e2 ef wp E e2 Q wp_fork ef) wp E e1 Q.
Proof.
intros He Hsafe Hstep r [|n] ?; [done|]; intros Hwp; constructor; auto.
intros rf k Ef σ1 ???; split; [done|].
......@@ -56,17 +56,17 @@ Qed.
Opaque uPred_holds.
Import uPred.
Lemma wp_lift_atomic_step {E Q} e1 (φ : val Λ state Λ option (expr Λ) Prop) σ1 :
Lemma wp_lift_atomic_step {E Q} e1
(φ : val Λ state Λ option (expr Λ) Prop) σ1 :
to_val e1 = None
reducible e1 σ1
( e' σ' ef, prim_step e1 σ1 e' σ' ef v', to_val e' = Some v' φ v' σ' ef)
(ownP σ1 v2 σ2 ef, φ v2 σ2 ef ownP σ2 -
Q v2 default True ef (flip (wp coPset_all) (λ _, True)))
wp E e1 Q.
( e2 σ2 ef,
prim_step e1 σ1 e2 σ2 ef v2, to_val e2 = Some v2 φ v2 σ2 ef)
(ownP σ1 v2 σ2 ef, φ v2 σ2 ef ownP σ2 - Q v2 wp_fork ef)
wp E e1 Q.
Proof.
intros He Hsafe Hstep.
rewrite -(wp_lift_step E E
(λ e' σ' ef, v', to_val e' = Some v' φ v' σ' ef) _ e1 σ1) //; [].
intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, v2,
to_val e2 = Some v2 φ v2 σ2 ef) _ e1 σ1) //; [].
rewrite -pvs_intro. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'.
apply forall_intro=>ef; apply wand_intro_l.
......@@ -80,33 +80,29 @@ Qed.
Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :
to_val e1 = None
reducible e1 σ1
( e' σ' ef', prim_step e1 σ1 e' σ' ef' ef' = ef e' = of_val v2 σ' = σ2)
(ownP σ1 (ownP σ2 - Q v2
default True ef (flip (wp coPset_all) (λ _, True))))
wp E e1 Q.
( e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef'
σ2 = σ2' to_val e2' = Some v2 ef = ef')
(ownP σ1 (ownP σ2 - Q v2 wp_fork ef)) wp E e1 Q.
Proof.
intros He Hsafe Hstep.
rewrite -(wp_lift_atomic_step _ (λ v' σ' ef', v' = v2 σ' = σ2 ef' = ef) σ1) //;
last first.
{ intros. exists v2. apply Hstep in H. destruct_conjs; subst.
eauto using to_of_val. }
intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef',
σ2 = σ2' v2 = v2' ef = ef') σ1) //; last naive_solver.
apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
apply wand_intro_l.
rewrite always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[-> [-> ->]] /=.
by rewrite wand_elim_r.
apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r.
Qed.
Lemma wp_lift_pure_det_step {E Q} e1 e2 ef :
to_val e1 = None
( σ1, reducible e1 σ1)
( σ1 e' σ' ef', prim_step e1 σ1 e' σ' ef' σ1 = σ' ef' = ef e' = e2)
(wp E e2 Q default True ef (flip (wp coPset_all) (λ _, True))) wp E e1 Q.
( σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' σ1 = σ2 e2 = e2' ef = ef')
(wp E e2 Q wp_fork ef) wp E e1 Q.
Proof.
intros. rewrite -(wp_lift_pure_step E (λ e' ef', ef' = ef e' = e2) _ e1) //=.
intros.
rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ef = ef') _ e1) //=.
apply later_mono, forall_intro=>e'; apply forall_intro=>ef'.
apply impl_intro_l, const_elim_l=>-[-> ->] /=; done.
by apply impl_intro_l, const_elim_l=>-[-> ->].
Qed.
End lifting.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment