Commit 93792f5c authored by Robbert Krebbers's avatar Robbert Krebbers

Change notations of big_ops for upred.

Rationale: to make the code closer to what is on paper, I want the notations
to look like quantifiers, i.e. have a binder built-in. I thus introduced the
following notations:

  [★ map] k ↦ x ∈ m, P
  [★ set] x ∈ X, P

The good thing - contrary to the notations that we had before that required an
explicit lambda - is that type annotations of k and x are now not printed
making goals much easier to read.
parent 92768cff
Pipeline #1141 passed with stage
......@@ -2,31 +2,44 @@ From iris.algebra Require Export upred list.
From iris.prelude Require Import gmap fin_collections functions.
Import uPred.
(** We define the following big operators:
- The operators [ [★] Ps ] and [ [∧] Ps ] fold [★] and [∧] over the list [Ps].
This operator is not a quantifier, so it binds strongly.
- The operator [ [★ map] k ↦ x ∈ m, P ] asserts that [P] holds separately for
each [k ↦ x] in the map [m]. This operator is a quantifier, and thus has the
same precedence as [∀] and [∃].
- The operator [ [★ set] x ∈ X, P ] asserts that [P] holds separately for each
[x] in the set [X]. This operator is a quantifier, and thus has the same
precedence as [∀] and [∃]. *)
(** * Big ops over lists *)
(* These are the basic building blocks for other big ops *)
Fixpoint uPred_big_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_big_and Ps end%I.
Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
Notation "'[∧]' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
match Ps with [] => True | P :: Ps => P uPred_big_sep Ps end%I.
Instance: Params (@uPred_big_sep) 1.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
(** * Other big ops *)
(** We use a type class to obtain overloaded notations *)
Definition uPred_big_sepM {M} `{Countable K} {A}
(m : gmap K A) (Φ : K A uPred M) : uPred M :=
uPred_big_sep (curry Φ <$> map_to_list m).
[] (curry Φ <$> map_to_list m).
Instance: Params (@uPred_big_sepM) 6.
Notation "'Π★{map' m } Φ" := (uPred_big_sepM m Φ)
(at level 20, m at level 10, format "Π★{map m } Φ") : uPred_scope.
Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
(at level 200, m at level 10, k, x at level 1, right associativity,
format "[★ map ] k ↦ x ∈ m , P") : uPred_scope.
Definition uPred_big_sepS {M} `{Countable A}
(X : gset A) (Φ : A uPred M) : uPred M := uPred_big_sep (Φ <$> elements X).
(X : gset A) (Φ : A uPred M) : uPred M := [] (Φ <$> elements X).
Instance: Params (@uPred_big_sepS) 5.
Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
(at level 20, X at level 10, format "Π★{set X } Φ") : uPred_scope.
Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P))
(at level 200, X at level 10, x at level 1, right associativity,
format "[★ set ] x ∈ X , P") : uPred_scope.
(** * Persistence of lists of uPreds *)
Class PersistentL {M} (Ps : list (uPred M)) :=
......@@ -70,26 +83,26 @@ Proof.
- etrans; eauto.
Qed.
Lemma big_and_app Ps Qs : Π (Ps ++ Qs) (Π Ps Π Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : Π★ (Ps ++ Qs) (Π★ Ps Π★ Qs).
Lemma big_and_app Ps Qs : [] (Ps ++ Qs) ([] Ps [] Qs).
Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs) ([] Ps [] Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_and_contains Ps Qs : Qs `contains` Ps Π Ps Π Qs.
Lemma big_and_contains Ps Qs : Qs `contains` Ps [] Ps [] Qs.
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
Qed.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps Π★ Ps Π★ Qs.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps [] Ps [] Qs.
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
Qed.
Lemma big_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.
Lemma big_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.
Lemma big_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.
(** ** Big ops over finite maps *)
......@@ -100,16 +113,16 @@ Section gmap.
Lemma big_sepM_mono Φ Ψ m1 m2 :
m2 m1 ( x k, m2 !! k = Some x Φ k x Ψ k x)
Π★{map m1} Φ Π★{map m2} Ψ.
([ map] k x m1, Φ k x) ([ map] k x m2, Ψ k x).
Proof.
intros HX HΦ. trans (Π★{map m2} Φ)%I.
intros HX HΦ. trans ([ map] kx m2, Φ k x)%I.
- by apply big_sep_contains, fmap_contains, map_to_list_contains.
- apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
Qed.
Lemma big_sepM_proper Φ Ψ m1 m2 :
m1 m2 ( x k, m1 !! k = Some x m2 !! k = Some x Φ k x Ψ k x)
Π★{map m1} Φ Π★{map m2} Ψ.
([ map] k x m1, Φ k x) ([ map] k x m2, Ψ k x).
Proof.
(* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
File "./algebra/upred_big_op.v", line 114, characters 4-131:
......@@ -134,28 +147,32 @@ Section gmap.
(uPred_big_sepM (M:=M) m).
Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
Lemma big_sepM_empty Φ : Π★{map } Φ True.
Lemma big_sepM_empty Φ : ([ map] kx , Φ k x) True.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert Φ (m : gmap K A) i x :
m !! i = None Π★{map <[i:=x]> m} Φ (Φ i x Π★{map m} Φ).
m !! i = None
([ map] ky <[i:=x]> m, Φ k y) (Φ i x [ map] ky m, Φ k y).
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Lemma big_sepM_delete Φ (m : gmap K A) i x :
m !! i = Some x Π★{map m} Φ (Φ i x Π★{map delete i m} Φ).
m !! i = Some x
([ map] ky m, Φ k y) (Φ i x [ map] ky delete i m, Φ k y).
Proof. intros. by rewrite -big_sepM_insert ?lookup_delete // insert_delete. Qed.
Lemma big_sepM_singleton Φ i x : Π★{map {[i := x]}} Φ (Φ i x).
Lemma big_sepM_singleton Φ i x : ([ map] ky {[i:=x]}, Φ k y) Φ i x.
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id.
Qed.
Lemma big_sepM_sepM Φ Ψ m :
Π★{map m} (λ i x, Φ i x Ψ i x) (Π★{map m} Φ Π★{map m} Ψ).
([ map] kx m, Φ k x Ψ k x)
(([ map] kx m, Φ k x) ([ map] kx m, Ψ k x)).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ _)%I]comm -!assoc.
Qed.
Lemma big_sepM_later Φ m : Π★{map m} Φ Π★{map m} (λ i x, Φ i x).
Lemma big_sepM_later Φ m :
( [ map] kx m, Φ k x) ([ map] kx m, Φ k x).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
......@@ -170,15 +187,17 @@ Section gset.
Implicit Types Φ : A uPred M.
Lemma big_sepS_mono Φ Ψ X Y :
Y X ( x, x Y Φ x Ψ x) Π★{set X} Φ Π★{set Y} Ψ.
Y X ( x, x Y Φ x Ψ x)
([ set] x X, Φ x) ([ set] x Y, Ψ x).
Proof.
intros HX HΦ. trans (Π★{set Y} Φ)%I.
intros HX HΦ. trans ([ set] x Y, Φ x)%I.
- by apply big_sep_contains, fmap_contains, elements_contains.
- apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
Qed.
Lemma big_sepS_proper Φ Ψ X Y :
X Y ( x, x X x Y Φ x Ψ x) Π★{set X} Φ Π★{set Y} Ψ.
X Y ( x, x X x Y Φ x Ψ x)
([ set] x X, Φ x) ([ set] x Y, Ψ x).
Proof.
intros [??] ?; apply (anti_symm ()); apply big_sepS_mono;
eauto using equiv_entails, equiv_entails_sym.
......@@ -197,44 +216,44 @@ Section gset.
Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
Lemma big_sepS_empty Φ : Π★{set } Φ True.
Lemma big_sepS_empty Φ : ([ set] x , Φ x) True.
Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
Lemma big_sepS_insert Φ X x :
x X Π★{set {[ x ]} X} Φ (Φ x Π★{set X} Φ).
x X ([ set] y {[ x ]} X, Φ y) (Φ x [ set] y X, Φ y).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_insert' (Ψ : A uPred M uPred M) Φ X x P :
x X
Π★{set {[ x ]} X} (λ y, Ψ y (<[x:=P]> Φ y))
(Ψ x P Π★{set X} (λ y, Ψ y (Φ y))).
([ set] y {[ x ]} X, Ψ y (<[x:=P]> Φ y))
(Ψ x P [ set] y X, Ψ y (Φ y)).
Proof.
intros. rewrite big_sepS_insert // fn_lookup_insert.
apply sep_proper, big_sepS_proper; auto=> y ??.
by rewrite fn_lookup_insert_ne; last set_solver.
Qed.
Lemma big_sepS_insert'' Φ X x P :
x X Π★{set {[ x ]} X} (<[x:=P]> Φ) (P Π★{set X} Φ).
x X ([ set] y {[ x ]} X, <[x:=P]> Φ y) (P [ set] y X, Φ y).
Proof. apply (big_sepS_insert' (λ y, id)). Qed.
Lemma big_sepS_delete Φ X x :
x X Π★{set X} Φ (Φ x Π★{set X {[ x ]}} Φ).
x X ([ set] y X, Φ y) (Φ x [ set] y X {[ x ]}, Φ y).
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
Lemma big_sepS_singleton Φ x : Π★{set {[ x ]}} Φ (Φ x).
Lemma big_sepS_singleton Φ x : ([ set] y {[ x ]}, Φ y) Φ x.
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
Lemma big_sepS_sepS Φ Ψ X :
Π★{set X} (λ x, Φ x Ψ x) (Π★{set X} Φ Π★{set X} Ψ).
([ set] y X, Φ y Ψ y) (([ set] y X, Φ y) [ set] y X, Ψ y).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ _)%I]comm -!assoc.
Qed.
Lemma big_sepS_later Φ X : Π★{set X} Φ Π★{set X} (λ x, Φ x).
Lemma big_sepS_later Φ X : ( [ set] y X, Φ y) ([ set] y X, Φ y).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
......@@ -243,9 +262,9 @@ Section gset.
End gset.
(** ** Persistence *)
Global Instance big_and_persistent Ps : PersistentL Ps PersistentP (Π Ps).
Global Instance big_and_persistent Ps : PersistentL Ps PersistentP ([] Ps).
Proof. induction 1; apply _. Qed.
Global Instance big_sep_persistent Ps : PersistentL Ps PersistentP (Π★ Ps).
Global Instance big_sep_persistent Ps : PersistentL Ps PersistentP ([] Ps).
Proof. induction 1; apply _. Qed.
Global Instance nil_persistent : PersistentL (@nil (uPred M)).
......
......@@ -22,8 +22,7 @@ Module uPred_reflection. Section uPred_reflection.
| ESep e1 e2 => flatten e1 ++ flatten e2
end.
Notation eval_list Σ l :=
(uPred_big_sep ((λ n, from_option True%I (Σ !! n)) <$> l)).
Notation eval_list Σ l := ([] ((λ n, from_option True%I (Σ !! n)) <$> l))%I.
Lemma eval_flatten Σ e : eval Σ e eval_list Σ (flatten e).
Proof.
induction e as [| |e1 IH1 e2 IH2];
......
......@@ -98,7 +98,7 @@ Section heap.
(** Allocation *)
Lemma heap_alloc N E σ :
authG heap_lang Σ heapR nclose N E
ownP σ (|={E}=> _ : heapG Σ, heap_ctx N Π★{map σ} (λ l v, l v)).
ownP σ (|={E}=> _ : heapG Σ, heap_ctx N [ map] lv σ, l v).
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro.
......
......@@ -28,7 +28,7 @@ Local Notation iProp := (iPropG heap_lang Σ).
Definition ress (P : iProp) (I : gset gname) : iProp :=
( Ψ : gname iProp,
(P - Π★{set I} Ψ) Π★{set I} (λ i, saved_prop_own i (Ψ i)))%I.
(P - [ set] i I, Ψ i) [ set] i I, saved_prop_own i (Ψ i))%I.
Coercion state_to_val (s : state) : val :=
match s with State Low _ => #0 | State High _ => #1 end.
......@@ -159,7 +159,7 @@ Proof.
iSplit; [iPureIntro; by eauto using wait_step|].
iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert ( Ψ i Π★{set (I {[i]})} Ψ)%I with "[HΨ]" as "[HΨ HΨ']".
iAssert ( Ψ i [ set] j I {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
iSplitL "HΨ' Hl Hsp"; [iNext|].
+ rewrite {2}/barrier_inv /=; iFrame "Hl".
......
......@@ -25,7 +25,7 @@ Record envs_wf {M} (Δ : envs M) := {
}.
Coercion of_envs {M} (Δ : envs M) : uPred M :=
( envs_wf Δ Π env_persistent Δ Π★ env_spatial Δ)%I.
( envs_wf Δ [] env_persistent Δ [] env_spatial Δ)%I.
Instance: Params (@of_envs) 1.
Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
......@@ -102,7 +102,7 @@ Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.
Lemma of_envs_def Δ :
of_envs Δ = ( envs_wf Δ Π env_persistent Δ Π★ env_spatial Δ)%I.
of_envs Δ = ( envs_wf Δ [] env_persistent Δ [] env_spatial Δ)%I.
Proof. done. Qed.
Lemma envs_lookup_delete_Some Δ Δ' i p P :
......@@ -120,12 +120,12 @@ Proof.
rewrite /envs_lookup /envs_delete /of_envs=>?; apply const_elim_sep_l=> Hwf.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
- rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
ecancel [ Π _; P; Π★ _]%I; apply const_intro.
ecancel [ [] _; P; [] _]%I; apply const_intro.
destruct Hwf; constructor;
naive_solver eauto using env_delete_wf, env_delete_fresh.
- destruct (Γs !! i) eqn:?; simplify_eq/=.
rewrite (env_lookup_perm Γs) //=.
ecancel [ Π _; P; Π★ _]%I; apply const_intro.
ecancel [ [] _; P; [] _]%I; apply const_intro.
destruct Hwf; constructor;
naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
......@@ -158,7 +158,7 @@ Lemma envs_lookup_delete_sound' Δ Δ' i p P :
envs_lookup_delete i Δ = Some (p,P,Δ') Δ (P Δ')%I.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' Δ (?p Π★ Γ - Δ').
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' Δ (?p [] Γ - Δ').
Proof.
rewrite /of_envs /envs_app=> ?; apply const_elim_sep_l=> Hwf.
destruct Δ as [Γp Γs], p; simplify_eq/=.
......@@ -182,7 +182,7 @@ Qed.
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
envs_simple_replace i p Γ Δ = Some Δ'
envs_delete i p Δ (?p Π★ Γ - Δ')%I.
envs_delete i p Δ (?p [] Γ - Δ')%I.
Proof.
rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
apply const_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
......@@ -206,11 +206,11 @@ Qed.
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
envs_lookup i Δ = Some (p,P) envs_simple_replace i p Γ Δ = Some Δ'
Δ (?p P (?p Π★ Γ - Δ'))%I.
Δ (?p P (?p [] Γ - Δ'))%I.
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
Lemma envs_replace_sound' Δ Δ' i p q Γ :
envs_replace i p q Γ Δ = Some Δ' envs_delete i p Δ (?q Π★ Γ - Δ')%I.
envs_replace i p q Γ Δ = Some Δ' envs_delete i p Δ (?q [] Γ - Δ')%I.
Proof.
rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
- apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
......@@ -219,7 +219,7 @@ Qed.
Lemma envs_replace_sound Δ Δ' i p q P Γ :
envs_lookup i Δ = Some (p,P) envs_replace i p q Γ Δ = Some Δ'
Δ (?p P (?q Π★ Γ - Δ'))%I.
Δ (?p P (?q [] Γ - Δ'))%I.
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
Lemma envs_split_sound Δ lr js Δ1 Δ2 :
......@@ -228,21 +228,21 @@ Proof.
rewrite /envs_split /of_envs=> ?; apply const_elim_sep_l=> Hwf.
destruct Δ as [Γp Γs], (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq/=.
rewrite (env_split_perm Γs) // big_sep_app {1}always_sep_dup'.
destruct lr; simplify_eq/=; cancel [ Π Γp; Π Γp; Π★ Γs1; Π★ Γs2]%I;
destruct lr; simplify_eq/=; cancel [ [] Γp; [] Γp; [] Γs1; [] Γs2]%I;
destruct Hwf; apply sep_intro_True_l; apply const_intro; constructor;
naive_solver eauto using env_split_wf_1, env_split_wf_2,
env_split_fresh_1, env_split_fresh_2.
Qed.
Lemma envs_clear_spatial_sound Δ :
Δ (envs_clear_spatial Δ Π★ env_spatial Δ)%I.
Δ (envs_clear_spatial Δ [] env_spatial Δ)%I.
Proof.
rewrite /of_envs /envs_clear_spatial /=; apply const_elim_sep_l=> Hwf.
rewrite right_id -assoc; apply sep_intro_True_l; [apply const_intro|done].
destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.
Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ (Π★ Γ - Q).
Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ ([] Γ - Q).
Proof.
revert Q; induction Γ as [|Γ IH i P]=> Q /=; [by rewrite wand_True|].
by rewrite IH wand_curry (comm uPred_sep).
......
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