Commit 4d94262b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use keywords in the notation of big ops on uPred.

We now have:

  Π★{map Q } ...
  Π★{set Q } ...

to differentiate between sets and maps.
parent 9997d0ef
...@@ -3,28 +3,27 @@ From prelude Require Import fin_maps fin_collections. ...@@ -3,28 +3,27 @@ From prelude Require Import fin_maps fin_collections.
(** * Big ops over lists *) (** * Big ops over lists *)
(* These are the basic building blocks for other big ops *) (* These are the basic building blocks for other big ops *)
Fixpoint uPred_list_and {M} (Ps : list (uPred M)) : uPred M:= Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M:=
match Ps with [] => True | P :: Ps => P uPred_list_and Ps end%I. match Ps with [] => True | P :: Ps => P uPred_big_and Ps end%I.
Instance: Params (@uPred_list_and) 1. Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_list_and Ps) (at level 20) : uPred_scope. Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
Fixpoint uPred_list_sep {M} (Ps : list (uPred M)) : uPred M := Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
match Ps with [] => True | P :: Ps => P uPred_list_sep Ps end%I. match Ps with [] => True | P :: Ps => P uPred_big_sep Ps end%I.
Instance: Params (@uPred_list_sep) 1. Instance: Params (@uPred_big_sep) 1.
Notation "'Π★' Ps" := (uPred_list_sep Ps) (at level 20) : uPred_scope. Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
(** * Other big ops *) (** * Other big ops *)
(** We use a type class to obtain overloaded notations *) (** We use a type class to obtain overloaded notations *)
Class UPredBigSep (M : cmraT) (A B : Type) := Definition uPred_big_sepM {M} `{FinMapToList K A MA}
uPred_big_sep : A B uPred M. (m : MA) (P : K A uPred M) : uPred M :=
Instance: Params (@uPred_big_sep) 4. uPred_big_sep (curry P <$> map_to_list m).
Notation "'Π★{' x } P" := (uPred_big_sep x P) Notation "'Π★{map' m } P" := (uPred_big_sepM m P)
(at level 20, x at level 10, format "Π★{ x } P") : uPred_scope. (at level 20, m at level 10, format "Π★{map m } P") : uPred_scope.
Instance uPred_big_sepM {M} `{FinMapToList K A MA} : Definition uPred_big_sepS {M} `{Elements A C}
UPredBigSep M MA (K A uPred M) := λ m P, (X : C) (P : A uPred M) : uPred M := uPred_big_sep (P <$> elements X).
uPred_list_sep (curry P <$> map_to_list m). Notation "'Π★{set' X } P" := (uPred_big_sepS X P)
Instance uPred_big_sepC {M} `{Elements A C} : (at level 20, X at level 10, format "Π★{set X } P") : uPred_scope.
UPredBigSep M C (A uPred M) := λ X P, uPred_list_sep (P <$> elements X).
(** * Always stability for lists *) (** * Always stability for lists *)
Class AlwaysStableL {M} (Ps : list (uPred M)) := Class AlwaysStableL {M} (Ps : list (uPred M)) :=
...@@ -38,47 +37,47 @@ Implicit Types Ps Qs : list (uPred M). ...@@ -38,47 +37,47 @@ Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type. Implicit Types A : Type.
(* Big ops *) (* Big ops *)
Global Instance list_and_proper : Proper (() ==> ()) (@uPred_list_and M). Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance list_sep_proper : Proper (() ==> ()) (@uPred_list_sep M). Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance list_and_perm : Proper (() ==> ()) (@uPred_list_and M). Global Instance big_and_perm : Proper (() ==> ()) (@uPred_big_and M).
Proof. Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
* by rewrite IH. * by rewrite IH.
* by rewrite !assoc (comm _ P). * by rewrite !assoc (comm _ P).
* etransitivity; eauto. * etransitivity; eauto.
Qed. Qed.
Global Instance list_sep_perm : Proper (() ==> ()) (@uPred_list_sep M). Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M).
Proof. Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
* by rewrite IH. * by rewrite IH.
* by rewrite !assoc (comm _ P). * by rewrite !assoc (comm _ P).
* etransitivity; eauto. * etransitivity; eauto.
Qed. Qed.
Lemma list_and_app Ps Qs : (Π (Ps ++ Qs))%I (Π Ps Π Qs)%I. Lemma big_and_app Ps Qs : (Π (Ps ++ Qs))%I (Π Ps Π Qs)%I.
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma list_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I (Π★ Ps Π★ Qs)%I. Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I (Π★ Ps Π★ Qs)%I.
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma list_sep_and Ps : (Π★ Ps) (Π Ps). Lemma big_sep_and Ps : (Π★ Ps) (Π Ps).
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed. Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
Lemma list_and_elem_of Ps P : P Ps (Π Ps) P. Lemma big_and_elem_of Ps P : P Ps (Π Ps) P.
Proof. induction 1; simpl; auto with I. Qed. Proof. induction 1; simpl; auto with I. Qed.
Lemma list_sep_elem_of Ps P : P Ps (Π★ Ps) P. Lemma big_sep_elem_of Ps P : P Ps (Π★ Ps) P.
Proof. induction 1; simpl; auto with I. Qed. Proof. induction 1; simpl; auto with I. Qed.
(* Big ops over finite maps *) (* Big ops over finite maps *)
Section fin_map. Section fin_map.
Context `{FinMap K Ma} {A} (P : K A uPred M). Context `{FinMap K Ma} {A} (P : K A uPred M).
Lemma big_sepM_empty : (Π★{} P)%I True%I. Lemma big_sepM_empty : (Π★{map } P)%I True%I.
Proof. by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_empty. Qed. Proof. by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert (m : Ma A) i x : Lemma big_sepM_insert (m : Ma A) i x :
m !! i = None (Π★{<[i:=x]> m} P)%I (P i x Π★{m} P)%I. m !! i = None (Π★{map <[i:=x]> m} P)%I (P i x Π★{map m} P)%I.
Proof. Proof.
intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert. intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert.
Qed. Qed.
Lemma big_sepM_singleton i x : (Π★{{[i x]}} P)%I (P i x)%I. Lemma big_sepM_singleton i x : (Π★{map {[i x]}} P)%I (P i x)%I.
Proof. Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty. rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id. by rewrite big_sepM_empty right_id.
...@@ -88,9 +87,9 @@ End fin_map. ...@@ -88,9 +87,9 @@ End fin_map.
(* Always stable *) (* Always stable *)
Local Notation AS := AlwaysStable. Local Notation AS := AlwaysStable.
Local Notation ASL := AlwaysStableL. Local Notation ASL := AlwaysStableL.
Global Instance list_and_always_stable Ps : ASL Ps AS (Π Ps). Global Instance big_and_always_stable Ps : ASL Ps AS (Π Ps).
Proof. induction 1; apply _. Qed. Proof. induction 1; apply _. Qed.
Global Instance list_sep_always_stable Ps : ASL Ps AS (Π★ Ps). Global Instance big_sep_always_stable Ps : ASL Ps AS (Π★ Ps).
Proof. induction 1; apply _. Qed. Proof. induction 1; apply _. Qed.
Global Instance nil_always_stable : ASL (@nil (uPred M)). Global Instance nil_always_stable : ASL (@nil (uPred M)).
......
...@@ -72,7 +72,7 @@ Section heap. ...@@ -72,7 +72,7 @@ Section heap.
Qed. Qed.
Lemma heap_alloc N σ : Lemma heap_alloc N σ :
ownP σ pvs N N ( γ, heap_ctx HeapI γ N Π★{σ} heap_mapsto HeapI γ). ownP σ pvs N N ( γ, heap_ctx HeapI γ N Π★{map σ} heap_mapsto HeapI γ).
Proof. Proof.
rewrite -{1}(from_to_heap σ); etransitivity; rewrite -{1}(from_to_heap σ); etransitivity;
first apply (auth_alloc (ownP of_heap) N (to_heap σ)), to_heap_valid. first apply (auth_alloc (ownP of_heap) N (to_heap σ)), to_heap_valid.
......
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