Commit f2d59d09 authored by Robbert Krebbers's avatar Robbert Krebbers

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

This reverts commit 20b4ae55bdf00edb751ccdab3eb876cb9b13c99f, which does
not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).
parent f79a0b6f
...@@ -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 {_ _ _} _ !_ !_ / : simpl nomatch. Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.
Class DifferenceWith (M : Type Type) := Class DifferenceWith (A M : Type) :=
difference_with : {A}, (A A option A) M A M A M A. difference_with: (A A option A) M M M.
Instance: Params (@difference_with) 3. Instance: Params (@difference_with) 3.
Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch. Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
Definition intersection_with_list `{IntersectionWith M} {A} Definition intersection_with_list `{IntersectionWith A M}
(f : A A option A) : M A list (M A) M A := (f : A A option A) : M list M M := fold_right (intersection_with f).
fold_right (intersection_with f).
Arguments intersection_with_list _ _ _ _ _ !_ /. 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 *) (** * Axiomatization of collections *)
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with (** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
......
...@@ -326,13 +326,13 @@ Proof. ...@@ -326,13 +326,13 @@ Proof.
Qed. Qed.
(** * Domain of finite maps *) (** * Domain of finite maps *)
Instance Pmap_dom_coPset : Dom Pmap coPset := λ A m, of_Pset (dom _ m). Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m).
Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset. Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
Proof. Proof.
split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset. split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
by rewrite elem_of_of_Pset, elem_of_dom. by rewrite elem_of_of_Pset, elem_of_dom.
Qed. Qed.
Instance gmap_dom_coPset : Dom (gmap positive) coPset := λ A m, Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
of_gset (dom _ m). of_gset (dom _ m).
Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset. Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
Proof. Proof.
......
...@@ -5,9 +5,10 @@ maps. We provide such an axiomatization, instead of implementing the domain ...@@ -5,9 +5,10 @@ maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *) function in a generic way, to allow more efficient implementations. *)
From stdpp Require Export collections fin_maps. From stdpp Require Export collections fin_maps.
Class FinMapDom K M D `{FMap M, Lookup K M, A, Empty (M A), PartialAlter K M, Class FinMapDom K M D `{FMap M,
OMap M, Merge M, FinMapToList K M, i j : K, Decision (i = j), A, Lookup K A (M A), A, Empty (M A), A, PartialAlter K A (M A),
Dom M D, ElemOf K D, Empty D, Singleton K D, 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,
Union D, Intersection D, Difference D} := { Union D, Intersection D, Difference D} := {
finmap_dom_map :>> FinMap K M; finmap_dom_map :>> FinMap K M;
finmap_dom_collection :>> Collection K D; finmap_dom_collection :>> Collection K D;
......
...@@ -23,11 +23,11 @@ prove well founded recursion on finite maps. *) ...@@ -23,11 +23,11 @@ prove well founded recursion on finite maps. *)
which enables us to give a generic implementation of [union_with], which enables us to give a generic implementation of [union_with],
[intersection_with], and [difference_with]. *) [intersection_with], and [difference_with]. *)
Class FinMapToList (K : Type) (M : Type Type) := Class FinMapToList K A M := map_to_list: M list (K * A).
map_to_list : {A}, M A list (K * A).
Class FinMap K M `{FMap M, Lookup K M, A, Empty (M A), PartialAlter K M, Class FinMap K M `{FMap M, A, Lookup K A (M A), A, Empty (M A), A,
OMap M, Merge M, FinMapToList K M, i j : K, Decision (i = j)} := { PartialAlter K A (M A), OMap M, Merge M, A, FinMapToList K A (M A),
i j : K, Decision (i = j)} := {
map_eq {A} (m1 m2 : M A) : ( i, m1 !! i = m2 !! i) m1 = m2; map_eq {A} (m1 m2 : M A) : ( i, m1 !! i = m2 !! i) m1 = m2;
lookup_empty {A} i : ( : M A) !! i = None; lookup_empty {A} i : ( : M A) !! i = None;
lookup_partial_alter {A} f (m : M A) i : lookup_partial_alter {A} f (m : M A) i :
...@@ -48,47 +48,47 @@ Class FinMap K M `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M, ...@@ -48,47 +48,47 @@ Class FinMap K M `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M,
finite map implementations. These generic implementations do not cause a finite map implementations. These generic implementations do not cause a
significant performance loss to make including them in the finite map interface significant performance loss to make including them in the finite map interface
worthwhile. *) worthwhile. *)
Instance map_insert `{PartialAlter K M} : Insert K M := Instance map_insert `{PartialAlter K A M} : Insert K A M :=
λ A i x, partial_alter (λ _, Some x) i. λ i x, partial_alter (λ _, Some x) i.
Instance map_alter `{PartialAlter K M} : Alter K M := Instance map_alter `{PartialAlter K A M} : Alter K A M :=
λ A f, partial_alter (fmap f). λ f, partial_alter (fmap f).
Instance map_delete `{PartialAlter K M} : Delete K M := Instance map_delete `{PartialAlter K A M} : Delete K M :=
λ A, partial_alter (λ _, None). partial_alter (λ _, None).
Instance map_singleton `{PartialAlter K M, A, Empty (M A)} : SingletonM K M := Instance map_singleton `{PartialAlter K A M, Empty M} :
λ A i x, <[i:=x]> . SingletonM K A M := λ i x, <[i:=x]> .
Definition map_of_list `{Insert K M, Empty (M A)} : list (K * A) M A := Definition map_of_list `{Insert K A M, Empty M} : list (K * A) M :=
fold_right (λ p, <[p.1:=p.2]>) . fold_right (λ p, <[p.1:=p.2]>) .
Definition map_of_collection `{Elements K C, Insert K M, Empty (M A)} Definition map_of_collection `{Elements K C, Insert K A M, Empty M}
(f : K option A) (X : C) : M A := (f : K option A) (X : C) : M :=
map_of_list (omap (λ i, (i,) <$> f i) (elements X)). map_of_list (omap (λ i, (i,) <$> f i) (elements X)).
Instance map_union_with `{Merge M} : UnionWith M := Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
λ A f, merge (union_with f). λ f, merge (union_with f).
Instance map_intersection_with `{Merge M} : IntersectionWith M := Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
λ A f, merge (intersection_with f). λ f, merge (intersection_with f).
Instance map_difference_with `{Merge M} : DifferenceWith M := Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
λ A f, merge (difference_with f). λ f, merge (difference_with f).
Instance map_equiv `{Lookup K M, Equiv A} : Equiv (M A) | 18 := Instance map_equiv `{ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 18 :=
λ m1 m2, i, m1 !! i m2 !! i. λ m1 m2, i, m1 !! i m2 !! i.
(** The relation [intersection_forall R] on finite maps describes that the (** The relation [intersection_forall R] on finite maps describes that the
relation [R] holds for each pair in the intersection. *) relation [R] holds for each pair in the intersection. *)
Definition map_Forall `{Lookup K M} {A} (P : K A Prop) : M A Prop := Definition map_Forall `{Lookup K A M} (P : K A Prop) : M Prop :=
λ m, i x, m !! i = Some x P i x. λ m, i x, m !! i = Some x P i x.
Definition map_relation `{Lookup K M} {A B} (R : A B Prop) Definition map_relation `{ A, Lookup K A (M A)} {A B} (R : A B Prop)
(P : A Prop) (Q : B Prop) (m1 : M A) (m2 : M B) : Prop := i, (P : A Prop) (Q : B Prop) (m1 : M A) (m2 : M B) : Prop := i,
option_relation R P Q (m1 !! i) (m2 !! i). option_relation R P Q (m1 !! i) (m2 !! i).
Definition map_included `{Lookup K M} {A} Definition map_included `{ A, Lookup K A (M A)} {A}
(R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True). (R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
Definition map_disjoint `{Lookup K M} {A} : relation (M A) := Definition map_disjoint `{ A, Lookup K A (M A)} {A} : relation (M A) :=
map_relation (λ _ _, False) (λ _, True) (λ _, True). map_relation (λ _ _, False) (λ _, True) (λ _, True).
Infix "⊥ₘ" := map_disjoint (at level 70) : C_scope. Infix "⊥ₘ" := map_disjoint (at level 70) : C_scope.
Hint Extern 0 (_ _) => symmetry; eassumption. Hint Extern 0 (_ _) => symmetry; eassumption.
Notation "( m ⊥ₘ.)" := (map_disjoint m) (only parsing) : C_scope. Notation "( m ⊥ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
Notation "(.⊥ₘ m )" := (λ m2, m2 m) (only parsing) : C_scope. Notation "(.⊥ₘ m )" := (λ m2, m2 m) (only parsing) : C_scope.
Instance map_subseteq `{Lookup K M} {A} : SubsetEq (M A) := Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
map_included (=). map_included (=).
(** The union of two finite maps only has a meaningful definition for maps (** 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) := ...@@ -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 (** 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. *) of the elements. Implemented by conversion to lists, so not very efficient. *)
Definition map_imap `{Insert K M, A, Empty (M A), Definition map_imap `{ A, Insert K A (M A), A, Empty (M A),
FinMapToList K M} {A B} (f : K A option B) (m : M A) : M B := A, FinMapToList K A (M A)} {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)). map_of_list (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)).
(** * Theorems *) (** * Theorems *)
...@@ -124,25 +124,27 @@ Section setoid. ...@@ -124,25 +124,27 @@ Section setoid.
- by intros m1 m2 ? i. - by intros m1 m2 ? i.
- by intros m1 m2 m3 ?? i; trans (m2 !! i). - by intros m1 m2 m3 ?? i; trans (m2 !! i).
Qed. Qed.
Global Instance lookup_proper (i: K) : Proper (() ==> ()) (lookup (M:=M) i). Global Instance lookup_proper (i : K) :
Proper (() ==> ()) (lookup (M:=M A) i).
Proof. by intros m1 m2 Hm. Qed. Proof. by intros m1 m2 Hm. Qed.
Global Instance partial_alter_proper : Global Instance partial_alter_proper :
Proper ((() ==> ()) ==> (=) ==> () ==> ()) (partial_alter (M:=M)). Proper ((() ==> ()) ==> (=) ==> () ==> ()) (partial_alter (M:=M A)).
Proof. Proof.
by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|]; 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; rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
try apply Hf; apply lookup_proper. try apply Hf; apply lookup_proper.
Qed. Qed.
Global Instance insert_proper (i : K) : Global Instance insert_proper (i : K) :
Proper (() ==> () ==> ()) (insert (M:=M) i). Proper (() ==> () ==> ()) (insert (M:=M A) i).
Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed. Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
Global Instance singleton_proper (i : K) : Global Instance singleton_proper k :
Proper (() ==> ()) (singletonM (M:=M) i). Proper (() ==> ()) (singletonM k : A M A).
Proof. by intros ???; apply insert_proper. Qed. Proof. by intros ???; apply insert_proper. Qed.
Global Instance delete_proper (i: K) : Proper (() ==> ()) (delete (M:=M) i). Global Instance delete_proper (i : K) :
Proper (() ==> ()) (delete (M:=M A) i).
Proof. by apply partial_alter_proper; [constructor|]. Qed. Proof. by apply partial_alter_proper; [constructor|]. Qed.
Global Instance alter_proper : Global Instance alter_proper :
Proper ((() ==> ()) ==> (=) ==> () ==> ()) (alter (M:=M)). Proper ((() ==> ()) ==> (=) ==> () ==> ()) (alter (A:=A) (M:=M A)).
Proof. Proof.
intros ?? Hf; apply partial_alter_proper. intros ?? Hf; apply partial_alter_proper.
by destruct 1; constructor; apply Hf. by destruct 1; constructor; apply Hf.
...@@ -154,7 +156,7 @@ Section setoid. ...@@ -154,7 +156,7 @@ Section setoid.
by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf. by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
Qed. Qed.
Global Instance union_with_proper : Global Instance union_with_proper :
Proper ((() ==> () ==> ()) ==> () ==> () ==>()) (union_with (M:=M)). Proper ((() ==> () ==> ()) ==> () ==> () ==>()) (union_with (M:=M A)).
Proof. Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto. intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor]. by do 2 destruct 1; first [apply Hf | constructor].
......
...@@ -2,10 +2,10 @@ From stdpp Require Export base tactics. ...@@ -2,10 +2,10 @@ From stdpp Require Export base tactics.
Section definitions. Section definitions.
Context {A T : Type} `{ a b : A, Decision (a = b)}. Context {A T : Type} `{ a b : A, Decision (a = b)}.
Definition fn_insert (a : A) (t : T) (f : A T) : A T := λ b, Global Instance fn_insert : Insert A T (A T) :=
if decide (a = b) then t else f b. λ a t f b, if decide (a = b) then t else f b.
Definition fn_alter (g : T T) (a : A) (f : A T) : A T := λ b, Global Instance fn_alter : Alter A T (A T) :=
if decide (a = b) then g (f a) else f b. λ (g : T T) a f b, if decide (a = b) then g (f a) else f b.
End definitions. End definitions.
(* TODO: For now, we only have the properties here that do not need a notion (* TODO: For now, we only have the properties here that do not need a notion
...@@ -14,17 +14,17 @@ End definitions. ...@@ -14,17 +14,17 @@ End definitions.
Section functions. Section functions.
Context {A T : Type} `{ a b : A, Decision (a = b)}. Context {A T : Type} `{ a b : A, Decision (a = b)}.
Lemma fn_lookup_insert (f : A T) a t : fn_insert a t f a = t. Lemma fn_lookup_insert (f : A T) a t : <[a:=t]>f a = t.
Proof. unfold fn_insert. by destruct (decide (a = a)). Qed. Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed.
Lemma fn_lookup_insert_rev (f : A T) a t1 t2 : Lemma fn_lookup_insert_rev (f : A T) a t1 t2 :
fn_insert a t1 f a = t2 t1 = t2. <[a:=t1]>f a = t2 t1 = t2.
Proof. rewrite fn_lookup_insert. congruence. Qed. Proof. rewrite fn_lookup_insert. congruence. Qed.
Lemma fn_lookup_insert_ne (f : A T) a b t : a b fn_insert a t f b = f b. Lemma fn_lookup_insert_ne (f : A T) a b t : a b <[a:=t]>f b = f b.
Proof. unfold fn_insert. by destruct (decide (a = b)). Qed. Proof. unfold insert, fn_insert. by destruct (decide (a = b)). Qed.
Lemma fn_lookup_alter (g : T T) (f : A T) a : fn_alter g a f a = g (f a). Lemma fn_lookup_alter (g : T T) (f : A T) a : alter g a f a = g (f a).
Proof. unfold fn_alter. by destruct (decide (a = a)). Qed. Proof. unfold alter, fn_alter. by destruct (decide (a = a)). Qed.
Lemma fn_lookup_alter_ne (g : T T) (f : A T) a b : Lemma fn_lookup_alter_ne (g : T T) (f : A T) a b :
a b fn_alter g a f b = f b. a b alter g a f b = f b.
Proof. unfold fn_alter. by destruct (decide (a = b)). Qed. Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
End functions. End functions.
...@@ -30,7 +30,7 @@ Proof. ...@@ -30,7 +30,7 @@ Proof.
Defined. Defined.
(** * Operations on the data structure *) (** * Operations on the data structure *)
Instance gmap_lookup `{Countable K} : Lookup K (gmap K) := λ A i m, Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
let (m,_) := m in m !! encode i. let (m,_) := m in m !! encode i.
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap 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 : Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A option A) m i :
...@@ -40,7 +40,8 @@ Proof. ...@@ -40,7 +40,8 @@ Proof.
- rewrite decode_encode; eauto. - rewrite decode_encode; eauto.
- rewrite lookup_partial_alter_ne by done. by apply Hm. - rewrite lookup_partial_alter_ne by done. by apply Hm.
Qed. Qed.
Instance gmap_partial_alter `{Countable K} : PartialAlter K (gmap K) := λ A f i m, Instance gmap_partial_alter `{Countable K} {A} :
PartialAlter K A (gmap K A) := λ f i m,
let (m,Hm) := m in GMap (partial_alter f (encode 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_pack _ (gmap_partial_alter_wf f m i
(bool_decide_unpack _ Hm))). (bool_decide_unpack _ Hm))).
...@@ -69,7 +70,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2, ...@@ -69,7 +70,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 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 _ _ GMap (merge f' m1 m2) (bool_decide_pack _ (gmap_merge_wf f _ _
(bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))). (bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
Instance gmap_to_list `{Countable K} : FinMapToList K (gmap K) := λ A m, Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
let (m,_) := m in omap (λ ix : positive * A, let (m,_) := m in omap (λ ix : positive * A,
let (i,x) := ix in (,x) <$> decode i) (map_to_list m). let (i,x) := ix in (,x) <$> decode i) (map_to_list m).
...@@ -113,7 +114,7 @@ Qed. ...@@ -113,7 +114,7 @@ Qed.
(** * Finite sets *) (** * Finite sets *)
Notation gset K := (mapset (gmap K)). Notation gset K := (mapset (gmap K)).
Instance gset_dom `{Countable K} : Dom (gmap K) (gset K) := mapset_dom. Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
Instance gset_dom_spec `{Countable K} : Instance gset_dom_spec `{Countable K} :
FinMapDom K (gmap K) (gset K) := mapset_dom_spec. FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
......
...@@ -57,15 +57,15 @@ Existing Instance list_equiv. ...@@ -57,15 +57,15 @@ Existing Instance list_equiv.
(** The operation [l !! i] gives the [i]th element of the list [l], or [None] (** The operation [l !! i] gives the [i]th element of the list [l], or [None]
in case [i] is out of bounds. *) in case [i] is out of bounds. *)
Instance list_lookup : Lookup nat list := Instance list_lookup {A} : Lookup nat A (list A) :=
fix go A i l {struct l} : option A := let _ : Lookup _ _ := @go in fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in
match l with match l with
| [] => None | x :: l => match i with 0 => Some x | S i => l !! i end | [] => None | x :: l => match i with 0 => Some x | S i => l !! i end
end. end.
(** The operation [alter f i l] applies the function [f] to the [i]th element (** 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. *) of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_alter : Alter nat list := λ A f, Instance list_alter {A} : Alter nat A (list A) := λ f,
fix go i l {struct l} := fix go i l {struct l} :=
match l with match l with
| [] => [] | [] => []
...@@ -74,8 +74,8 @@ Instance list_alter : Alter nat list := λ A f, ...@@ -74,8 +74,8 @@ Instance list_alter : Alter nat list := λ A f,
(** The operation [<[i:=x]> l] overwrites the element at position [i] with the (** 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. *) value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_insert : Insert nat list := Instance list_insert {A} : Insert nat A (list A) :=
fix go A i y l {struct l} := let _ : Insert _ _ := @go in fix go i y l {struct l} := let _ : Insert _ _ _ := @go in
match l with match l with
| [] => [] | [] => []
| x :: l => match i with 0 => y :: l | S i => x :: <[i:=y]>l end | x :: l => match i with 0 => y :: l | S i => x :: <[i:=y]>l end
...@@ -90,11 +90,11 @@ Instance: Params (@list_inserts) 1. ...@@ -90,11 +90,11 @@ Instance: Params (@list_inserts) 1.
(** The operation [delete i l] removes the [i]th element of [l] and moves (** 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, all consecutive elements one position ahead. In case [i] is out of bounds,
the list is returned unchanged. *) the list is returned unchanged. *)
Instance list_delete : Delete nat list := Instance list_delete {A} : Delete nat (list A) :=
fix go A (i : nat) (l : list A) {struct l} : list A := fix go (i : nat) (l : list A) {struct l} : list A :=
match l with 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. end.
(** The function [option_list o] converts an element [Some x] into the (** The function [option_list o] converts an element [Some x] into the
...@@ -2733,13 +2733,13 @@ Section setoid. ...@@ -2733,13 +2733,13 @@ Section setoid.
Global Instance drop_proper n : Proper (() ==> ()) (@drop A n). Global Instance drop_proper n : Proper (() ==> ()) (@drop A n).
Proof. induction n; destruct 1; simpl; try constructor; auto. Qed. Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
Global Instance list_lookup_proper i : Global Instance list_lookup_proper i :
Proper (() ==> ()) (lookup (M:=list) i). Proper (() ==> ()) (lookup (M:=list A) i).
Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed. Proof. induction i; destruct 1; simpl; f_equiv; auto