Commit daeeaf05 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/bigop' into 'gen_proofmode'

provide big_op lemmas outside of bi module

See merge request FP/iris-coq!149
parents 0ea6c627 031c3914
...@@ -6,9 +6,16 @@ Module Import bi. ...@@ -6,9 +6,16 @@ Module Import bi.
Export bi.interface.bi. Export bi.interface.bi.
Export bi.derived_laws_bi.bi. Export bi.derived_laws_bi.bi.
Export bi.derived_laws_sbi.bi. Export bi.derived_laws_sbi.bi.
(* For better compatibility with some developments created during
gen_proofmode times, also provide bigops inside the bi
module. *)
Export bi.big_op.bi. Export bi.big_op.bi.
End bi. End bi.
(* For better compatibility with pre-gen_proofmode-Iris, also provide
bigops outside of the bi module. *)
Export bi.big_op.bi.
(* Hint DB for the logic *) (* Hint DB for the logic *)
Hint Resolve pure_intro. Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r' : BI. Hint Resolve or_elim or_intro_l' or_intro_r' : BI.
......
...@@ -104,7 +104,7 @@ Proof. ...@@ -104,7 +104,7 @@ Proof.
iApply (wp_lift_pure_det_step with "[HWP]"). iApply (wp_lift_pure_det_step with "[HWP]").
- intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val. - intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
- destruct s; naive_solver. - destruct s; naive_solver.
- by rewrite bi.big_sepL_nil right_id. - by rewrite big_sepL_nil right_id.
Qed. Qed.
Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ : Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
......
...@@ -170,7 +170,7 @@ Section lifting. ...@@ -170,7 +170,7 @@ Section lifting.
{{{ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}. {{{ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
Proof. Proof.
intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..]. intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
rewrite bi.big_sepL_nil right_id. by apply bi.wand_intro_r. rewrite big_sepL_nil right_id. by apply bi.wand_intro_r.
Qed. Qed.
Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs : Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
...@@ -188,7 +188,7 @@ Section lifting. ...@@ -188,7 +188,7 @@ Section lifting.
( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs') ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs')
WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}. WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?bi.big_sepL_nil ?right_id; eauto. intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
Qed. Qed.
End lifting. 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