Skip to content
Snippets Groups Projects
Verified Commit 737e3930 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Test changes

parent c4116388
No related tags found
No related merge requests found
...@@ -28,42 +28,42 @@ Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M := ...@@ -28,42 +28,42 @@ Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
Instance: Params (@big_opL) 4 := {}. Instance: Params (@big_opL) 4 := {}.
Arguments big_opL {M} o {_ A} _ !_ /. Arguments big_opL {M} o {_ A} _ !_ /.
Typeclasses Opaque big_opL. Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l) Notation "'[' '^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity, (at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
format "[^ o list] k ↦ x ∈ l , P") : stdpp_scope. format "[ ^ o list] k ↦ x ∈ l , P") : stdpp_scope.
Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l) Notation "'[' '^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity, (at level 200, o at level 1, l at level 10, x at level 1, right associativity,
format "[^ o list] x ∈ l , P") : stdpp_scope. format "[ ^ o list] x ∈ l , P") : stdpp_scope.
Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K A M) Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K A M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m). (m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
Instance: Params (@big_opM) 7 := {}. Instance: Params (@big_opM) 7 := {}.
Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never. Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never.
Typeclasses Opaque big_opM. Typeclasses Opaque big_opM.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m) Notation "'[' '^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
(at level 200, o at level 1, m at level 10, k, x at level 1, right associativity, (at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
format "[^ o map] k ↦ x ∈ m , P") : stdpp_scope. format "[ ^ o map] k ↦ x ∈ m , P") : stdpp_scope.
Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m) Notation "'[' '^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity, (at level 200, o at level 1, m at level 10, x at level 1, right associativity,
format "[^ o map] x ∈ m , P") : stdpp_scope. format "[ ^ o map] x ∈ m , P") : stdpp_scope.
Definition big_opS `{Monoid M o} `{Countable A} (f : A M) Definition big_opS `{Monoid M o} `{Countable A} (f : A M)
(X : gset A) : M := big_opL o (λ _, f) (elements X). (X : gset A) : M := big_opL o (λ _, f) (elements X).
Instance: Params (@big_opS) 6 := {}. Instance: Params (@big_opS) 6 := {}.
Arguments big_opS {M} o {_ A _ _} _ _ : simpl never. Arguments big_opS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opS. Typeclasses Opaque big_opS.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X) Notation "'[' '^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity, (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o set] x ∈ X , P") : stdpp_scope. format "[ ^ o set] x ∈ X , P") : stdpp_scope.
Definition big_opMS `{Monoid M o} `{Countable A} (f : A M) Definition big_opMS `{Monoid M o} `{Countable A} (f : A M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X). (X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Instance: Params (@big_opMS) 7 := {}. Instance: Params (@big_opMS) 7 := {}.
Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never. Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opMS. Typeclasses Opaque big_opMS.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X) Notation "'[' '^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity, (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o mset] x ∈ X , P") : stdpp_scope. format "[ ^ o mset] x ∈ X , P") : stdpp_scope.
(** * Properties about big ops *) (** * Properties about big ops *)
Section big_op. Section big_op.
...@@ -80,7 +80,7 @@ Section list. ...@@ -80,7 +80,7 @@ Section list.
Lemma big_opL_nil f : ([^o list] ky [], f k y) = monoid_unit. Lemma big_opL_nil f : ([^o list] ky [], f k y) = monoid_unit.
Proof. done. Qed. Proof. done. Qed.
Lemma big_opL_cons f x l : Lemma big_opL_cons f x l :
([^o list] ky x :: l, f k y) = f 0 x `o` [^o list] ky l, f (S k) y. ([^o list] ky x :: l, f k y) = f 0 x `o` ([^o list] ky l, f (S k) y).
Proof. done. Qed. Proof. done. Qed.
Lemma big_opL_singleton f x : ([^o list] ky [x], f k y) f 0 x. Lemma big_opL_singleton f x : ([^o list] ky [x], f k y) f 0 x.
Proof. by rewrite /= right_id. Qed. Proof. by rewrite /= right_id. Qed.
...@@ -106,7 +106,7 @@ Section list. ...@@ -106,7 +106,7 @@ Section list.
Lemma big_opL_ext f g l : Lemma big_opL_ext f g l :
( k y, l !! k = Some y f k y = g k y) ( k y, l !! k = Some y f k y = g k y)
([^o list] k y l, f k y) = [^o list] k y l, g k y. ([^o list] k y l, f k y) = ([^o list] k y l, g k y).
Proof. apply big_opL_forall; apply _. Qed. Proof. apply big_opL_forall; apply _. Qed.
Lemma big_opL_proper f g l : Lemma big_opL_proper f g l :
( k y, l !! k = Some y f k y g k y) ( k y, l !! k = Some y f k y g k y)
...@@ -135,10 +135,10 @@ Section list. ...@@ -135,10 +135,10 @@ Section list.
Proof. intros f f' Hf l ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed. Proof. intros f f' Hf l ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
Lemma big_opL_consZ_l (f : Z A M) x l : Lemma big_opL_consZ_l (f : Z A M) x l :
([^o list] ky x :: l, f k y) = f 0 x `o` [^o list] ky l, f (1 + k)%Z y. ([^o list] ky x :: l, f k y) = f 0 x `o` ([^o list] ky l, f (1 + k)%Z y).
Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed. Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
Lemma big_opL_consZ_r (f : Z A M) x l : Lemma big_opL_consZ_r (f : Z A M) x l :
([^o list] ky x :: l, f k y) = f 0 x `o` [^o list] ky l, f (k + 1)%Z y. ([^o list] ky x :: l, f k y) = f 0 x `o` ([^o list] ky l, f (k + 1)%Z y).
Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed. Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
Lemma big_opL_fmap {B} (h : A B) (f : nat B M) l : Lemma big_opL_fmap {B} (h : A B) (f : nat B M) l :
...@@ -198,12 +198,12 @@ Section gmap. ...@@ -198,12 +198,12 @@ Section gmap.
Lemma big_opM_insert f m i x : Lemma big_opM_insert f m i x :
m !! i = None m !! i = None
([^o map] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky m, f k y. ([^o map] ky <[i:=x]> m, f k y) f i x `o` ([^o map] ky m, f k y).
Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed. Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed.
Lemma big_opM_delete f m i x : Lemma big_opM_delete f m i x :
m !! i = Some x m !! i = Some x
([^o map] ky m, f k y) f i x `o` [^o map] ky delete i m, f k y. ([^o map] ky m, f k y) f i x `o` ([^o map] ky delete i m, f k y).
Proof. Proof.
intros. rewrite -big_opM_insert ?lookup_delete //. intros. rewrite -big_opM_insert ?lookup_delete //.
by rewrite insert_delete insert_id. by rewrite insert_delete insert_id.
...@@ -236,7 +236,7 @@ Section gmap. ...@@ -236,7 +236,7 @@ Section gmap.
Lemma big_opM_fn_insert {B} (g : K A B M) (f : K B) m i (x : A) b : Lemma big_opM_fn_insert {B} (g : K A B M) (f : K B) m i (x : A) b :
m !! i = None m !! i = None
([^o map] ky <[i:=x]> m, g k y (<[i:=b]> f k)) ([^o map] ky <[i:=x]> m, g k y (<[i:=b]> f k))
g i x b `o` [^o map] ky m, g k y (f k). g i x b `o` ([^o map] ky m, g k y (f k)).
Proof. Proof.
intros. rewrite big_opM_insert // fn_lookup_insert. intros. rewrite big_opM_insert // fn_lookup_insert.
f_equiv; apply big_opM_proper; auto=> k y ?. f_equiv; apply big_opM_proper; auto=> k y ?.
...@@ -244,7 +244,7 @@ Section gmap. ...@@ -244,7 +244,7 @@ Section gmap.
Qed. Qed.
Lemma big_opM_fn_insert' (f : K M) m i x P : Lemma big_opM_fn_insert' (f : K M) m i x P :
m !! i = None m !! i = None
([^o map] ky <[i:=x]> m, <[i:=P]> f k) (P `o` [^o map] ky m, f k). ([^o map] ky <[i:=x]> m, <[i:=P]> f k) (P `o` ([^o map] ky m, f k)).
Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed. Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
Lemma big_opM_union f m1 m2 : Lemma big_opM_union f m1 m2 :
...@@ -301,19 +301,19 @@ Section gset. ...@@ -301,19 +301,19 @@ Section gset.
Proof. by rewrite /big_opS elements_empty. Qed. Proof. by rewrite /big_opS elements_empty. Qed.
Lemma big_opS_insert f X x : Lemma big_opS_insert f X x :
x X ([^o set] y {[ x ]} X, f y) (f x `o` [^o set] y X, f y). x X ([^o set] y {[ x ]} X, f y) (f x `o` ([^o set] y X, f y)).
Proof. intros. by rewrite /big_opS elements_union_singleton. Qed. Proof. intros. by rewrite /big_opS elements_union_singleton. Qed.
Lemma big_opS_fn_insert {B} (f : A B M) h X x b : Lemma big_opS_fn_insert {B} (f : A B M) h X x b :
x X x X
([^o set] y {[ x ]} X, f y (<[x:=b]> h y)) ([^o set] y {[ x ]} X, f y (<[x:=b]> h y))
f x b `o` [^o set] y X, f y (h y). f x b `o` ([^o set] y X, f y (h y)).
Proof. Proof.
intros. rewrite big_opS_insert // fn_lookup_insert. intros. rewrite big_opS_insert // fn_lookup_insert.
f_equiv; apply big_opS_proper; auto=> y ?. f_equiv; apply big_opS_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_opS_fn_insert' f X x P : Lemma big_opS_fn_insert' f X x P :
x X ([^o set] y {[ x ]} X, <[x:=P]> f y) (P `o` [^o set] y X, f y). x X ([^o set] y {[ x ]} X, <[x:=P]> f y) (P `o` ([^o set] y X, f y)).
Proof. apply (big_opS_fn_insert (λ y, id)). Qed. Proof. apply (big_opS_fn_insert (λ y, id)). Qed.
Lemma big_opS_union f X Y : Lemma big_opS_union f X Y :
...@@ -327,7 +327,7 @@ Section gset. ...@@ -327,7 +327,7 @@ Section gset.
Qed. Qed.
Lemma big_opS_delete f X x : Lemma big_opS_delete f X x :
x X ([^o set] y X, f y) f x `o` [^o set] y X {[ x ]}, f y. x X ([^o set] y X, f y) f x `o` ([^o set] y X {[ x ]}, f y).
Proof. Proof.
intros. rewrite -big_opS_insert; last set_solver. intros. rewrite -big_opS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver. by rewrite -union_difference_L; last set_solver.
...@@ -388,7 +388,7 @@ Section gmultiset. ...@@ -388,7 +388,7 @@ Section gmultiset.
Proof. by rewrite /big_opMS gmultiset_elements_empty. Qed. Proof. by rewrite /big_opMS gmultiset_elements_empty. Qed.
Lemma big_opMS_disj_union f X Y : Lemma big_opMS_disj_union f X Y :
([^o mset] y X Y, f y) ([^o mset] y X, f y) `o` [^o mset] y Y, f y. ([^o mset] y X Y, f y) ([^o mset] y X, f y) `o` ([^o mset] y Y, f y).
Proof. by rewrite /big_opMS gmultiset_elements_disj_union big_opL_app. Qed. Proof. by rewrite /big_opMS gmultiset_elements_disj_union big_opL_app. Qed.
Lemma big_opMS_singleton f x : ([^o mset] y {[ x ]}, f y) f x. Lemma big_opMS_singleton f x : ([^o mset] y {[ x ]}, f y) f x.
...@@ -397,7 +397,7 @@ Section gmultiset. ...@@ -397,7 +397,7 @@ Section gmultiset.
Qed. Qed.
Lemma big_opMS_delete f X x : Lemma big_opMS_delete f X x :
x X ([^o mset] y X, f y) f x `o` [^o mset] y X {[ x ]}, f y. x X ([^o mset] y X, f y) f x `o` ([^o mset] y X {[ x ]}, f y).
Proof. Proof.
intros. rewrite -big_opMS_singleton -big_opMS_disj_union. intros. rewrite -big_opMS_singleton -big_opMS_disj_union.
by rewrite -gmultiset_disj_union_difference'. by rewrite -gmultiset_disj_union_difference'.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment