Commit 735dd18f authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

parents 9fc48e66 94ab527c
...@@ -23,21 +23,22 @@ Lemma wp_alloc_pst E σ e v Q : ...@@ -23,21 +23,22 @@ Lemma wp_alloc_pst E σ e v Q :
Proof. Proof.
(* TODO RJ: Without the set, ssreflect rewrite doesn't work. Figure out why or (* TODO RJ: Without the set, ssreflect rewrite doesn't work. Figure out why or
reprot a bug. *) reprot a bug. *)
intros. set (φ v' σ' := l, v' = LocV l σ' = <[l:=v]>σ σ !! l = None). intros. set (φ v' σ' ef := l, ef = @None expr v' = LocV l σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ; rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
last by intros; inv_step; eauto 8. last by intros; inv_step; eauto 8.
apply sep_mono, later_mono; first done. apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l. 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'. rewrite always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[l [-> [-> ?]]]. apply const_elim_l=>-[l [-> [-> [-> ?]]]].
by rewrite (forall_elim l) const_equiv // left_id wand_elim_r. by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
Qed. Qed.
Lemma wp_load_pst E σ l v Q : Lemma wp_load_pst E σ l v Q :
σ !! l = Some v σ !! l = Some v
(ownP σ (ownP σ - Q v)) wp E (Load (Loc l)) Q. (ownP σ (ownP σ - Q v)) wp E (Load (Loc l)) Q.
Proof. Proof.
intros; rewrite -(wp_lift_atomic_det_step σ v σ) //; intros; rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
last (by intros; inv_step; eauto). last (by intros; inv_step; eauto).
Qed. Qed.
...@@ -46,7 +47,7 @@ Lemma wp_store_pst E σ l e v v' Q : ...@@ -46,7 +47,7 @@ Lemma wp_store_pst E σ l e v v' Q :
(ownP σ (ownP (<[l:=v]>σ) - Q LitUnitV)) wp E (Store (Loc l) e) Q. (ownP σ (ownP (<[l:=v]>σ) - Q LitUnitV)) wp E (Store (Loc l) e) Q.
Proof. Proof.
intros. intros.
rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ)) //; rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ) None) ?right_id //;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
Qed. Qed.
...@@ -54,7 +55,7 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q : ...@@ -54,7 +55,7 @@ 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 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. (ownP σ (ownP σ - Q LitFalseV)) wp E (Cas (Loc l) e1 e2) Q.
Proof. Proof.
intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ) //; intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ None) ?right_id //;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
Qed. Qed.
...@@ -63,7 +64,7 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q : ...@@ -63,7 +64,7 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
(ownP σ (ownP (<[l:=v2]>σ) - Q LitTrueV)) wp E (Cas (Loc l) e1 e2) Q. (ownP σ (ownP (<[l:=v2]>σ) - Q LitTrueV)) wp E (Cas (Loc l) e1 e2) Q.
Proof. Proof.
intros. intros.
rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ)) //; rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ) None) ?right_id //;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
Qed. Qed.
...@@ -71,26 +72,25 @@ Qed. ...@@ -71,26 +72,25 @@ Qed.
Lemma wp_fork E e : Lemma wp_fork E e :
wp (Σ:=Σ) coPset_all e (λ _, True) wp E (Fork e) (λ v, (v = LitUnitV)). wp (Σ:=Σ) coPset_all e (λ _, True) wp E (Fork e) (λ v, (v = LitUnitV)).
Proof. Proof.
rewrite -(wp_lift_pure_step E (λ e' ef, e' = LitUnit ef = Some e)) //=; rewrite -(wp_lift_pure_det_step (Fork e) LitUnit (Some e)) //=;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
apply later_mono, forall_intro=>e2; apply forall_intro=>ef. apply later_mono, sep_intro_True_l; last done.
apply impl_intro_l, const_elim_l=>-[-> ->] /=. by rewrite -(wp_value' _ _ LitUnit) //; apply const_intro.
apply sep_intro_True_l; last done.
by rewrite -wp_value' //; apply const_intro.
Qed. Qed.
Lemma wp_rec E ef e v Q : Lemma wp_rec E ef e v Q :
to_val e = Some v to_val e = Some v
wp E ef.[Rec ef, e /] Q wp E (App (Rec ef) e) Q. wp E ef.[Rec ef, e /] Q wp E (App (Rec ef) e) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (App _ _) ef.[Rec ef, e /]) //=; intros; rewrite -(wp_lift_pure_det_step (App _ _) ef.[Rec ef, e /] None)
?right_id //=;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
Qed. Qed.
Lemma wp_plus E n1 n2 Q : Lemma wp_plus E n1 n2 Q :
Q (LitNatV (n1 + n2)) wp E (Plus (LitNat n1) (LitNat n2)) Q. Q (LitNatV (n1 + n2)) wp E (Plus (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2))) //=; rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2)) None) ?right_id //;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
...@@ -99,8 +99,8 @@ Lemma wp_le_true E n1 n2 Q : ...@@ -99,8 +99,8 @@ Lemma wp_le_true E n1 n2 Q :
n1 n2 n1 n2
Q LitTrueV wp E (Le (LitNat n1) (LitNat n2)) Q. Q LitTrueV wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue) //=; intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
last by intros; inv_step; eauto with lia. last by intros; inv_step; eauto with omega.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
...@@ -108,8 +108,8 @@ Lemma wp_le_false E n1 n2 Q : ...@@ -108,8 +108,8 @@ Lemma wp_le_false E n1 n2 Q :
n1 > n2 n1 > n2
Q LitFalseV wp E (Le (LitNat n1) (LitNat n2)) Q. Q LitFalseV wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse) //=; intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
last by intros; inv_step; eauto with lia. last by intros; inv_step; eauto with omega.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
...@@ -117,7 +117,7 @@ Lemma wp_fst E e1 v1 e2 v2 Q : ...@@ -117,7 +117,7 @@ Lemma wp_fst E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
Q v1 wp E (Fst (Pair e1 e2)) Q. Q v1 wp E (Fst (Pair e1 e2)) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (Fst _) e1) //=; intros; rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
...@@ -126,7 +126,7 @@ Lemma wp_snd E e1 v1 e2 v2 Q : ...@@ -126,7 +126,7 @@ Lemma wp_snd E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
Q v2 wp E (Snd (Pair e1 e2)) Q. Q v2 wp E (Snd (Pair e1 e2)) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (Snd _) e2) //=; intros; rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
...@@ -135,7 +135,7 @@ Lemma wp_case_inl E e0 v0 e1 e2 Q : ...@@ -135,7 +135,7 @@ Lemma wp_case_inl E e0 v0 e1 e2 Q :
to_val e0 = Some v0 to_val e0 = Some v0
wp E e1.[e0/] Q wp E (Case (InjL e0) e1 e2) Q. wp E e1.[e0/] Q wp E (Case (InjL e0) e1 e2) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/]) //=; intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/] None) ?right_id //;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
Qed. Qed.
...@@ -143,7 +143,7 @@ Lemma wp_case_inr E e0 v0 e1 e2 Q : ...@@ -143,7 +143,7 @@ Lemma wp_case_inr E e0 v0 e1 e2 Q :
to_val e0 = Some v0 to_val e0 = Some v0
wp E e2.[e0/] Q wp E (Case (InjR e0) e1 e2) Q. wp E e2.[e0/] Q wp E (Case (InjR e0) e1 e2) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/]) //=; intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/] None) ?right_id //;
last by intros; inv_step; eauto. last by intros; inv_step; eauto.
Qed. Qed.
...@@ -155,7 +155,7 @@ Lemma wp_le E n1 n2 P Q : ...@@ -155,7 +155,7 @@ Lemma wp_le E n1 n2 P Q :
Proof. Proof.
intros; destruct (decide (n1 n2)). intros; destruct (decide (n1 n2)).
* rewrite -wp_le_true; auto. * rewrite -wp_le_true; auto.
* rewrite -wp_le_false; auto with lia. * rewrite -wp_le_false; auto with omega.
Qed. Qed.
End lifting. End lifting.
...@@ -90,7 +90,7 @@ Module LiftingTests. ...@@ -90,7 +90,7 @@ Module LiftingTests.
* rewrite -wp_case_inr //. * rewrite -wp_case_inr //.
rewrite -!later_intro -wp_value' //. rewrite -!later_intro -wp_value' //.
rewrite and_elim_r. apply const_elim_l=>Hle. rewrite and_elim_r. apply const_elim_l=>Hle.
by replace n1 with (pred n2) by lia. by replace n1 with (pred n2) by omega.
Qed. Qed.
Lemma Pred_spec n E Q : Lemma Pred_spec n E Q :
...@@ -101,10 +101,10 @@ Module LiftingTests. ...@@ -101,10 +101,10 @@ Module LiftingTests.
apply later_mono, wp_le=> Hn. apply later_mono, wp_le=> Hn.
- rewrite -wp_case_inl //. - rewrite -wp_case_inl //.
rewrite -!later_intro -wp_value' //. rewrite -!later_intro -wp_value' //.
by replace n with 0 by lia. by replace n with 0 by omega.
- rewrite -wp_case_inr //. - rewrite -wp_case_inr //.
rewrite -!later_intro -FindPred_spec. rewrite -!later_intro -FindPred_spec.
auto using and_intro, const_intro with lia. auto using and_intro, const_intro with omega.
Qed. Qed.
Goal E, Goal E,
......
...@@ -44,6 +44,7 @@ Proof. ...@@ -44,6 +44,7 @@ Proof.
rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v. rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
by apply const_intro. by apply const_intro.
Qed. Qed.
Lemma ht_lift_atomic_step Lemma ht_lift_atomic_step
E (φ : expr Λ state Λ option (expr Λ) Prop) P e1 σ1 : E (φ : expr Λ state Λ option (expr Λ) Prop) P e1 σ1 :
atomic e1 atomic e1
...@@ -70,6 +71,7 @@ Proof. ...@@ -70,6 +71,7 @@ Proof.
rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //. rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro. by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
Qed. Qed.
Lemma ht_lift_pure_step E (φ : expr Λ option (expr Λ) Prop) P P' Q e1 : Lemma ht_lift_pure_step E (φ : expr Λ option (expr Λ) Prop) P P' Q e1 :
to_val e1 = None to_val e1 = None
( σ1, reducible e1 σ1) ( σ1, reducible e1 σ1)
...@@ -95,6 +97,7 @@ Proof. ...@@ -95,6 +97,7 @@ Proof.
rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v. rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
by apply const_intro. by apply const_intro.
Qed. Qed.
Lemma ht_lift_pure_det_step Lemma ht_lift_pure_det_step
E (φ : expr Λ option (expr Λ) Prop) P P' Q e1 e2 ef : E (φ : expr Λ option (expr Λ) Prop) P P' Q e1 e2 ef :
to_val e1 = None to_val e1 = None
...@@ -114,4 +117,5 @@ Proof. ...@@ -114,4 +117,5 @@ Proof.
rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst. rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst.
by rewrite /= /ht always_elim impl_elim_r. by rewrite /= /ht always_elim impl_elim_r.
Qed. Qed.
End lifting. End lifting.
...@@ -56,53 +56,60 @@ Qed. ...@@ -56,53 +56,60 @@ Qed.
Opaque uPred_holds. Opaque uPred_holds.
Import uPred. Import uPred.
Lemma wp_lift_atomic_step {E Q} e1 (φ : val Λ state Λ Prop) σ1 : Lemma wp_lift_atomic_step {E Q} e1 (φ : val Λ state Λ option (expr Λ) Prop) σ1 :
to_val e1 = None to_val e1 = None
reducible e1 σ1 reducible e1 σ1
( e' σ' ef, prim_step e1 σ1 e' σ' ef v', ef = None to_val e' = Some v' φ v' σ') ( e' σ' ef, prim_step e1 σ1 e' σ' ef v', to_val e' = Some v' φ v' σ' ef)
(ownP σ1 v2 σ2, ( φ v2 σ2 ownP σ2 - Q v2)) wp E e1 Q. (ownP σ1 v2 σ2 ef, φ v2 σ2 ef ownP σ2 -
Q v2 default True ef (flip (wp coPset_all) (λ _, True)))
wp E e1 Q.
Proof. Proof.
intros He Hsafe Hstep. intros He Hsafe Hstep.
rewrite -(wp_lift_step E E rewrite -(wp_lift_step E E
(λ e' σ' ef, v', ef = None to_val e' = Some v' φ v' σ') _ e1 σ1) //; []. (λ e' σ' ef, v', to_val e' = Some v' φ v' σ' ef) _ e1 σ1) //; [].
rewrite -pvs_intro. apply sep_mono, later_mono; first done. rewrite -pvs_intro. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'. apply forall_intro=>e2'; apply forall_intro=>σ2'.
apply forall_intro=>ef; apply wand_intro_l. apply forall_intro=>ef; apply wand_intro_l.
rewrite always_and_sep_l' -associative -always_and_sep_l'. rewrite always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[v2' [-> [Hv ?]]] /=. apply const_elim_l=>-[v2' [Hv ?]] /=.
rewrite -pvs_intro right_id -wp_value'; last by eassumption. rewrite -pvs_intro.
rewrite (forall_elim v2') (forall_elim σ2') const_equiv //. rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
by rewrite left_id wand_elim_r. rewrite left_id wand_elim_r. apply sep_mono; last done.
(* FIXME RJ why can't I do this rewrite before doing sep_mono? *)
by rewrite -(wp_value' _ _ e2').
Qed. Qed.
Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 : Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :
to_val e1 = None to_val e1 = None
reducible e1 σ1 reducible e1 σ1
( e' σ' ef, prim_step e1 σ1 e' σ' ef ef = None e' = of_val v2 σ' = σ2) ( e' σ' ef', prim_step e1 σ1 e' σ' ef' ef' = ef e' = of_val v2 σ' = σ2)
(ownP σ1 (ownP σ2 - Q v2)) wp E e1 Q. (ownP σ1 (ownP σ2 - Q v2
default True ef (flip (wp coPset_all) (λ _, True))))
wp E e1 Q.
Proof. Proof.
intros He Hsafe Hstep. intros He Hsafe Hstep.
rewrite -(wp_lift_atomic_step _ (λ v' σ', v' = v2 σ' = σ2) σ1) //; last first. 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. { intros. exists v2. apply Hstep in H. destruct_conjs; subst.
eauto using to_of_val. } eauto using to_of_val. }
apply sep_mono, later_mono; first done. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'. apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
apply wand_intro_l. apply wand_intro_l.
rewrite always_and_sep_l' -associative -always_and_sep_l'. rewrite always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[-> ->] /=. apply const_elim_l=>-[-> [-> ->]] /=.
by rewrite wand_elim_r. by rewrite wand_elim_r.
Qed. Qed.
Lemma wp_lift_pure_det_step {E Q} e1 e2 : Lemma wp_lift_pure_det_step {E Q} e1 e2 ef :
to_val e1 = None to_val e1 = None
( σ1, reducible e1 σ1) ( σ1, reducible e1 σ1)
( σ1 e' σ' ef, prim_step e1 σ1 e' σ' ef σ1 = σ' ef = None e' = e2) ( σ1 e' σ' ef', prim_step e1 σ1 e' σ' ef' σ1 = σ' ef' = ef e' = e2)
( wp E e2 Q) wp E e1 Q. (wp E e2 Q default True ef (flip (wp coPset_all) (λ _, True))) wp E e1 Q.
Proof. Proof.
intros. rewrite -(wp_lift_pure_step E (λ e' ef, ef = None e' = e2) _ e1) //=. intros. rewrite -(wp_lift_pure_step E (λ e' ef', ef' = ef e' = e2) _ e1) //=.
apply later_mono, forall_intro=>e'; apply forall_intro=>ef. apply later_mono, forall_intro=>e'; apply forall_intro=>ef'.
apply impl_intro_l, const_elim_l=>-[-> ->] /=. apply impl_intro_l, const_elim_l=>-[-> ->] /=; done.
by rewrite right_id.
Qed. Qed.
End lifting. End lifting.
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose tactics that are used throughout (** This file collects general purpose tactics that are used throughout
the development. *) the development. *)
Require Import Omega.
Require Export Psatz. Require Export Psatz.
Require Export prelude.base. Require Export prelude.base.
...@@ -24,6 +25,7 @@ to be combined in combination with other hint database. *) ...@@ -24,6 +25,7 @@ to be combined in combination with other hint database. *)
Hint Extern 998 (_ = _) => f_equal : f_equal. Hint Extern 998 (_ = _) => f_equal : f_equal.
Hint Extern 999 => congruence : congruence. Hint Extern 999 => congruence : congruence.
Hint Extern 1000 => lia : lia. Hint Extern 1000 => lia : lia.
Hint Extern 1000 => omega : omega.
(** The tactic [intuition] expands to [intuition auto with *] by default. This (** The tactic [intuition] expands to [intuition auto with *] by default. This
is rather efficient when having big hint databases, or expensive [Hint Extern] is rather efficient when having big hint databases, or expensive [Hint Extern]
......
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