Commit 5e7d8f0b authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Do not require bi to be affine unnecessarily

parent a86906f4
......@@ -79,8 +79,8 @@ Section sep_list.
Lemma big_sepL_nil Φ : ([ list] ky nil, Φ k y) emp.
Proof. done. Qed.
Lemma big_sepL_nil' `{BiAffine PROP} P Φ : P [ list] ky nil, Φ k y.
Proof. apply (affine _). Qed.
Lemma big_sepL_nil' P `{!Affine P} Φ : P [ list] ky nil, Φ k y.
Proof. apply: affine. Qed.
Lemma big_sepL_cons Φ x l :
([ list] ky x :: l, Φ k y) Φ 0 x [ list] ky l, Φ (S k) y.
Proof. by rewrite big_opL_cons. Qed.
......@@ -205,12 +205,11 @@ Section sep_list.
apply forall_intro=> k. by rewrite (forall_elim (S k)).
Qed.
Lemma big_sepL_dupl `{BiAffine PROP} P l :
Lemma big_sepL_dup P `{!Affine P} l :
(P - P P) - P - [ list] kx l, P.
Proof.
apply wand_intro_l. induction l as [|x l IH].
{ apply big_sepL_nil'. }
rewrite !big_sepL_cons //.
apply wand_intro_l.
induction l as [|x l IH]=> /=; first by apply: affine.
rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
Qed.
......@@ -324,8 +323,8 @@ Section sep_list2.
Lemma big_sepL2_nil Φ : ([ list] ky1;y2 []; [], Φ k y1 y2) emp.
Proof. done. Qed.
Lemma big_sepL2_nil' `{BiAffine PROP} P Φ : P [ list] ky1;y2 [];[], Φ k y1 y2.
Proof. apply (affine _). Qed.
Lemma big_sepL2_nil' P `{!Affine P} Φ : P [ list] ky1;y2 [];[], Φ k y1 y2.
Proof. apply: affine. Qed.
Lemma big_sepL2_nil_inv_l Φ l2 :
([ list] ky1;y2 []; l2, Φ k y1 y2) - l2 = [].
Proof. destruct l2; simpl; auto using False_elim, pure_intro. Qed.
......@@ -852,7 +851,7 @@ Section map.
Lemma big_sepM_empty Φ : ([ map] kx , Φ k x) emp.
Proof. by rewrite big_opM_empty. Qed.
Lemma big_sepM_empty' `{BiAffine PROP} P Φ : P [ map] kx , Φ k x.
Lemma big_sepM_empty' P `{!Affine P} Φ : P [ map] kx , Φ k x.
Proof. rewrite big_sepM_empty. apply: affine. Qed.
Lemma big_sepM_insert Φ m i x :
......@@ -1006,11 +1005,11 @@ Section map.
by rewrite pure_True // True_impl.
Qed.
Lemma big_sepM_dupl `{BiAffine PROP} P m :
Lemma big_sepM_dup P `{!Affine P} m :
(P - P P) - P - [ map] kx m, P.
Proof.
apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
{ apply big_sepM_empty'. }
{ apply: big_sepM_empty'. }
rewrite !big_sepM_insert //.
rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
......@@ -1142,8 +1141,8 @@ Section map2.
rewrite big_sepM2_eq /big_sepM2_def big_opM_eq pure_True ?left_id //.
intros k. rewrite !lookup_empty; split; by inversion 1.
Qed.
Lemma big_sepM2_empty' `{BiAffine PROP} P Φ : P [ map] ky1;y2 ;, Φ k y1 y2.
Proof. rewrite big_sepM2_empty. apply (affine _). Qed.
Lemma big_sepM2_empty' P `{!Affine P} Φ : P [ map] ky1;y2 ;, Φ k y1 y2.
Proof. rewrite big_sepM2_empty. apply: affine. Qed.
Lemma big_sepM2_empty_l m1 Φ : ([ map] ky1;y2 m1; , Φ k y1 y2) m1 = ∅⌝.
Proof.
......@@ -1474,7 +1473,7 @@ Section gset.
Lemma big_sepS_empty Φ : ([ set] x , Φ x) emp.
Proof. by rewrite big_opS_empty. Qed.
Lemma big_sepS_empty' `{!BiAffine PROP} P Φ : P [ set] x , Φ x.
Lemma big_sepS_empty' P `{!Affine P} Φ : P [ set] x , Φ x.
Proof. rewrite big_sepS_empty. apply: affine. Qed.
Lemma big_sepS_insert Φ X x :
......@@ -1594,11 +1593,11 @@ Section gset.
by rewrite pure_True ?True_impl; last set_solver.
Qed.
Lemma big_sepS_dupl `{BiAffine PROP} P X :
(P - P P) - P - [ set] x X, P.
Lemma big_sepS_dup P `{!Affine P} X :
(P - P P) - P - [ set] x X, P.
Proof.
apply wand_intro_l. induction X as [|x X ? IH] using set_ind_L.
{ apply big_sepS_empty'. }
{ apply: big_sepS_empty'. }
rewrite !big_sepS_insert //.
rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
......@@ -1676,7 +1675,7 @@ Section gmultiset.
Lemma big_sepMS_empty Φ : ([ mset] x , Φ x) emp.
Proof. by rewrite big_opMS_empty. Qed.
Lemma big_sepMS_empty' `{!BiAffine PROP} P Φ : P [ mset] x , Φ x.
Lemma big_sepMS_empty' P `{!Affine P} Φ : P [ mset] x , Φ x.
Proof. rewrite big_sepMS_empty. apply: affine. Qed.
Lemma big_sepMS_disj_union Φ X Y :
......
......@@ -3246,17 +3246,17 @@ below; see the discussion in !75 for further details. *)
Hint Extern 0 (envs_entails _ (_ _)) =>
rewrite envs_entails_eq; apply internal_eq_refl : core.
Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL_nil' : core.
rewrite envs_entails_eq; apply: big_sepL_nil' : core.
Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL2_nil' : core.
rewrite envs_entails_eq; apply: big_sepL2_nil' : core.
Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
rewrite envs_entails_eq; apply big_sepM_empty' : core.
rewrite envs_entails_eq; apply: big_sepM_empty' : core.
Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
rewrite envs_entails_eq; apply big_sepM2_empty' : core.
rewrite envs_entails_eq; apply: big_sepM2_empty' : core.
Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
rewrite envs_entails_eq; apply big_sepS_empty' : core.
rewrite envs_entails_eq; apply: big_sepS_empty' : core.
Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
rewrite envs_entails_eq; apply big_sepMS_empty' : core.
rewrite envs_entails_eq; apply: big_sepMS_empty' : core.
(* These introduce as much as possible at once, for better performance. *)
Hint Extern 0 (envs_entails _ ( _, _)) => iIntros : core.
......
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