Commit a3cbeaff authored by Robbert Krebbers's avatar Robbert Krebbers

Revert "Make the types of the finite map type classes more specific."

This reverts commit 20b4ae55, which does
not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).
parent 20b4ae55
...@@ -47,7 +47,7 @@ Proof. ...@@ -47,7 +47,7 @@ Proof.
by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k'). by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
Qed. Qed.
Global Instance insert_ne i n : Global Instance insert_ne i n :
Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K) i). Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
Proof. Proof.
intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq; intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
[by constructor|by apply lookup_ne]. [by constructor|by apply lookup_ne].
...@@ -56,7 +56,7 @@ Global Instance singleton_ne i n : ...@@ -56,7 +56,7 @@ Global Instance singleton_ne i n :
Proper (dist n ==> dist n) (singletonM i : A gmap K A). Proper (dist n ==> dist n) (singletonM i : A gmap K A).
Proof. by intros ???; apply insert_ne. Qed. Proof. by intros ???; apply insert_ne. Qed.
Global Instance delete_ne i n : Global Instance delete_ne i n :
Proper (dist n ==> dist n) (delete (M:=gmap K) i). Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
Proof. Proof.
intros m m' ? j; destruct (decide (i = j)); simplify_map_eq; intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
[by constructor|by apply lookup_ne]. [by constructor|by apply lookup_ne].
...@@ -183,12 +183,10 @@ Arguments gmapUR _ {_ _} _. ...@@ -183,12 +183,10 @@ Arguments gmapUR _ {_ _} _.
Section properties. Section properties.
Context `{Countable K} {A : cmraT}. Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A. Implicit Types m : gmap K A.
Implicit Types mm : option (gmap K A).
Implicit Types i : K. Implicit Types i : K.
Implicit Types x y : A. Implicit Types x y : A.
Lemma lookup_opM m1 mm2 i : Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i (mm2 = (!! i)).
(m1 ? mm2) !! i = m1 !! i (mm2 = (!! i) : option A).
Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed. Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
Lemma lookup_validN_Some n m i x : {n} m m !! i {n} Some x {n} x. Lemma lookup_validN_Some n m i x : {n} m m !! i {n} Some x {n} x.
...@@ -345,8 +343,7 @@ Section freshness. ...@@ -345,8 +343,7 @@ Section freshness.
End freshness. End freshness.
Lemma insert_local_update m i x y mf : Lemma insert_local_update m i x y mf :
x ~l~> y @ mf = (!! i) x ~l~> y @ mf = (!! i) <[i:=x]>m ~l~> <[i:=y]>m @ mf.
(<[i:=x]>m : gmap K A) ~l~> <[i:=y]>m @ mf.
Proof. Proof.
intros [Hxy Hxy']; split. intros [Hxy Hxy']; split.
- intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst. - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
...@@ -359,8 +356,7 @@ Proof. ...@@ -359,8 +356,7 @@ Proof.
Qed. Qed.
Lemma singleton_local_update i x y mf : Lemma singleton_local_update i x y mf :
x ~l~> y @ mf = (!! i) x ~l~> y @ mf = (!! i) {[ i := x ]} ~l~> {[ i := y ]} @ mf.
({[ i := x ]} : gmap K A) ~l~> {[ i := y ]} @ mf.
Proof. apply insert_local_update. Qed. Proof. apply insert_local_update. Qed.
Lemma alloc_singleton_local_update m i x mf : Lemma alloc_singleton_local_update m i x mf :
...@@ -375,8 +371,7 @@ Proof. ...@@ -375,8 +371,7 @@ Proof.
Qed. Qed.
Lemma alloc_unit_singleton_local_update i x mf : Lemma alloc_unit_singleton_local_update i x mf :
mf = (!! i) = None x mf = (!! i) = None x ~l~> {[ i := x ]} @ mf.
(:gmap K A) ~l~> {[ i := x ]} @ mf.
Proof. Proof.
intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi. intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
Qed. Qed.
......
...@@ -17,17 +17,17 @@ Global Instance tail_ne n : Proper (dist n ==> dist n) (@tail A) := _. ...@@ -17,17 +17,17 @@ Global Instance tail_ne n : Proper (dist n ==> dist n) (@tail A) := _.
Global Instance take_ne n : Proper (dist n ==> dist n) (@take A n) := _. Global Instance take_ne n : Proper (dist n ==> dist n) (@take A n) := _.
Global Instance drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _. Global Instance drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _.
Global Instance list_lookup_ne n i : Global Instance list_lookup_ne n i :
Proper (dist n ==> dist n) (lookup (M:=list) i). Proper (dist n ==> dist n) (lookup (M:=list A) i).
Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed. Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
Global Instance list_alter_ne n f i : Global Instance list_alter_ne n f i :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) f
Proper (dist n ==> dist n) (alter (M:=list) f i) := _. Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
Global Instance list_insert_ne n i : Global Instance list_insert_ne n i :
Proper (dist n ==> dist n ==> dist n) (insert (M:=list) i) := _. Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _.
Global Instance list_inserts_ne n i : Global Instance list_inserts_ne n i :
Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _. Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _.
Global Instance list_delete_ne n i : Global Instance list_delete_ne n i :
Proper (dist n ==> dist n) (delete (M:=list) i) := _. Proper (dist n ==> dist n) (delete (M:=list A) i) := _.
Global Instance option_list_ne n : Proper (dist n ==> dist n) (@option_list A). Global Instance option_list_ne n : Proper (dist n ==> dist n) (@option_list A).
Proof. intros ???; by apply Forall2_option_list, dist_option_Forall2. Qed. Proof. intros ???; by apply Forall2_option_list, dist_option_Forall2. Qed.
Global Instance list_filter_ne n P `{ x, Decision (P x)} : Global Instance list_filter_ne n P `{ x, Decision (P x)} :
...@@ -236,20 +236,17 @@ End cmra. ...@@ -236,20 +236,17 @@ End cmra.
Arguments listR : clear implicits. Arguments listR : clear implicits.
Arguments listUR : clear implicits. Arguments listUR : clear implicits.
Definition list_singleton {A : ucmraT} (n : nat) (x : A) : list A := Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
replicate n ++ [x]. replicate n ++ [x].
Section properties. Section properties.
Context {A : ucmraT}. Context {A : ucmraT}.
Implicit Types l k : list A. Implicit Types l : list A.
Implicit Types ml mk : option (list A).
Implicit Types x y z : A. Implicit Types x y z : A.
Implicit Types i : nat.
Local Arguments op _ _ !_ !_ / : simpl nomatch. Local Arguments op _ _ !_ !_ / : simpl nomatch.
Local Arguments cmra_op _ !_ !_ / : simpl nomatch. Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
Lemma list_lookup_opM l mk i : Lemma list_lookup_opM l mk i : (l ? mk) !! i = l !! i (mk = (!! i)).
(l ? mk) !! i = l !! i (mk = (!! i) : option A).
Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed. Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.
Lemma list_op_app l1 l2 l3 : Lemma list_op_app l1 l2 l3 :
...@@ -269,52 +266,57 @@ Section properties. ...@@ -269,52 +266,57 @@ Section properties.
Lemma replicate_valid n (x : A) : x replicate n x. Lemma replicate_valid n (x : A) : x replicate n x.
Proof. apply Forall_replicate. Qed. Proof. apply Forall_replicate. Qed.
Global Instance list_singleton_ne n i : Global Instance list_singletonM_ne n i :
Proper (dist n ==> dist n) (@list_singleton A i). Proper (dist n ==> dist n) (@list_singletonM A i).
Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed. Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
Global Instance list_singleton_proper i : Global Instance list_singletonM_proper i :
Proper (() ==> ()) (list_singleton i) := ne_proper _. Proper (() ==> ()) (list_singletonM i) := ne_proper _.
Lemma elem_of_list_singleton i z x : z list_singleton i x z = z = x. Lemma elem_of_list_singletonM i z x : z {[i := x]} z = z = x.
Proof. Proof.
rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver. rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
Qed. Qed.
Lemma list_lookup_singleton i x : list_singleton i x !! i = Some x. Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x.
Proof. induction i; by f_equal/=. Qed. Proof. induction i; by f_equal/=. Qed.
Lemma list_lookup_singleton_ne i j x : Lemma list_lookup_singletonM_ne i j x :
i j list_singleton i x !! j = None list_singleton i x !! j = Some . i j {[ i := x ]} !! j = None {[ i := x ]} !! j = Some .
Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed. Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
Lemma list_singleton_validN n i x : {n} (list_singleton i x) {n} x. Lemma list_singletonM_validN n i x : {n} {[ i := x ]} {n} x.
Proof. Proof.
rewrite list_lookup_validN. split. rewrite list_lookup_validN. split.
{ move=> /(_ i). by rewrite list_lookup_singleton. } { move=> /(_ i). by rewrite list_lookup_singletonM. }
intros Hx j; destruct (decide (i = j)); subst. intros Hx j; destruct (decide (i = j)); subst.
- by rewrite list_lookup_singleton. - by rewrite list_lookup_singletonM.
- destruct (list_lookup_singleton_ne i j x) as [Hi|Hi]; first done; - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
rewrite Hi; by try apply (ucmra_unit_validN (A:=A)). rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
Qed. Qed.
Lemma list_singleton_valid i x : (list_singleton i x) x. Lemma list_singleton_valid i x : {[ i := x ]} x.
Proof.
rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
Qed.
Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
Proof. Proof.
rewrite !cmra_valid_validN. by setoid_rewrite list_singleton_validN. rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
Qed. Qed.
Lemma list_singleton_length i x : length (list_singleton i x) = S i.
Proof. rewrite /list_singleton app_length replicate_length /=; lia. Qed.
Lemma list_core_singleton i x : Lemma list_core_singletonM i (x : A) : core {[ i := x ]} {[ i := core x ]}.
core (list_singleton i x) list_singleton i (core x).
Proof. Proof.
rewrite /list_singleton. rewrite /singletonM /list_singletonM.
by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ). by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ).
Qed. Qed.
Lemma list_op_singleton i x y : Lemma list_op_singletonM i (x y : A) :
list_singleton i x list_singleton i y list_singleton i (x y). {[ i := x ]} {[ i := y ]} {[ i := x y ]}.
Proof. induction i; constructor; rewrite ?left_id; auto. Qed. Proof.
Lemma list_alter_singleton f i x : rewrite /singletonM /list_singletonM /=.
alter f i (list_singleton i x) = list_singleton i (f x). induction i; constructor; rewrite ?left_id; auto.
Proof. rewrite /list_singleton. induction i; f_equal/=; auto. Qed. Qed.
Global Instance list_singleton_persistent i x : Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}.
Persistent x Persistent (list_singleton i x). Proof.
Proof. by rewrite !persistent_total list_core_singleton=> ->. Qed. rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
Qed.
Global Instance list_singleton_persistent i (x : A) :
Persistent x Persistent {[ i := x ]}.
Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed.
(* Update *) (* Update *)
Lemma list_middle_updateP (P : A Prop) (Q : list A Prop) l1 x l2 : Lemma list_middle_updateP (P : A Prop) (Q : list A Prop) l1 x l2 :
...@@ -360,7 +362,7 @@ Section properties. ...@@ -360,7 +362,7 @@ Section properties.
Qed. Qed.
Lemma list_singleton_local_update i x y ml : Lemma list_singleton_local_update i x y ml :
x ~l~> y @ ml = (!! i) list_singleton i x ~l~> list_singleton i y @ ml. x ~l~> y @ ml = (!! i) {[ i := x ]} ~l~> {[ i := y ]} @ ml.
Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed. Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
End properties. End properties.
......
...@@ -109,9 +109,7 @@ Proof. induction 1; simpl; auto with I. Qed. ...@@ -109,9 +109,7 @@ Proof. induction 1; simpl; auto with I. Qed.
Section gmap. Section gmap.
Context `{Countable K} {A : Type}. Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A. Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types Φ Ψ : K A uPred M. Implicit Types Φ Ψ : K A uPred M.
Implicit Types P : uPred M.
Lemma big_sepM_mono Φ Ψ m1 m2 : Lemma big_sepM_mono Φ Ψ m1 m2 :
m2 m1 ( k x, m2 !! k = Some x Φ k x Ψ k x) m2 m1 ( k x, m2 !! k = Some x Φ k x Ψ k x)
...@@ -189,17 +187,16 @@ Section gmap. ...@@ -189,17 +187,16 @@ Section gmap.
Lemma big_sepM_fn_insert {B} (Ψ : K A B uPred M) (f : K B) m i x b : Lemma big_sepM_fn_insert {B} (Ψ : K A B uPred M) (f : K B) m i x b :
m !! i = None m !! i = None
([ map] ky <[i:=x]> m, Ψ k y (fn_insert i b f k)) ([ map] ky <[i:=x]> m, Ψ k y (<[i:=b]> f k))
(Ψ i x b [ map] ky m, Ψ k y (f k)). (Ψ i x b [ map] ky m, Ψ k y (f k)).
Proof. Proof.
intros. rewrite big_sepM_insert // fn_lookup_insert. intros. rewrite big_sepM_insert // fn_lookup_insert.
apply sep_proper, big_sepM_proper; auto=> k y ?. apply sep_proper, big_sepM_proper; auto=> k y ?.
by rewrite fn_lookup_insert_ne; last set_solver. by rewrite fn_lookup_insert_ne; last set_solver.
Qed. Qed.
Lemma big_sepM_fn_insert' (Φ : K uPred M) m i x P : Lemma big_sepM_fn_insert' (Φ : K uPred M) m i x P :
m !! i = None m !! i = None
([ map] ky <[i:=x]> m, (fn_insert i P Φ k)) (P [ map] ky m, Φ k). ([ map] ky <[i:=x]> m, <[i:=P]> Φ k) (P [ map] ky m, Φ k).
Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed. Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
Lemma big_sepM_sepM Φ Ψ m : Lemma big_sepM_sepM Φ Ψ m :
...@@ -303,17 +300,15 @@ Section gset. ...@@ -303,17 +300,15 @@ Section gset.
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed. Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_fn_insert {B} (Ψ : A B uPred M) f X x b : Lemma big_sepS_fn_insert {B} (Ψ : A B uPred M) f X x b :
x X x X
([ set] y {[ x ]} X, Ψ y (fn_insert x b f y)) ([ set] y {[ x ]} X, Ψ y (<[x:=b]> f y))
(Ψ x b [ set] y X, Ψ y (f y)). (Ψ x b [ set] y X, Ψ y (f y)).
Proof. Proof.
intros. rewrite big_sepS_insert // fn_lookup_insert. intros. rewrite big_sepS_insert // fn_lookup_insert.
apply sep_proper, big_sepS_proper; auto=> y ??. apply sep_proper, big_sepS_proper; auto=> y ??.
by rewrite fn_lookup_insert_ne; last set_solver. by rewrite fn_lookup_insert_ne; last set_solver.
Qed. Qed.
Lemma big_sepS_fn_insert' Φ X x P : Lemma big_sepS_fn_insert' Φ X x P :
x X x X ([ set] y {[ x ]} X, <[x:=P]> Φ y) (P [ set] y X, Φ y).
([ set] y {[ x ]} X, fn_insert x P Φ y) (P [ set] y X, Φ y).
Proof. apply (big_sepS_fn_insert (λ y, id)). Qed. Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
Lemma big_sepS_delete Φ X x : Lemma big_sepS_delete Φ X x :
......
...@@ -82,7 +82,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I : ...@@ -82,7 +82,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
Proof. Proof.
iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]". iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done. iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iExists (fn_insert i1 R1 (fn_insert i2 R2 Ψ)). iSplitL "HQR HPΨ". iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit. - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP"). iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done. iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
......
...@@ -11,7 +11,6 @@ Context {Σ : iFunctor}. ...@@ -11,7 +11,6 @@ Context {Σ : iFunctor}.
Implicit Types P Q : iProp heap_lang Σ. Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val iProp heap_lang Σ. Implicit Types Φ : val iProp heap_lang Σ.
Implicit Types ef : option expr. Implicit Types ef : option expr.
Implicit Types l : loc.
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *) (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
Lemma wp_bind {E e} K Φ : Lemma wp_bind {E e} K Φ :
...@@ -93,19 +92,19 @@ Proof. ...@@ -93,19 +92,19 @@ Proof.
intros; inv_head_step; eauto. intros; inv_head_step; eauto.
Qed. Qed.
Lemma wp_un_op E op li li' Φ : Lemma wp_un_op E op l l' Φ :
un_op_eval op li = Some li' un_op_eval op l = Some l'
(|={E}=> Φ (LitV li')) WP UnOp op (Lit li) @ E {{ Φ }}. (|={E}=> Φ (LitV l')) WP UnOp op (Lit l) @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit li') None) intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto. ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Qed. Qed.
Lemma wp_bin_op E op li1 li2 li' Φ : Lemma wp_bin_op E op l1 l2 l' Φ :
bin_op_eval op li1 li2 = Some li' bin_op_eval op l1 l2 = Some l'
(|={E}=> Φ (LitV li')) WP BinOp op (Lit li1) (Lit li2) @ E {{ Φ }}. (|={E}=> Φ (LitV l')) WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Proof. Proof.
intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit li') None) intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto. ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Qed. Qed.
......
...@@ -785,7 +785,7 @@ Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o)) ...@@ -785,7 +785,7 @@ Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
(** In this section we define operational type classes for the operations (** In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps. on maps. In the file [fin_maps] we will axiomatize finite maps.
The function look up [m !! k] should yield the element at key [k] in [m]. *) The function look up [m !! k] should yield the element at key [k] in [m]. *)
Class Lookup (K : Type) (M : Type Type) := lookup : {A}, K M A option A. Class Lookup (K A M : Type) := lookup: K M option A.
Instance: Params (@lookup) 4. Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope. Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
Notation "(!!)" := lookup (only parsing) : C_scope. Notation "(!!)" := lookup (only parsing) : C_scope.
...@@ -794,14 +794,13 @@ Notation "(!! i )" := (lookup i) (only parsing) : C_scope. ...@@ -794,14 +794,13 @@ Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch. Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
(** The singleton map *) (** The singleton map *)
Class SingletonM (K : Type) (M : Type Type) := Class SingletonM K A M := singletonM: K A M.
singletonM : {A}, K A M A.
Instance: Params (@singletonM) 5. Instance: Params (@singletonM) 5.
Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope. Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope.
(** The function insert [<[k:=a]>m] should update the element at key [k] with (** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *) value [a] in [m]. *)
Class Insert (K : Type) (M : Type Type) := insert : {A}, K A M A M A. Class Insert (K A M : Type) := insert: K A M M.
Instance: Params (@insert) 5. Instance: Params (@insert) 5.
Notation "<[ k := a ]>" := (insert k a) Notation "<[ k := a ]>" := (insert k a)
(at level 5, right associativity, format "<[ k := a ]>") : C_scope. (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
...@@ -810,14 +809,13 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch. ...@@ -810,14 +809,13 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
(** The function delete [delete k m] should delete the value at key [k] in (** The function delete [delete k m] should delete the value at key [k] in
[m]. If the key [k] is not a member of [m], the original map should be [m]. If the key [k] is not a member of [m], the original map should be
returned. *) returned. *)
Class Delete (K : Type) (M : Type Type) := delete : {A}, K M A M A. Class Delete (K M : Type) := delete: K M M.
Instance: Params (@delete) 5. Instance: Params (@delete) 4.
Arguments delete _ _ _ _ !_ !_ / : simpl nomatch. Arguments delete _ _ _ !_ !_ / : simpl nomatch.
(** The function [alter f k m] should update the value at key [k] using the (** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value. *) function [f], which is called with the original value. *)
Class Alter (K : Type) (M : Type Type) := Class Alter (K A M : Type) := alter: (A A) K M M.
alter : {A}, (A A) K M A M A.
Instance: Params (@alter) 5. Instance: Params (@alter) 5.
Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch. Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
...@@ -825,16 +823,16 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch. ...@@ -825,16 +823,16 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
function [f], which is called with the original value at key [k] or [None] function [f], which is called with the original value at key [k] or [None]
if [k] is not a member of [m]. The value at [k] should be deleted if [f] if [k] is not a member of [m]. The value at [k] should be deleted if [f]
yields [None]. *) yields [None]. *)
Class PartialAlter (K : Type) (M : Type Type) := Class PartialAlter (K A M : Type) :=
partial_alter : {A}, (option A option A) K M A M A. partial_alter: (option A option A) K M M.
Instance: Params (@partial_alter) 4. Instance: Params (@partial_alter) 4.
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch. Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
(** The function [dom C m] should yield the domain of [m]. That is a finite (** The function [dom C m] should yield the domain of [m]. That is a finite
collection of type [C] that contains the keys that are a member of [m]. *) collection of type [C] that contains the keys that are a member of [m]. *)
Class Dom (M : Type Type) (C : Type) := dom : {A}, M A C. Class Dom (M C : Type) := dom: M C.
Instance: Params (@dom) 4. Instance: Params (@dom) 3.
Arguments dom {_} _ {_ _} !_ / : simpl nomatch, clear implicits. Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits.
(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*) constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
...@@ -846,27 +844,39 @@ Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch. ...@@ -846,27 +844,39 @@ Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch.
(** The function [union_with f m1 m2] is supposed to yield the union of [m1] (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
and [m2] using the function [f] to combine values of members that are in and [m2] using the function [f] to combine values of members that are in
both [m1] and [m2]. *) both [m1] and [m2]. *)
Class UnionWith (M : Type Type) := Class UnionWith (A M : Type) :=
union_with : {A}, (A A option A) M A M A M A. union_with: (A A option A) M M M.
Instance: Params (@union_with) 3. Instance: Params (@union_with) 3.
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch. Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
(** Similarly for intersection and difference. *) (** Similarly for intersection and difference. *)
Class IntersectionWith (M : Type Type) := Class IntersectionWith (A M : Type) :=
intersection_with : {A}, (A A option A) M A M A M A. intersection_with: (A A option A) M M M.
Instance: Params (@intersection_with) 3. Instance: Params (@intersection_with) 3.
Arguments intersection_with {_ _