From 20b4ae55bdf00edb751ccdab3eb876cb9b13c99f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Jul 2016 12:56:27 +0200
Subject: [PATCH] Make the types of the finite map type classes more specific.
This makes type checking more directed, and somewhat more predictable.
On the downside, it makes it impossible to declare the singleton on
lists as an instance of SingletonM and the insert and alter operations
on functions as instances of Alter and Insert. However, these were not
used often anyway.
---
algebra/gmap.v | 17 +++++---
algebra/list.v | 80 +++++++++++++++++------------------
algebra/upred_big_op.v | 13 ++++--
heap_lang/lib/barrier/proof.v | 2 +-
heap_lang/lifting.v | 17 ++++----
prelude/base.v | 56 ++++++++++--------------
prelude/coPset.v | 4 +-
prelude/fin_map_dom.v | 7 ++-
prelude/fin_maps.v | 76 ++++++++++++++++-----------------
prelude/functions.v | 26 ++++++------
prelude/gmap.v | 9 ++--
prelude/list.v | 24 +++++------
prelude/mapset.v | 2 +-
prelude/natmap.v | 8 ++--
prelude/nmap.v | 8 ++--
prelude/option.v | 8 ++--
prelude/pmap.v | 14 +++---
prelude/zmap.v | 8 ++--
program_logic/boxes.v | 2 +-
program_logic/resources.v | 2 +-
20 files changed, 189 insertions(+), 194 deletions(-)
diff --git a/algebra/gmap.v b/algebra/gmap.v
index c0e59099a..b7884958e 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -47,7 +47,7 @@ Proof.
by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
Qed.
Global Instance insert_ne i n :
- Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
+ Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K) i).
Proof.
intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
[by constructor|by apply lookup_ne].
@@ -56,7 +56,7 @@ Global Instance singleton_ne i n :
Proper (dist n ==> dist n) (singletonM i : A → gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
Global Instance delete_ne i n :
- Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
+ Proper (dist n ==> dist n) (delete (M:=gmap K) i).
Proof.
intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
[by constructor|by apply lookup_ne].
@@ -183,10 +183,12 @@ Arguments gmapUR _ {_ _} _.
Section properties.
Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A.
+Implicit Types mm : option (gmap K A).
Implicit Types i : K.
Implicit Types x y : A.
-Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
+Lemma lookup_opM m1 mm2 i :
+ (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i) : option A).
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.
@@ -343,7 +345,8 @@ Section freshness.
End freshness.
Lemma insert_local_update m i x y mf :
- x ~l~> y @ mf ≫= (!! i) → <[i:=x]>m ~l~> <[i:=y]>m @ mf.
+ x ~l~> y @ mf ≫= (!! i) →
+ (<[i:=x]>m : gmap K A) ~l~> <[i:=y]>m @ mf.
Proof.
intros [Hxy Hxy']; split.
- intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
@@ -356,7 +359,8 @@ Proof.
Qed.
Lemma singleton_local_update i x y mf :
- x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf.
+ x ~l~> y @ mf ≫= (!! i) →
+ ({[ i := x ]} : gmap K A) ~l~> {[ i := y ]} @ mf.
Proof. apply insert_local_update. Qed.
Lemma alloc_singleton_local_update m i x mf :
@@ -371,7 +375,8 @@ Proof.
Qed.
Lemma alloc_unit_singleton_local_update i x mf :
- mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf.
+ mf ≫= (!! i) = None → ✓ x →
+ (∅:gmap K A) ~l~> {[ i := x ]} @ mf.
Proof.
intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
Qed.
diff --git a/algebra/list.v b/algebra/list.v
index 3ab4d27c2..415af3315 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -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 drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _.
Global Instance list_lookup_ne n i :
- Proper (dist n ==> dist n) (lookup (M:=list A) i).
+ Proper (dist n ==> dist n) (lookup (M:=list) i).
Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
Global Instance list_alter_ne n f i :
Proper (dist n ==> dist n) f →
- Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
+ Proper (dist n ==> dist n) (alter (M:=list) f i) := _.
Global Instance list_insert_ne n i :
- Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _.
+ Proper (dist n ==> dist n ==> dist n) (insert (M:=list) i) := _.
Global Instance list_inserts_ne n i :
Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _.
Global Instance list_delete_ne n i :
- Proper (dist n ==> dist n) (delete (M:=list A) i) := _.
+ Proper (dist n ==> dist n) (delete (M:=list) i) := _.
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.
Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
@@ -236,17 +236,20 @@ End cmra.
Arguments listR : clear implicits.
Arguments listUR : clear implicits.
-Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
+Definition list_singleton {A : ucmraT} (n : nat) (x : A) : list A :=
replicate n ∅ ++ [x].
Section properties.
Context {A : ucmraT}.
- Implicit Types l : list A.
+ Implicit Types l k : list A.
+ Implicit Types ml mk : option (list A).
Implicit Types x y z : A.
+ Implicit Types i : nat.
Local Arguments op _ _ !_ !_ / : simpl nomatch.
Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
- Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i)).
+ Lemma list_lookup_opM l mk i :
+ (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i) : option A).
Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.
Lemma list_op_app l1 l2 l3 :
@@ -266,57 +269,52 @@ Section properties.
Lemma replicate_valid n (x : A) : ✓ x → ✓ replicate n x.
Proof. apply Forall_replicate. Qed.
- Global Instance list_singletonM_ne n i :
- Proper (dist n ==> dist n) (@list_singletonM A i).
+ Global Instance list_singleton_ne n i :
+ Proper (dist n ==> dist n) (@list_singleton A i).
Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
- Global Instance list_singletonM_proper i :
- Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
+ Global Instance list_singleton_proper i :
+ Proper ((≡) ==> (≡)) (list_singleton i) := ne_proper _.
- Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x.
+ Lemma elem_of_list_singleton i z x : z ∈ list_singleton i x → z = ∅ ∨ z = x.
Proof.
rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
Qed.
- Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x.
+ Lemma list_lookup_singleton i x : list_singleton i x !! i = Some x.
Proof. induction i; by f_equal/=. Qed.
- Lemma list_lookup_singletonM_ne i j x :
- i ≠j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅.
+ Lemma list_lookup_singleton_ne i j x :
+ i ≠j → list_singleton i x !! j = None ∨ list_singleton i x !! j = Some ∅.
Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
- Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x.
+ Lemma list_singleton_validN n i x : ✓{n} (list_singleton i x) ↔ ✓{n} x.
Proof.
rewrite list_lookup_validN. split.
- { move=> /(_ i). by rewrite list_lookup_singletonM. }
+ { move=> /(_ i). by rewrite list_lookup_singleton. }
intros Hx j; destruct (decide (i = j)); subst.
- - by rewrite list_lookup_singletonM.
- - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
+ - by rewrite list_lookup_singleton.
+ - destruct (list_lookup_singleton_ne i j x) as [Hi|Hi]; first done;
rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
Qed.
- 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.
+ Lemma list_singleton_valid i x : ✓ (list_singleton i x) ↔ ✓ x.
Proof.
- rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
+ rewrite !cmra_valid_validN. by setoid_rewrite list_singleton_validN.
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_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
+ Lemma list_core_singleton i x :
+ core (list_singleton i x) ≡ list_singleton i (core x).
Proof.
- rewrite /singletonM /list_singletonM.
+ rewrite /list_singleton.
by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ∅).
Qed.
- Lemma list_op_singletonM i (x y : A) :
- {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
- Proof.
- rewrite /singletonM /list_singletonM /=.
- induction i; constructor; rewrite ?left_id; auto.
- Qed.
- Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}.
- Proof.
- 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.
+ Lemma list_op_singleton i x y :
+ list_singleton i x ⋅ list_singleton i y ≡ list_singleton i (x ⋅ y).
+ Proof. induction i; constructor; rewrite ?left_id; auto. Qed.
+ Lemma list_alter_singleton f i x :
+ alter f i (list_singleton i x) = list_singleton i (f x).
+ Proof. rewrite /list_singleton. induction i; f_equal/=; auto. Qed.
+ Global Instance list_singleton_persistent i x :
+ Persistent x → Persistent (list_singleton i x).
+ Proof. by rewrite !persistent_total list_core_singleton=> ->. Qed.
(* Update *)
Lemma list_middle_updateP (P : A → Prop) (Q : list A → Prop) l1 x l2 :
@@ -362,7 +360,7 @@ Section properties.
Qed.
Lemma list_singleton_local_update i x y ml :
- x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
+ x ~l~> y @ ml ≫= (!! i) → list_singleton i x ~l~> list_singleton i y @ ml.
Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
End properties.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 85e2b3346..fff429f16 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -109,7 +109,9 @@ Proof. induction 1; simpl; auto with I. Qed.
Section gmap.
Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A.
+ Implicit Types i : K.
Implicit Types Φ Ψ : K → A → uPred M.
+ Implicit Types P : uPred M.
Lemma big_sepM_mono Φ Ψ m1 m2 :
m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
@@ -187,16 +189,17 @@ Section gmap.
Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b :
m !! i = None →
- ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))
+ ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (fn_insert i b f k))
⊣⊢ (Ψ i x b ★ [★ map] k↦y ∈ m, Ψ k y (f k)).
Proof.
intros. rewrite big_sepM_insert // fn_lookup_insert.
apply sep_proper, big_sepM_proper; auto=> k y ?.
by rewrite fn_lookup_insert_ne; last set_solver.
Qed.
+
Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
m !! i = None →
- ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
+ ([★ map] k↦y ∈ <[i:=x]> m, (fn_insert i P Φ k)) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
Lemma big_sepM_sepM Φ Ψ m :
@@ -300,15 +303,17 @@ Section gset.
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 :
x ∉ X →
- ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y))
+ ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (fn_insert x b f y))
⊣⊢ (Ψ x b ★ [★ set] y ∈ X, Ψ y (f 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_fn_insert' Φ X x P :
- x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y).
+ x ∉ X →
+ ([★ set] y ∈ {[ x ]} ∪ X, fn_insert x P Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y).
Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
Lemma big_sepS_delete Φ X x :
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 879ac67ca..0251c484b 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -82,7 +82,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
Proof.
iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
- iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
+ iExists (fn_insert i1 R1 (fn_insert i2 R2 Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 24eb4d3a6..5edc2f180 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -11,6 +11,7 @@ Context {Σ : iFunctor}.
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val → iProp heap_lang Σ.
Implicit Types ef : option expr.
+Implicit Types l : loc.
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
Lemma wp_bind {E e} K Φ :
@@ -92,19 +93,19 @@ Proof.
intros; inv_head_step; eauto.
Qed.
-Lemma wp_un_op E op l l' Φ :
- un_op_eval op l = Some l' →
- ▷ (|={E}=> Φ (LitV l')) ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
+Lemma wp_un_op E op li li' Φ :
+ un_op_eval op li = Some li' →
+ ▷ (|={E}=> Φ (LitV li')) ⊢ WP UnOp op (Lit li) @ E {{ Φ }}.
Proof.
- intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
+ intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit li') None)
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Qed.
-Lemma wp_bin_op E op l1 l2 l' Φ :
- bin_op_eval op l1 l2 = Some l' →
- ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+Lemma wp_bin_op E op li1 li2 li' Φ :
+ bin_op_eval op li1 li2 = Some li' →
+ ▷ (|={E}=> Φ (LitV li')) ⊢ WP BinOp op (Lit li1) (Lit li2) @ E {{ Φ }}.
Proof.
- intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
+ intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit li') None)
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Qed.
diff --git a/prelude/base.v b/prelude/base.v
index b046cf8e8..40e58b18e 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -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
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]. *)
-Class Lookup (K A M : Type) := lookup: K → M → option A.
+Class Lookup (K : Type) (M : Type → Type) := lookup : ∀ {A}, K → M A → option A.
Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
Notation "(!!)" := lookup (only parsing) : C_scope.
@@ -794,13 +794,14 @@ Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
(** The singleton map *)
-Class SingletonM K A M := singletonM: K → A → M.
+Class SingletonM (K : Type) (M : Type → Type) :=
+ singletonM : ∀ {A}, K → A → M A.
Instance: Params (@singletonM) 5.
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
value [a] in [m]. *)
-Class Insert (K A M : Type) := insert: K → A → M → M.
+Class Insert (K : Type) (M : Type → Type) := insert : ∀ {A}, K → A → M A → M A.
Instance: Params (@insert) 5.
Notation "<[ k := a ]>" := (insert k a)
(at level 5, right associativity, format "<[ k := a ]>") : C_scope.
@@ -809,13 +810,14 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
(** 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
returned. *)
-Class Delete (K M : Type) := delete: K → M → M.
-Instance: Params (@delete) 4.
-Arguments delete _ _ _ !_ !_ / : simpl nomatch.
+Class Delete (K : Type) (M : Type → Type) := delete : ∀ {A}, K → M A → M A.
+Instance: Params (@delete) 5.
+Arguments delete _ _ _ _ !_ !_ / : simpl nomatch.
(** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value. *)
-Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
+Class Alter (K : Type) (M : Type → Type) :=
+ alter : ∀ {A}, (A → A) → K → M A → M A.
Instance: Params (@alter) 5.
Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
@@ -823,16 +825,16 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
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]
yields [None]. *)
-Class PartialAlter (K A M : Type) :=
- partial_alter: (option A → option A) → K → M → M.
+Class PartialAlter (K : Type) (M : Type → Type) :=
+ partial_alter : ∀ {A}, (option A → option A) → K → M A → M A.
Instance: Params (@partial_alter) 4.
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
(** 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]. *)
-Class Dom (M C : Type) := dom: M → C.
-Instance: Params (@dom) 3.
-Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits.
+Class Dom (M : Type → Type) (C : Type) := dom : ∀ {A}, M A → C.
+Instance: Params (@dom) 4.
+Arguments dom {_} _ {_ _} !_ / : simpl nomatch, clear implicits.
(** 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)].*)
@@ -844,39 +846,27 @@ Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch.
(** 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
both [m1] and [m2]. *)
-Class UnionWith (A M : Type) :=
- union_with: (A → A → option A) → M → M → M.
+Class UnionWith (M : Type → Type) :=
+ union_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
Instance: Params (@union_with) 3.
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
(** Similarly for intersection and difference. *)
-Class IntersectionWith (A M : Type) :=
- intersection_with: (A → A → option A) → M → M → M.
+Class IntersectionWith (M : Type → Type) :=
+ intersection_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
Instance: Params (@intersection_with) 3.
Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.
-Class DifferenceWith (A M : Type) :=
- difference_with: (A → A → option A) → M → M → M.
+Class DifferenceWith (M : Type → Type) :=
+ difference_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
Instance: Params (@difference_with) 3.
Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
-Definition intersection_with_list `{IntersectionWith A M}
- (f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
+Definition intersection_with_list `{IntersectionWith M} {A}
+ (f : A → A → option A) : M A → list (M A) → M A :=
+ fold_right (intersection_with f).
Arguments intersection_with_list _ _ _ _ _ !_ /.
-Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
-Instance: Params (@lookupE) 6.
-Notation "m !!{ Γ } i" := (lookupE Γ i m)
- (at level 20, format "m !!{ Γ } i") : C_scope.
-Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope.
-Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch.
-
-Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
-Instance: Params (@insertE) 6.
-Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
- (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
-Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.
-
(** * Axiomatization of collections *)
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
diff --git a/prelude/coPset.v b/prelude/coPset.v
index 9e37b07d0..2a572ec97 100644
--- a/prelude/coPset.v
+++ b/prelude/coPset.v
@@ -326,13 +326,13 @@ Proof.
Qed.
(** * Domain of finite maps *)
-Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m).
+Instance Pmap_dom_coPset : Dom Pmap coPset := λ A m, of_Pset (dom _ m).
Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
Proof.
split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
by rewrite elem_of_of_Pset, elem_of_dom.
Qed.
-Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
+Instance gmap_dom_coPset : Dom (gmap positive) coPset := λ A m,
of_gset (dom _ m).
Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
Proof.
diff --git a/prelude/fin_map_dom.v b/prelude/fin_map_dom.v
index afb29ae11..42d0a40ec 100644
--- a/prelude/fin_map_dom.v
+++ b/prelude/fin_map_dom.v
@@ -5,10 +5,9 @@ maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *)
From iris.prelude Require Export collections fin_maps.
-Class FinMapDom K M D `{FMap M,
- ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
- OMap M, Merge M, ∀ A, FinMapToList K A (M A), ∀ i j : K, Decision (i = j),
- ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D,
+Class FinMapDom K M D `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M,
+ OMap M, Merge M, FinMapToList K M, ∀ i j : K, Decision (i = j),
+ Dom M D, ElemOf K D, Empty D, Singleton K D,
Union D, Intersection D, Difference D} := {
finmap_dom_map :>> FinMap K M;
finmap_dom_collection :>> Collection K D;
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 5f4b4bcae..574e2c334 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -23,11 +23,11 @@ prove well founded recursion on finite maps. *)
which enables us to give a generic implementation of [union_with],
[intersection_with], and [difference_with]. *)
-Class FinMapToList K A M := map_to_list: M → list (K * A).
+Class FinMapToList (K : Type) (M : Type → Type) :=
+ map_to_list : ∀ {A}, M A → list (K * A).
-Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
- PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A),
- ∀ i j : K, Decision (i = j)} := {
+Class FinMap K M `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M,
+ OMap M, Merge M, FinMapToList K M, ∀ i j : K, Decision (i = j)} := {
map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2;
lookup_empty {A} i : (∅ : M A) !! i = None;
lookup_partial_alter {A} f (m : M A) i :
@@ -48,47 +48,47 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
finite map implementations. These generic implementations do not cause a
significant performance loss to make including them in the finite map interface
worthwhile. *)
-Instance map_insert `{PartialAlter K A M} : Insert K A M :=
- λ i x, partial_alter (λ _, Some x) i.
-Instance map_alter `{PartialAlter K A M} : Alter K A M :=
- λ f, partial_alter (fmap f).
-Instance map_delete `{PartialAlter K A M} : Delete K M :=
- partial_alter (λ _, None).
-Instance map_singleton `{PartialAlter K A M, Empty M} :
- SingletonM K A M := λ i x, <[i:=x]> ∅.
+Instance map_insert `{PartialAlter K M} : Insert K M :=
+ λ A i x, partial_alter (λ _, Some x) i.
+Instance map_alter `{PartialAlter K M} : Alter K M :=
+ λ A f, partial_alter (fmap f).
+Instance map_delete `{PartialAlter K M} : Delete K M :=
+ λ A, partial_alter (λ _, None).
+Instance map_singleton `{PartialAlter K M, ∀ A, Empty (M A)} : SingletonM K M :=
+ λ A i x, <[i:=x]> ∅.
-Definition map_of_list `{Insert K A M, Empty M} : list (K * A) → M :=
+Definition map_of_list `{Insert K M, Empty (M A)} : list (K * A) → M A :=
fold_right (λ p, <[p.1:=p.2]>) ∅.
-Definition map_of_collection `{Elements K C, Insert K A M, Empty M}
- (f : K → option A) (X : C) : M :=
+Definition map_of_collection `{Elements K C, Insert K M, Empty (M A)}
+ (f : K → option A) (X : C) : M A :=
map_of_list (omap (λ i, (i,) <$> f i) (elements X)).
-Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
- λ f, merge (union_with f).
-Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
- λ f, merge (intersection_with f).
-Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
- λ f, merge (difference_with f).
+Instance map_union_with `{Merge M} : UnionWith M :=
+ λ A f, merge (union_with f).
+Instance map_intersection_with `{Merge M} : IntersectionWith M :=
+ λ A f, merge (intersection_with f).
+Instance map_difference_with `{Merge M} : DifferenceWith M :=
+ λ A f, merge (difference_with f).
-Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 18 :=
+Instance map_equiv `{Lookup K M, Equiv A} : Equiv (M A) | 18 :=
λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
(** The relation [intersection_forall R] on finite maps describes that the
relation [R] holds for each pair in the intersection. *)
-Definition map_Forall `{Lookup K A M} (P : K → A → Prop) : M → Prop :=
+Definition map_Forall `{Lookup K M} {A} (P : K → A → Prop) : M A → Prop :=
λ m, ∀ i x, m !! i = Some x → P i x.
-Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : A → B → Prop)
+Definition map_relation `{Lookup K M} {A B} (R : A → B → Prop)
(P : A → Prop) (Q : B → Prop) (m1 : M A) (m2 : M B) : Prop := ∀ i,
option_relation R P Q (m1 !! i) (m2 !! i).
-Definition map_included `{∀ A, Lookup K A (M A)} {A}
+Definition map_included `{Lookup K M} {A}
(R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
-Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
+Definition map_disjoint `{Lookup K M} {A} : relation (M A) :=
map_relation (λ _ _, False) (λ _, True) (λ _, True).
Infix "⊥ₘ" := map_disjoint (at level 70) : C_scope.
Hint Extern 0 (_ ⊥ₘ _) => symmetry; eassumption.
Notation "( m ⊥ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
Notation "(.⊥ₘ m )" := (λ m2, m2 ⊥ₘ m) (only parsing) : C_scope.
-Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
+Instance map_subseteq `{Lookup K M} {A} : SubsetEq (M A) :=
map_included (=).
(** The union of two finite maps only has a meaningful definition for maps
@@ -106,8 +106,8 @@ Instance map_difference `{Merge M} {A} : Difference (M A) :=
(** A stronger variant of map that allows the mapped function to use the index
of the elements. Implemented by conversion to lists, so not very efficient. *)
-Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
- ∀ A, FinMapToList K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B :=
+Definition map_imap `{Insert K M, ∀ A, Empty (M A),
+ FinMapToList K M} {A B} (f : K → A → option B) (m : M A) : M B :=
map_of_list (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)).
(** * Theorems *)
@@ -124,27 +124,25 @@ Section setoid.
- by intros m1 m2 ? i.
- by intros m1 m2 m3 ?? i; trans (m2 !! i).
Qed.
- Global Instance lookup_proper (i : K) :
- Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
+ Global Instance lookup_proper (i: K) : Proper ((≡) ==> (≡)) (lookup (M:=M) i).
Proof. by intros m1 m2 Hm. Qed.
Global Instance partial_alter_proper :
- Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M A)).
+ Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M)).
Proof.
by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
try apply Hf; apply lookup_proper.
Qed.
Global Instance insert_proper (i : K) :
- Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M A) i).
+ Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M) i).
Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
- Global Instance singleton_proper k :
- Proper ((≡) ==> (≡)) (singletonM k : A → M A).
+ Global Instance singleton_proper (i : K) :
+ Proper ((≡) ==> (≡)) (singletonM (M:=M) i).
Proof. by intros ???; apply insert_proper. Qed.
- Global Instance delete_proper (i : K) :
- Proper ((≡) ==> (≡)) (delete (M:=M A) i).
+ Global Instance delete_proper (i: K) : Proper ((≡) ==> (≡)) (delete (M:=M) i).
Proof. by apply partial_alter_proper; [constructor|]. Qed.
Global Instance alter_proper :
- Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (A:=A) (M:=M A)).
+ Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (M:=M)).
Proof.
intros ?? Hf; apply partial_alter_proper.
by destruct 1; constructor; apply Hf.
@@ -156,7 +154,7 @@ Section setoid.
by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
Qed.
Global Instance union_with_proper :
- Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M A)).
+ Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M)).
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor].
diff --git a/prelude/functions.v b/prelude/functions.v
index 935d1b448..8d401dec0 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -2,10 +2,10 @@ From iris.prelude Require Export base tactics.
Section definitions.
Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
- Global Instance fn_insert : Insert A T (A → T) :=
- λ a t f b, if decide (a = b) then t else f b.
- Global Instance fn_alter : Alter A T (A → T) :=
- λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b.
+ Definition fn_insert (a : A) (t : T) (f : A → T) : A → T := λ b,
+ if decide (a = b) then t else f b.
+ Definition fn_alter (g : T → T) (a : A) (f : A → T) : A → T := λ b,
+ if decide (a = b) then g (f a) else f b.
End definitions.
(* TODO: For now, we only have the properties here that do not need a notion
@@ -14,17 +14,17 @@ End definitions.
Section functions.
Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
- Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t.
- Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed.
+ Lemma fn_lookup_insert (f : A → T) a t : fn_insert a t f a = t.
+ Proof. unfold fn_insert. by destruct (decide (a = a)). Qed.
Lemma fn_lookup_insert_rev (f : A → T) a t1 t2 :
- <[a:=t1]>f a = t2 → t1 = t2.
+ fn_insert a t1 f a = t2 → t1 = t2.
Proof. rewrite fn_lookup_insert. congruence. Qed.
- Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠b → <[a:=t]>f b = f b.
- Proof. unfold insert, fn_insert. by destruct (decide (a = b)). Qed.
+ Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠b → fn_insert a t f b = f b.
+ Proof. unfold fn_insert. by destruct (decide (a = b)). Qed.
- Lemma fn_lookup_alter (g : T → T) (f : A → T) a : alter g a f a = g (f a).
- Proof. unfold alter, fn_alter. by destruct (decide (a = a)). Qed.
+ Lemma fn_lookup_alter (g : T → T) (f : A → T) a : fn_alter g a f a = g (f a).
+ Proof. unfold fn_alter. by destruct (decide (a = a)). Qed.
Lemma fn_lookup_alter_ne (g : T → T) (f : A → T) a b :
- a ≠b → alter g a f b = f b.
- Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
+ a ≠b → fn_alter g a f b = f b.
+ Proof. unfold fn_alter. by destruct (decide (a = b)). Qed.
End functions.
diff --git a/prelude/gmap.v b/prelude/gmap.v
index bf74baaaf..1d86a6950 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -30,7 +30,7 @@ Proof.
Defined.
(** * Operations on the data structure *)
-Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
+Instance gmap_lookup `{Countable K} : Lookup K (gmap K) := λ A i m,
let (m,_) := m in m !! encode i.
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
@@ -40,8 +40,7 @@ Proof.
- rewrite decode_encode; eauto.
- rewrite lookup_partial_alter_ne by done. by apply Hm.
Qed.
-Instance gmap_partial_alter `{Countable K} {A} :
- PartialAlter K A (gmap K A) := λ f i m,
+Instance gmap_partial_alter `{Countable K} : PartialAlter K (gmap K) := λ A f i m,
let (m,Hm) := m in GMap (partial_alter f (encode i) m)
(bool_decide_pack _ (gmap_partial_alter_wf f m i
(bool_decide_unpack _ Hm))).
@@ -70,7 +69,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
GMap (merge f' m1 m2) (bool_decide_pack _ (gmap_merge_wf f _ _
(bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
-Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
+Instance gmap_to_list `{Countable K} : FinMapToList K (gmap K) := λ A m,
let (m,_) := m in omap (λ ix : positive * A,
let (i,x) := ix in (,x) <$> decode i) (map_to_list m).
@@ -114,7 +113,7 @@ Qed.
(** * Finite sets *)
Notation gset K := (mapset (gmap K)).
-Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
+Instance gset_dom `{Countable K} : Dom (gmap K) (gset K) := mapset_dom.
Instance gset_dom_spec `{Countable K} :
FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
diff --git a/prelude/list.v b/prelude/list.v
index 59b263318..12dc6a82a 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -57,15 +57,15 @@ Existing Instance list_equiv.
(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
in case [i] is out of bounds. *)
-Instance list_lookup {A} : Lookup nat A (list A) :=
- fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in
+Instance list_lookup : Lookup nat list :=
+ fix go A i l {struct l} : option A := let _ : Lookup _ _ := @go in
match l with
| [] => None | x :: l => match i with 0 => Some x | S i => l !! i end
end.
(** The operation [alter f i l] applies the function [f] to the [i]th element
of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_alter {A} : Alter nat A (list A) := λ f,
+Instance list_alter : Alter nat list := λ A f,
fix go i l {struct l} :=
match l with
| [] => []
@@ -74,8 +74,8 @@ Instance list_alter {A} : Alter nat A (list A) := λ f,
(** The operation [<[i:=x]> l] overwrites the element at position [i] with the
value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_insert {A} : Insert nat A (list A) :=
- fix go i y l {struct l} := let _ : Insert _ _ _ := @go in
+Instance list_insert : Insert nat list :=
+ fix go A i y l {struct l} := let _ : Insert _ _ := @go in
match l with
| [] => []
| x :: l => match i with 0 => y :: l | S i => x :: <[i:=y]>l end
@@ -90,11 +90,11 @@ Instance: Params (@list_inserts) 1.
(** The operation [delete i l] removes the [i]th element of [l] and moves
all consecutive elements one position ahead. In case [i] is out of bounds,
the list is returned unchanged. *)
-Instance list_delete {A} : Delete nat (list A) :=
- fix go (i : nat) (l : list A) {struct l} : list A :=
+Instance list_delete : Delete nat list :=
+ fix go A (i : nat) (l : list A) {struct l} : list A :=
match l with
| [] => []
- | x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end
+ | x :: l => match i with 0 => l | S i => x :: @delete _ _ go _ i l end
end.
(** The function [option_list o] converts an element [Some x] into the
@@ -2733,13 +2733,13 @@ Section setoid.
Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
Global Instance list_lookup_proper i :
- Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
+ Proper ((≡) ==> (≡)) (lookup (M:=list) i).
Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
Global Instance list_alter_proper f i :
- Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
+ Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list) f i).
Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
Global Instance list_insert_proper i :
- Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i).
+ Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list) i).
Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
Global Instance list_inserts_proper i :
Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
@@ -2748,7 +2748,7 @@ Section setoid.
induction Hk; intros ????; simpl; try f_equiv; naive_solver.
Qed.
Global Instance list_delete_proper i :
- Proper ((≡) ==> (≡)) (delete (M:=list A) i).
+ Proper ((≡) ==> (≡)) (delete (M:=list) i).
Proof. induction i; destruct 1; try constructor; eauto. Qed.
Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
Proof. destruct 1; by constructor. Qed.
diff --git a/prelude/mapset.v b/prelude/mapset.v
index 5a3dd7188..17282118a 100644
--- a/prelude/mapset.v
+++ b/prelude/mapset.v
@@ -118,7 +118,7 @@ Proof.
- destruct (Is_true_reflect (f a)); naive_solver.
- naive_solver.
Qed.
-Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
+Instance mapset_dom : Dom M (mapset M) := λ A, mapset_dom_with (λ _, true).
Instance mapset_dom_spec: FinMapDom K M (mapset M).
Proof.
split; try apply _. intros. unfold dom, mapset_dom, is_Some.
diff --git a/prelude/natmap.v b/prelude/natmap.v
index 5845901a6..a79f1b982 100644
--- a/prelude/natmap.v
+++ b/prelude/natmap.v
@@ -44,7 +44,7 @@ Global Instance natmap_eq_dec `{∀ x y : A, Decision (x = y)}
end.
Instance natmap_empty {A} : Empty (natmap A) := NatMap [] I.
-Instance natmap_lookup {A} : Lookup nat A (natmap A) := λ i m,
+Instance natmap_lookup : Lookup nat natmap := λ A i m,
let (l,_) := m in mjoin (l !! i).
Fixpoint natmap_singleton_raw {A} (i : nat) (x : A) : natmap_raw A :=
@@ -92,7 +92,7 @@ Proof.
revert i. induction l; [intro | intros [|?]]; simpl; repeat case_match;
eauto using natmap_singleton_wf, natmap_cons_canon_wf, natmap_wf_inv.
Qed.
-Instance natmap_alter {A} : PartialAlter nat A (natmap A) := λ f i m,
+Instance natmap_alter : PartialAlter nat natmap := λ A f i m,
let (l,Hl) := m in NatMap _ (natmap_alter_wf f i l Hl).
Lemma natmap_lookup_alter_raw {A} (f : option A → option A) i l :
mjoin (natmap_alter_raw f i l !! i) = f (mjoin (l !! i)).
@@ -188,7 +188,7 @@ Proof.
revert i. induction l as [|[?|] ? IH]; simpl; try constructor; auto.
rewrite natmap_elem_of_to_list_raw_aux. intros (?&?&?). lia.
Qed.
-Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
+Instance natmap_to_list : FinMapToList nat natmap := λ A m,
let (l,_) := m in natmap_to_list_raw 0 l.
Definition natmap_map_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B :=
@@ -256,7 +256,7 @@ Qed.
(** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
Notation natset := (mapset natmap).
-Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
+Instance natmap_dom : Dom natmap natset := mapset_dom.
Instance: FinMapDom nat natmap natset := mapset_dom_spec.
(* Fixpoint avoids this definition from being unfolded *)
diff --git a/prelude/nmap.v b/prelude/nmap.v
index 11fead13c..c3c42ea93 100644
--- a/prelude/nmap.v
+++ b/prelude/nmap.v
@@ -22,17 +22,17 @@ Proof.
Defined.
Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
Global Opaque Nempty.
-Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
+Instance Nlookup : Lookup N Nmap := λ A i t,
match i with
| N0 => Nmap_0 t
| Npos p => Nmap_pos t !! p
end.
-Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
+Instance Npartial_alter : PartialAlter N Nmap := λ A f i t,
match i, t with
| N0, NMap o t => NMap (f o) t
| Npos p, NMap o t => NMap o (partial_alter f p t)
end.
-Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
+Instance Nto_list : FinMapToList N Nmap := λ A t,
match t with
| NMap o t =>
default [] o (λ x, [(0,x)]) ++ (prod_map Npos id <$> map_to_list t)
@@ -82,7 +82,7 @@ Qed.
(** * Finite sets *)
(** We construct sets of [N]s satisfying extensional equality. *)
Notation Nset := (mapset Nmap).
-Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
+Instance Nmap_dom : Dom Nmap Nset := mapset_dom.
Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
(** * Fresh numbers *)
diff --git a/prelude/option.v b/prelude/option.v
index 0f972ca16..7c4142070 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -239,16 +239,16 @@ Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /.
(** * Union, intersection and difference *)
-Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
+Instance option_union_with : UnionWith option := λ A f mx my,
match mx, my with
| Some x, Some y => f x y
| Some x, None => Some x
| None, Some y => Some y
| None, None => None
end.
-Instance option_intersection_with {A} : IntersectionWith A (option A) :=
- λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end.
-Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my,
+Instance option_intersection_with : IntersectionWith option := λ A f mx my,
+ match mx, my with Some x, Some y => f x y | _, _ => None end.
+Instance option_difference_with : DifferenceWith option := λ A f mx my,
match mx, my with
| Some x, Some y => f x y
| Some x, None => Some x
diff --git a/prelude/pmap.v b/prelude/pmap.v
index 483eac8b1..1416ed314 100644
--- a/prelude/pmap.v
+++ b/prelude/pmap.v
@@ -52,9 +52,9 @@ Local Hint Resolve PNode_wf.
(** Operations *)
Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
-Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
- fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
- let _ : Lookup _ _ _ := @go in
+Instance Plookup_raw : Lookup positive Pmap_raw :=
+ fix go A (i : positive) (t : Pmap_raw A) {struct t} : option A :=
+ let _ : Lookup _ _ := @go in
match t with
| PLeaf => None
| PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
@@ -273,12 +273,12 @@ Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)}
| right H => right (H ∘ proj1 (Pmap_eq m1 m2))
end.
Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
-Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
-Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
+Instance Plookup : Lookup positive Pmap := λ A i m, pmap_car m !! i.
+Instance Ppartial_alter : PartialAlter positive Pmap := λ A f i m,
let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
Instance Pfmap : FMap Pmap := λ A B f m,
let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
-Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
+Instance Pto_list : FinMapToList positive Pmap := λ A m,
let (t,Ht) := m in Pto_list_raw 1 t [].
Instance Pomap : OMap Pmap := λ A B f m,
let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
@@ -305,7 +305,7 @@ Qed.
(** * Finite sets *)
(** We construct sets of [positives]s satisfying extensional equality. *)
Notation Pset := (mapset Pmap).
-Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
+Instance Pmap_dom : Dom Pmap Pset := mapset_dom.
Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
(** * Fresh numbers *)
diff --git a/prelude/zmap.v b/prelude/zmap.v
index 238fadc46..063c5b9cd 100644
--- a/prelude/zmap.v
+++ b/prelude/zmap.v
@@ -23,17 +23,17 @@ Proof.
end; abstract congruence.
Defined.
Instance Zempty {A} : Empty (Zmap A) := ZMap None ∅ ∅.
-Instance Zlookup {A} : Lookup Z A (Zmap A) := λ i t,
+Instance Zlookup : Lookup Z Zmap := λ A i t,
match i with
| Z0 => Zmap_0 t | Zpos p => Zmap_pos t !! p | Zneg p => Zmap_neg t !! p
end.
-Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
+Instance Zpartial_alter : PartialAlter Z Zmap := λ A f i t,
match i, t with
| Z0, ZMap o t t' => ZMap (f o) t t'
| Zpos p, ZMap o t t' => ZMap o (partial_alter f p t) t'
| Zneg p, ZMap o t t' => ZMap o t (partial_alter f p t')
end.
-Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
+Instance Zto_list : FinMapToList Z Zmap := λ A t,
match t with
| ZMap o t t' => default [] o (λ x, [(0,x)]) ++
(prod_map Zpos id <$> map_to_list t) ++
@@ -93,5 +93,5 @@ Qed.
(** * Finite sets *)
(** We construct sets of [Z]s satisfying extensional equality. *)
Notation Zset := (mapset Zmap).
-Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
+Instance Zmap_dom : Dom Zmap Zset := mapset_dom.
Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index e81180b79..fd4e2cd16 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -102,7 +102,7 @@ Proof.
iPvs (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done.
{ iNext. iExists false; eauto. }
iPvsIntro; iExists γ; repeat iSplit; auto.
- iNext. iExists (<[γ:=Q]> Φ); iSplit.
+ iNext. iExists (fn_insert γ Q Φ); iSplit.
- iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
- rewrite (big_sepM_fn_insert (λ _ _ P', _ ★ _ _ P' ★ _ _ (_ _ P')))%I //.
iFrame; eauto.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 1590ee737..8795d0256 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -150,7 +150,7 @@ Lemma lookup_wld_op_l n r1 r2 i P :
✓{n} (r1⋅r2) → wld r1 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
Proof.
move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
- destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
+ case Hi : (wld r2 !! i)=> [P'|]; rewrite ?right_id // =>-> ?.
by constructor; rewrite (agree_op_inv _ P P') // agree_idemp.
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
--
GitLab