Commit 37e95231 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename solve_elem_of into set_solver.

It is doing much more than just dealing with ∈, it solves all kinds
of goals involving set operations (including ≡ and ⊆).
parent 20690605
...@@ -207,7 +207,7 @@ Ltac decompose_empty := repeat ...@@ -207,7 +207,7 @@ Ltac decompose_empty := repeat
occurrences of [(∪)], [(∩)], [(∖)], [(<$>)], [∅], [{[_]}], [(≡)], and [(⊆)], occurrences of [(∪)], [(∩)], [(∖)], [(<$>)], [∅], [{[_]}], [(≡)], and [(⊆)],
by rewriting these into logically equivalent propositions. For example we by rewriting these into logically equivalent propositions. For example we
rewrite [A → x ∈ X ∪ ∅] into [A → x ∈ X ∨ False]. *) rewrite [A → x ∈ X ∪ ∅] into [A → x ∈ X ∨ False]. *)
Ltac unfold_elem_of := Ltac set_unfold :=
repeat_on_hyps (fun H => repeat_on_hyps (fun H =>
repeat match type of H with repeat match type of H with
| context [ _ _ ] => setoid_rewrite elem_of_subseteq in H | context [ _ _ ] => setoid_rewrite elem_of_subseteq in H
...@@ -251,21 +251,21 @@ Ltac unfold_elem_of := ...@@ -251,21 +251,21 @@ Ltac unfold_elem_of :=
end. end.
(** Since [firstorder] fails or loops on very small goals generated by (** Since [firstorder] fails or loops on very small goals generated by
[solve_elem_of] already. We use the [naive_solver] tactic as a substitute. [set_solver] already. We use the [naive_solver] tactic as a substitute.
This tactic either fails or proves the goal. *) This tactic either fails or proves the goal. *)
Tactic Notation "solve_elem_of" tactic3(tac) := Tactic Notation "set_solver" tactic3(tac) :=
setoid_subst; setoid_subst;
decompose_empty; decompose_empty;
unfold_elem_of; set_unfold;
naive_solver tac. naive_solver tac.
Tactic Notation "solve_elem_of" "-" hyp_list(Hs) "/" tactic3(tac) := Tactic Notation "set_solver" "-" hyp_list(Hs) "/" tactic3(tac) :=
clear Hs; solve_elem_of tac. clear Hs; set_solver tac.
Tactic Notation "solve_elem_of" "+" hyp_list(Hs) "/" tactic3(tac) := Tactic Notation "set_solver" "+" hyp_list(Hs) "/" tactic3(tac) :=
revert Hs; clear; solve_elem_of tac. revert Hs; clear; set_solver tac.
Tactic Notation "solve_elem_of" := solve_elem_of eauto. Tactic Notation "set_solver" := set_solver eauto.
Tactic Notation "solve_elem_of" "-" hyp_list(Hs) := clear Hs; solve_elem_of. Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
Tactic Notation "solve_elem_of" "+" hyp_list(Hs) := Tactic Notation "set_solver" "+" hyp_list(Hs) :=
revert Hs; clear; solve_elem_of. revert Hs; clear; set_solver.
(** * More theorems *) (** * More theorems *)
Section collection. Section collection.
...@@ -273,7 +273,7 @@ Section collection. ...@@ -273,7 +273,7 @@ Section collection.
Implicit Types X Y : C. Implicit Types X Y : C.
Global Instance: Lattice C. Global Instance: Lattice C.
Proof. split. apply _. firstorder auto. solve_elem_of. Qed. Proof. split. apply _. firstorder auto. set_solver. Qed.
Global Instance difference_proper : Global Instance difference_proper :
Proper (() ==> () ==> ()) (@difference C _). Proper (() ==> () ==> ()) (@difference C _).
Proof. Proof.
...@@ -281,23 +281,23 @@ Section collection. ...@@ -281,23 +281,23 @@ Section collection.
by rewrite !elem_of_difference, HX, HY. by rewrite !elem_of_difference, HX, HY.
Qed. Qed.
Lemma non_empty_inhabited x X : x X X . Lemma non_empty_inhabited x X : x X X .
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma intersection_singletons x : ({[x]} : C) {[x]} {[x]}. Lemma intersection_singletons x : ({[x]} : C) {[x]} {[x]}.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma difference_twice X Y : (X Y) Y X Y. Lemma difference_twice X Y : (X Y) Y X Y.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma subseteq_empty_difference X Y : X Y X Y . Lemma subseteq_empty_difference X Y : X Y X Y .
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma difference_diag X : X X . Lemma difference_diag X : X X .
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma difference_union_distr_l X Y Z : (X Y) Z X Z Y Z. Lemma difference_union_distr_l X Y Z : (X Y) Z X Z Y Z.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma difference_union_distr_r X Y Z : Z (X Y) (Z X) (Z Y). Lemma difference_union_distr_r X Y Z : Z (X Y) (Z X) (Z Y).
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma difference_intersection_distr_l X Y Z : (X Y) Z X Z Y Z. Lemma difference_intersection_distr_l X Y Z : (X Y) Z X Z Y Z.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma disjoint_union_difference X Y : X Y (X Y) X Y. Lemma disjoint_union_difference X Y : X Y (X Y) X Y.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Section leibniz. Section leibniz.
Context `{!LeibnizEquiv C}. Context `{!LeibnizEquiv C}.
...@@ -334,10 +334,10 @@ Section collection. ...@@ -334,10 +334,10 @@ Section collection.
Lemma non_empty_difference X Y : X Y Y X . Lemma non_empty_difference X Y : X Y Y X .
Proof. Proof.
intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x. intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
destruct (decide (x X)); solve_elem_of. destruct (decide (x X)); set_solver.
Qed. Qed.
Lemma empty_difference_subseteq X Y : X Y X Y. Lemma empty_difference_subseteq X Y : X Y X Y.
Proof. intros ? x ?; apply dec_stable; solve_elem_of. Qed. Proof. intros ? x ?; apply dec_stable; set_solver. Qed.
Context `{!LeibnizEquiv C}. Context `{!LeibnizEquiv C}.
Lemma union_difference_L X Y : X Y Y = X Y X. Lemma union_difference_L X Y : X Y Y = X Y X.
Proof. unfold_leibniz. apply union_difference. Qed. Proof. unfold_leibniz. apply union_difference. Qed.
...@@ -396,33 +396,33 @@ Section NoDup. ...@@ -396,33 +396,33 @@ Section NoDup.
Proof. firstorder. Qed. Proof. firstorder. Qed.
Lemma elem_of_upto_elem_of x X : x X elem_of_upto x X. Lemma elem_of_upto_elem_of x X : x X elem_of_upto x X.
Proof. unfold elem_of_upto. solve_elem_of. Qed. Proof. unfold elem_of_upto. set_solver. Qed.
Lemma elem_of_upto_empty x : ¬elem_of_upto x . Lemma elem_of_upto_empty x : ¬elem_of_upto x .
Proof. unfold elem_of_upto. solve_elem_of. Qed. Proof. unfold elem_of_upto. set_solver. Qed.
Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} R x y. Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} R x y.
Proof. unfold elem_of_upto. solve_elem_of. Qed. Proof. unfold elem_of_upto. set_solver. Qed.
Lemma elem_of_upto_union X Y x : Lemma elem_of_upto_union X Y x :
elem_of_upto x (X Y) elem_of_upto x X elem_of_upto x Y. elem_of_upto x (X Y) elem_of_upto x X elem_of_upto x Y.
Proof. unfold elem_of_upto. solve_elem_of. Qed. Proof. unfold elem_of_upto. set_solver. Qed.
Lemma not_elem_of_upto x X : ¬elem_of_upto x X y, y X ¬R x y. Lemma not_elem_of_upto x X : ¬elem_of_upto x X y, y X ¬R x y.
Proof. unfold elem_of_upto. solve_elem_of. Qed. Proof. unfold elem_of_upto. set_solver. Qed.
Lemma set_NoDup_empty: set_NoDup . Lemma set_NoDup_empty: set_NoDup .
Proof. unfold set_NoDup. solve_elem_of. Qed. Proof. unfold set_NoDup. set_solver. Qed.
Lemma set_NoDup_add x X : Lemma set_NoDup_add x X :
¬elem_of_upto x X set_NoDup X set_NoDup ({[ x ]} X). ¬elem_of_upto x X set_NoDup X set_NoDup ({[ x ]} X).
Proof. unfold set_NoDup, elem_of_upto. solve_elem_of. Qed. Proof. unfold set_NoDup, elem_of_upto. set_solver. Qed.
Lemma set_NoDup_inv_add x X : Lemma set_NoDup_inv_add x X :
x X set_NoDup ({[ x ]} X) ¬elem_of_upto x X. x X set_NoDup ({[ x ]} X) ¬elem_of_upto x X.
Proof. Proof.
intros Hin Hnodup [y [??]]. intros Hin Hnodup [y [??]].
rewrite (Hnodup x y) in Hin; solve_elem_of. rewrite (Hnodup x y) in Hin; set_solver.
Qed. Qed.
Lemma set_NoDup_inv_union_l X Y : set_NoDup (X Y) set_NoDup X. Lemma set_NoDup_inv_union_l X Y : set_NoDup (X Y) set_NoDup X.
Proof. unfold set_NoDup. solve_elem_of. Qed. Proof. unfold set_NoDup. set_solver. Qed.
Lemma set_NoDup_inv_union_r X Y : set_NoDup (X Y) set_NoDup Y. Lemma set_NoDup_inv_union_r X Y : set_NoDup (X Y) set_NoDup Y.
Proof. unfold set_NoDup. solve_elem_of. Qed. Proof. unfold set_NoDup. set_solver. Qed.
End NoDup. End NoDup.
(** * Quantifiers *) (** * Quantifiers *)
...@@ -433,27 +433,27 @@ Section quantifiers. ...@@ -433,27 +433,27 @@ Section quantifiers.
Definition set_Exists X := x, x X P x. Definition set_Exists X := x, x X P x.
Lemma set_Forall_empty : set_Forall . Lemma set_Forall_empty : set_Forall .
Proof. unfold set_Forall. solve_elem_of. Qed. Proof. unfold set_Forall. set_solver. Qed.
Lemma set_Forall_singleton x : set_Forall {[ x ]} P x. Lemma set_Forall_singleton x : set_Forall {[ x ]} P x.
Proof. unfold set_Forall. solve_elem_of. Qed. Proof. unfold set_Forall. set_solver. Qed.
Lemma set_Forall_union X Y : set_Forall X set_Forall Y set_Forall (X Y). Lemma set_Forall_union X Y : set_Forall X set_Forall Y set_Forall (X Y).
Proof. unfold set_Forall. solve_elem_of. Qed. Proof. unfold set_Forall. set_solver. Qed.
Lemma set_Forall_union_inv_1 X Y : set_Forall (X Y) set_Forall X. Lemma set_Forall_union_inv_1 X Y : set_Forall (X Y) set_Forall X.
Proof. unfold set_Forall. solve_elem_of. Qed. Proof. unfold set_Forall. set_solver. Qed.
Lemma set_Forall_union_inv_2 X Y : set_Forall (X Y) set_Forall Y. Lemma set_Forall_union_inv_2 X Y : set_Forall (X Y) set_Forall Y.
Proof. unfold set_Forall. solve_elem_of. Qed. Proof. unfold set_Forall. set_solver. Qed.
Lemma set_Exists_empty : ¬set_Exists . Lemma set_Exists_empty : ¬set_Exists .
Proof. unfold set_Exists. solve_elem_of. Qed. Proof. unfold set_Exists. set_solver. Qed.
Lemma set_Exists_singleton x : set_Exists {[ x ]} P x. Lemma set_Exists_singleton x : set_Exists {[ x ]} P x.
Proof. unfold set_Exists. solve_elem_of. Qed. Proof. unfold set_Exists. set_solver. Qed.
Lemma set_Exists_union_1 X Y : set_Exists X set_Exists (X Y). Lemma set_Exists_union_1 X Y : set_Exists X set_Exists (X Y).
Proof. unfold set_Exists. solve_elem_of. Qed. Proof. unfold set_Exists. set_solver. Qed.
Lemma set_Exists_union_2 X Y : set_Exists Y set_Exists (X Y). Lemma set_Exists_union_2 X Y : set_Exists Y set_Exists (X Y).
Proof. unfold set_Exists. solve_elem_of. Qed. Proof. unfold set_Exists. set_solver. Qed.
Lemma set_Exists_union_inv X Y : Lemma set_Exists_union_inv X Y :
set_Exists (X Y) set_Exists X set_Exists Y. set_Exists (X Y) set_Exists X set_Exists Y.
Proof. unfold set_Exists. solve_elem_of. Qed. Proof. unfold set_Exists. set_solver. Qed.
End quantifiers. End quantifiers.
Section more_quantifiers. Section more_quantifiers.
...@@ -510,7 +510,7 @@ Section fresh. ...@@ -510,7 +510,7 @@ Section fresh.
Qed. Qed.
Lemma Forall_fresh_subseteq X Y xs : Lemma Forall_fresh_subseteq X Y xs :
Forall_fresh X xs Y X Forall_fresh Y xs. Forall_fresh X xs Y X Forall_fresh Y xs.
Proof. rewrite !Forall_fresh_alt; solve_elem_of. Qed. Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
Lemma fresh_list_length n X : length (fresh_list n X) = n. Lemma fresh_list_length n X : length (fresh_list n X) = n.
Proof. revert X. induction n; simpl; auto. Qed. Proof. revert X. induction n; simpl; auto. Qed.
...@@ -518,12 +518,12 @@ Section fresh. ...@@ -518,12 +518,12 @@ Section fresh.
Proof. Proof.
revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|]. revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|].
rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|]. rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
apply IH in Hin; solve_elem_of. apply IH in Hin; set_solver.
Qed. Qed.
Lemma NoDup_fresh_list n X : NoDup (fresh_list n X). Lemma NoDup_fresh_list n X : NoDup (fresh_list n X).
Proof. Proof.
revert X. induction n; simpl; constructor; auto. revert X. induction n; simpl; constructor; auto.
intros Hin; apply fresh_list_is_fresh in Hin; solve_elem_of. intros Hin; apply fresh_list_is_fresh in Hin; set_solver.
Qed. Qed.
Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X). Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X).
Proof. Proof.
...@@ -537,50 +537,50 @@ Section collection_monad. ...@@ -537,50 +537,50 @@ Section collection_monad.
Global Instance collection_fmap_mono {A B} : Global Instance collection_fmap_mono {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B). Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof. intros f g ? X Y ?; solve_elem_of. Qed. Proof. intros f g ? X Y ?; set_solver. Qed.
Global Instance collection_fmap_proper {A B} : Global Instance collection_fmap_proper {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B). Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof. intros f g ? X Y [??]; split; solve_elem_of. Qed. Proof. intros f g ? X Y [??]; split; set_solver. Qed.
Global Instance collection_bind_mono {A B} : Global Instance collection_bind_mono {A B} :
Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B). Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
Proof. unfold respectful; intros f g Hfg X Y ?; solve_elem_of. Qed. Proof. unfold respectful; intros f g Hfg X Y ?; set_solver. Qed.
Global Instance collection_bind_proper {A B} : Global Instance collection_bind_proper {A B} :
Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B). Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
Proof. unfold respectful; intros f g Hfg X Y [??]; split; solve_elem_of. Qed. Proof. unfold respectful; intros f g Hfg X Y [??]; split; set_solver. Qed.
Global Instance collection_join_mono {A} : Global Instance collection_join_mono {A} :
Proper (() ==> ()) (@mjoin M _ A). Proper (() ==> ()) (@mjoin M _ A).
Proof. intros X Y ?; solve_elem_of. Qed. Proof. intros X Y ?; set_solver. Qed.
Global Instance collection_join_proper {A} : Global Instance collection_join_proper {A} :
Proper (() ==> ()) (@mjoin M _ A). Proper (() ==> ()) (@mjoin M _ A).
Proof. intros X Y [??]; split; solve_elem_of. Qed. Proof. intros X Y [??]; split; set_solver. Qed.
Lemma collection_bind_singleton {A B} (f : A M B) x : {[ x ]} = f f x. Lemma collection_bind_singleton {A B} (f : A M B) x : {[ x ]} = f f x.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma collection_guard_True {A} `{Decision P} (X : M A) : P guard P; X X. Lemma collection_guard_True {A} `{Decision P} (X : M A) : P guard P; X X.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma collection_fmap_compose {A B C} (f : A B) (g : B C) (X : M A) : Lemma collection_fmap_compose {A B C} (f : A B) (g : B C) (X : M A) :
g f <$> X g <$> (f <$> X). g f <$> X g <$> (f <$> X).
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma elem_of_fmap_1 {A B} (f : A B) (X : M A) (y : B) : Lemma elem_of_fmap_1 {A B} (f : A B) (X : M A) (y : B) :
y f <$> X x, y = f x x X. y f <$> X x, y = f x x X.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma elem_of_fmap_2 {A B} (f : A B) (X : M A) (x : A) : Lemma elem_of_fmap_2 {A B} (f : A B) (X : M A) (x : A) :
x X f x f <$> X. x X f x f <$> X.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma elem_of_fmap_2_alt {A B} (f : A B) (X : M A) (x : A) (y : B) : Lemma elem_of_fmap_2_alt {A B} (f : A B) (X : M A) (x : A) (y : B) :
x X y = f x y f <$> X. x X y = f x y f <$> X.
Proof. solve_elem_of. Qed. Proof. set_solver. Qed.
Lemma elem_of_mapM {A B} (f : A M B) l k : Lemma elem_of_mapM {A B} (f : A M B) l k :
l mapM f k Forall2 (λ x y, x f y) l k. l mapM f k Forall2 (λ x y, x f y) l k.
Proof. Proof.
split. split.
- revert l. induction k; solve_elem_of. - revert l. induction k; set_solver.
- induction 1; solve_elem_of. - induction 1; set_solver.
Qed. Qed.
Lemma collection_mapM_length {A B} (f : A M B) l k : Lemma collection_mapM_length {A B} (f : A M B) l k :
l mapM f k length l = length k. l mapM f k length l = length k.
Proof. revert l; induction k; solve_elem_of. Qed. Proof. revert l; induction k; set_solver. Qed.
Lemma elem_of_mapM_fmap {A B} (f : A B) (g : B M A) l k : Lemma elem_of_mapM_fmap {A B} (f : A B) (g : B M A) l k :
Forall (λ x, y, y g x f y = x) l k mapM g l fmap f k = l. Forall (λ x, y, y g x f y = x) l k mapM g l fmap f k = l.
Proof. Proof.
...@@ -606,7 +606,7 @@ Section finite. ...@@ -606,7 +606,7 @@ Section finite.
Context `{SimpleCollection A B}. Context `{SimpleCollection A B}.
Global Instance set_finite_subseteq : Global Instance set_finite_subseteq :
Proper (flip () ==> impl) (@set_finite A B _). Proper (flip () ==> impl) (@set_finite A B _).
Proof. intros X Y HX [l Hl]; exists l; solve_elem_of. Qed. Proof. intros X Y HX [l Hl]; exists l; set_solver. Qed.
Global Instance set_finite_proper : Proper (() ==> iff) (@set_finite A B _). Global Instance set_finite_proper : Proper (() ==> iff) (@set_finite A B _).
Proof. by intros X Y [??]; split; apply set_finite_subseteq. Qed. Proof. by intros X Y [??]; split; apply set_finite_subseteq. Qed.
Lemma empty_finite : set_finite . Lemma empty_finite : set_finite .
...@@ -619,9 +619,9 @@ Section finite. ...@@ -619,9 +619,9 @@ Section finite.
rewrite elem_of_union, elem_of_app; naive_solver. rewrite elem_of_union, elem_of_app; naive_solver.
Qed. Qed.
Lemma union_finite_inv_l X Y : set_finite (X Y) set_finite X. Lemma union_finite_inv_l X Y : set_finite (X Y) set_finite X.
Proof. intros [l ?]; exists l; solve_elem_of. Qed. Proof. intros [l ?]; exists l; set_solver. Qed.
Lemma union_finite_inv_r X Y : set_finite (X Y) set_finite Y. Lemma union_finite_inv_r X Y : set_finite (X Y) set_finite Y.
Proof. intros [l ?]; exists l; solve_elem_of. Qed. Proof. intros [l ?]; exists l; set_solver. Qed.
End finite. End finite.
Section more_finite. Section more_finite.
...@@ -636,6 +636,6 @@ Section more_finite. ...@@ -636,6 +636,6 @@ Section more_finite.
set_finite Y set_finite (X Y) set_finite X. set_finite Y set_finite (X Y) set_finite X.
Proof. Proof.
intros [l ?] [k ?]; exists (l ++ k). intros [l ?] [k ?]; exists (l ++ k).
intros x ?; destruct (decide (x Y)); rewrite elem_of_app; solve_elem_of. intros x ?; destruct (decide (x Y)); rewrite elem_of_app; set_solver.
Qed. Qed.
End more_finite. End more_finite.
...@@ -41,7 +41,7 @@ Qed. ...@@ -41,7 +41,7 @@ Qed.
Lemma elements_singleton x : elements {[ x ]} = [x]. Lemma elements_singleton x : elements {[ x ]} = [x].
Proof. Proof.
apply Permutation_singleton. by rewrite <-(right_id () {[x]}), apply Permutation_singleton. by rewrite <-(right_id () {[x]}),
elements_union_singleton, elements_empty by solve_elem_of. elements_union_singleton, elements_empty by set_solver.
Qed. Qed.
Lemma elements_contains X Y : X Y elements X `contains` elements Y. Lemma elements_contains X Y : X Y elements X `contains` elements Y.
Proof. Proof.
...@@ -90,7 +90,7 @@ Proof. ...@@ -90,7 +90,7 @@ Proof.
intros E. destruct (size_pos_elem_of X); auto with lia. intros E. destruct (size_pos_elem_of X); auto with lia.
exists x. apply elem_of_equiv. split. exists x. apply elem_of_equiv. split.
- rewrite elem_of_singleton. eauto using size_singleton_inv. - rewrite elem_of_singleton. eauto using size_singleton_inv.
- solve_elem_of. - set_solver.
Qed. Qed.
Lemma size_union X Y : X Y size (X Y) = size X + size Y. Lemma size_union X Y : X Y size (X Y) = size X + size Y.
Proof. Proof.
...@@ -98,7 +98,7 @@ Proof. ...@@ -98,7 +98,7 @@ Proof.
apply Permutation_length, NoDup_Permutation. apply Permutation_length, NoDup_Permutation.
- apply NoDup_elements. - apply NoDup_elements.
- apply NoDup_app; repeat split; try apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements.
intros x; rewrite !elem_of_elements; solve_elem_of. intros x; rewrite !elem_of_elements; set_solver.
- intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Qed. Qed.
Instance elem_of_dec_slow (x : A) (X : C) : Decision (x X) | 100. Instance elem_of_dec_slow (x : A) (X : C) : Decision (x X) | 100.
...@@ -121,15 +121,15 @@ Next Obligation. ...@@ -121,15 +121,15 @@ Next Obligation.
Qed. Qed.
Lemma size_union_alt X Y : size (X Y) = size X + size (Y X). Lemma size_union_alt X Y : size (X Y) = size X + size (Y X).
Proof. Proof.
rewrite <-size_union by solve_elem_of. rewrite <-size_union by set_solver.
setoid_replace (Y X) with ((Y X) X) by solve_elem_of. setoid_replace (Y X) with ((Y X) X) by set_solver.
rewrite <-union_difference, (comm ()); solve_elem_of. rewrite <-union_difference, (comm ()); set_solver.
Qed. Qed.
Lemma subseteq_size X Y : X Y size X size Y. Lemma subseteq_size X Y : X Y size X size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed. Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Lemma subset_size X Y : X Y size X < size Y. Lemma subset_size X Y : X Y size X < size Y.
Proof. Proof.
intros. rewrite (union_difference X Y) by solve_elem_of. intros. rewrite (union_difference X Y) by set_solver.
rewrite size_union_alt, difference_twice. rewrite size_union_alt, difference_twice.
cut (size (Y X) 0); [lia |]. cut (size (Y X) 0); [lia |].
by apply size_non_empty_iff, non_empty_difference. by apply size_non_empty_iff, non_empty_difference.
...@@ -143,8 +143,8 @@ Proof. ...@@ -143,8 +143,8 @@ Proof.
intros ? Hemp Hadd. apply well_founded_induction with (). intros ? Hemp Hadd. apply well_founded_induction with ().
{ apply collection_wf. } { apply collection_wf. }
intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX]. intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
- rewrite (union_difference {[ x ]} X) by solve_elem_of. - rewrite (union_difference {[ x ]} X) by set_solver.
apply Hadd. solve_elem_of. apply IH; solve_elem_of. apply Hadd. set_solver. apply IH; set_solver.
- by rewrite HX. - by rewrite HX.
Qed. Qed.
Lemma collection_fold_ind {B} (P : B C Prop) (f : A B B) (b : B) : Lemma collection_fold_ind {B} (P : B C Prop) (f : A B B) (b : B) :
...@@ -158,10 +158,10 @@ Proof. ...@@ -158,10 +158,10 @@ Proof.
symmetry. apply elem_of_elements. } symmetry. apply elem_of_elements. }
induction 1 as [|x l ?? IH]; simpl. induction 1 as [|x l ?? IH]; simpl.
- intros X HX. setoid_rewrite elem_of_nil in HX. - intros X HX. setoid_rewrite elem_of_nil in HX.
rewrite equiv_empty. done. solve_elem_of. rewrite equiv_empty. done. set_solver.
- intros X HX. setoid_rewrite elem_of_cons in HX. - intros X HX. setoid_rewrite elem_of_cons in HX.
rewrite (union_difference {[ x ]} X) by solve_elem_of. rewrite (union_difference {[ x ]} X) by set_solver.
apply Hadd. solve_elem_of. apply IH. solve_elem_of. apply Hadd. set_solver. apply IH. set_solver.
Qed. Qed.
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R} Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
(f : A B B) (b : B) `{!Proper ((=) ==> R ==> R) f} (f : A B B) (b : B) `{!Proper ((=) ==> R ==> R) f}
......
...@@ -36,13 +36,13 @@ Proof. ...@@ -36,13 +36,13 @@ Proof.
Qed. Qed.
Lemma dom_empty {A} : dom D (@empty (M A) _) . Lemma dom_empty {A} : dom D (@empty (M A) _) .
Proof. Proof.
split; intro; [|solve_elem_of]. split; intro; [|set_solver].
rewrite elem_of_dom, lookup_empty. by inversion 1. rewrite elem_of_dom, lookup_empty. by inversion 1.
Qed.