Commit a9be1e26 by Robbert Krebbers

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 65ab1289
 ... ... @@ -46,16 +46,16 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts := (** Tactic setup *) Hint Resolve Step. Hint Extern 10 (equiv (A:=set _) _ _) => solve_elem_of : sts. Hint Extern 10 (¬equiv (A:=set _) _ _) => solve_elem_of : sts. Hint Extern 10 (_ ∈ _) => solve_elem_of : sts. Hint Extern 10 (_ ⊆ _) => solve_elem_of : sts. Hint Extern 10 (equiv (A:=set _) _ _) => set_solver : sts. Hint Extern 10 (¬equiv (A:=set _) _ _) => set_solver : sts. Hint Extern 10 (_ ∈ _) => set_solver : sts. Hint Extern 10 (_ ⊆ _) => set_solver : sts. (** ** Setoids *) Instance framestep_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step. Proof. intros ?? HT ?? <- ?? <-; destruct 1; econstructor; eauto with sts; solve_elem_of. eauto with sts; set_solver. Qed. Global Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step. Proof. by intros ?? [??] ??????; split; apply framestep_mono. Qed. ... ... @@ -84,7 +84,7 @@ Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed. (** ** Properties of closure under frame steps *) Lemma closed_disjoint' S T s : closed S T → s ∈ S → tok s ∩ T ≡ ∅. Proof. intros [_ ? _]; solve_elem_of. Qed. Proof. intros [_ ? _]; set_solver. Qed. Lemma closed_steps S T s1 s2 : closed S T → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S. Proof. induction 3; eauto using closed_step. Qed. ... ... @@ -92,7 +92,7 @@ Lemma closed_op T1 T2 S1 S2 : closed S1 T1 → closed S2 T2 → T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (S1 ∩ S2) (T1 ∪ T2). Proof. intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|]. intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|set_solver|]. intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split. - apply Hstep1 with s3, Frame_step with T3 T4; auto with sts. - apply Hstep2 with s3, Frame_step with T3 T4; auto with sts. ... ... @@ -103,7 +103,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf : Proof. inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto. - eapply Hstep with s1, Frame_step with T1 T2; auto with sts. - solve_elem_of -Hstep Hs1 Hs2. - set_solver -Hstep Hs1 Hs2. Qed. (** ** Properties of the closure operators *) ... ... @@ -117,7 +117,7 @@ Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ∩ T ⊆ ∅) → S ≢ ∅ → closed (up_set S T) T. Proof. intros HS Hne; unfold up_set; split. - assert (∀ s, s ∈ up s T) by eauto using elem_of_up. solve_elem_of. - assert (∀ s, s ∈ up s T) by eauto using elem_of_up. set_solver. - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs'). specialize (HS s' Hs'); clear Hs' Hne S. induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done. ... ... @@ -130,7 +130,7 @@ Proof. eauto using closed_up_set with sts. Qed. Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed (up s T) T. Proof. intros; rewrite -(collection_bind_singleton (λ s, up s T) s). apply closed_up_set; solve_elem_of. apply closed_up_set; set_solver. Qed. Lemma closed_up_empty s : closed (up s ∅) ∅. Proof. eauto using closed_up with sts. Qed. ... ... @@ -198,10 +198,10 @@ Instance sts_minus : Minus (car sts) := λ x1 x2, | auth s T1, auth _ T2 => frag (up s (T1 ∖ T2)) (T1 ∖ T2) end. Hint Extern 10 (equiv (A:=set _) _ _) => solve_elem_of : sts. Hint Extern 10 (¬equiv (A:=set _) _ _) => solve_elem_of : sts. Hint Extern 10 (_ ∈ _) => solve_elem_of : sts. Hint Extern 10 (_ ⊆ _) => solve_elem_of : sts. Hint Extern 10 (equiv (A:=set _) _ _) => set_solver : sts. Hint Extern 10 (¬equiv (A:=set _) _ _) => set_solver : sts. Hint Extern 10 (_ ∈ _) => set_solver : sts. Hint Extern 10 (_ ⊆ _) => set_solver : sts. Instance sts_equivalence: Equivalence ((≡) : relation (car sts)). Proof. split. ... ... @@ -220,7 +220,7 @@ Proof. - by do 2 destruct 1; constructor; setoid_subst. - assert (∀ T T' S s, closed S T → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅). { intros S T T' s [??]; solve_elem_of. } { intros S T T' s [??]; set_solver. } destruct 3; simpl in *; auto using closed_op with sts. - intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts. - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst; ... ... @@ -233,7 +233,7 @@ Proof. - destruct 3; constructor; auto with sts. - intros [|S T]; constructor; auto using elem_of_up with sts. assert (S ⊆ up_set S ∅ ∧ S ≢ ∅) by eauto using subseteq_up_set, closed_ne. solve_elem_of. set_solver. - intros [|S T]; constructor; auto with sts. assert (S ⊆ up_set S ∅); auto using subseteq_up_set with sts. - intros [s T|S T]; constructor; auto with sts. ... ... @@ -241,7 +241,7 @@ Proof. + rewrite (up_closed (up_set _ _)); eauto using closed_up_set, closed_ne with sts. - intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_ands. + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of. + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver. + destruct Hxz; inversion_clear Hy; simpl; auto using closed_up_set_empty, closed_up_empty with sts. + destruct Hxz; inversion_clear Hy; constructor; ... ... @@ -324,9 +324,9 @@ Proof. by move=> /(_ 0) [? [? Hdisj]]; inversion Hdisj. Qed. Lemma sts_op_auth_frag s S T : s ∈ S → closed S T → sts_auth s ∅ ⋅ sts_frag S T ≡ sts_auth s T. Proof. intros; split; [split|constructor; solve_elem_of]; simpl. intros; split; [split|constructor; set_solver]; simpl. - intros (?&?&?); by apply closed_disjoint' with S. - intros; split_ands. solve_elem_of+. done. constructor; solve_elem_of. - intros; split_ands. set_solver+. done. constructor; set_solver. Qed. Lemma sts_op_auth_frag_up s T : tok s ∩ T ≡ ∅ → sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T. ... ... @@ -339,7 +339,7 @@ Proof. intros HT HS1 HS2. rewrite /sts_frag. (* FIXME why does rewrite not work?? *) etransitivity; last eapply to_validity_op; try done; []. intros Hval. constructor; last solve_elem_of. eapply closed_ne, Hval. intros Hval. constructor; last set_solver. eapply closed_ne, Hval. Qed. (** Frame preserving updates *) ... ... @@ -356,8 +356,8 @@ Lemma sts_update_frag S1 S2 T : Proof. rewrite /sts_frag=> HS Hcl. apply validity_update. inversion 3 as [|? S ? Tf|]; simplify_eq/=. - split; first done. constructor; [solve_elem_of|done]. - split; first done. constructor; solve_elem_of. - split; first done. constructor; [set_solver|done]. - split; first done. constructor; set_solver. Qed. Lemma sts_update_frag_up s1 S2 T : ... ... @@ -388,16 +388,16 @@ when we have RAs back *) + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done. destruct Hscl as [s' [Hsup Hs']]. eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done. solve_elem_of +HS Hs'. set_solver +HS Hs'. - intros (Hcl1 & Tf & Htk & Hf & Hs). exists (sts_frag (up_set S2 Tf) Tf). split; first split; simpl;[|done|]. + intros _. split_ands; first done. * apply closed_up_set; last by eapply closed_ne. move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2). solve_elem_of +Htk. set_solver +Htk. * constructor; last done. rewrite -Hs. by eapply closed_ne. + intros _. constructor; [ solve_elem_of +Htk | done]. + intros _. constructor; [ set_solver +Htk | done]. Qed. Lemma sts_frag_included' S1 S2 T : ... ... @@ -405,6 +405,6 @@ Lemma sts_frag_included' S1 S2 T : sts_frag S1 T ≼ sts_frag S2 T. Proof. intros. apply sts_frag_included; split_ands; auto. exists ∅; split_ands; done || solve_elem_of+. exists ∅; split_ands; done || set_solver+. Qed. End stsRA.
 ... ... @@ -178,8 +178,8 @@ Section gset. Lemma big_sepS_delete P X x : x ∈ X → (Π★{set X} P)%I ≡ (P x ★ Π★{set X ∖ {[ x ]}} P)%I. Proof. intros. rewrite -big_sepS_insert; last solve_elem_of. by rewrite -union_difference_L; last solve_elem_of. intros. rewrite -big_sepS_insert; last set_solver. by rewrite -union_difference_L; last set_solver. Qed. Lemma big_sepS_singleton P x : (Π★{set {[ x ]}} P)%I ≡ (P x)%I. Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed. ... ...
 ... ... @@ -57,11 +57,11 @@ Module barrier_proto. rewrite /= /tok /=. intros. apply dec_stable. assert (Change i ∉ change_tokens I1) as HI1 by (rewrite mkSet_not_elem_of; solve_elem_of +Hs1). by (rewrite mkSet_not_elem_of; set_solver +Hs1). assert (Change i ∉ change_tokens I2) as HI2. { destruct p. - solve_elem_of +Htok Hdisj HI1. - solve_elem_of +Htok Hdisj HI1 / discriminate. } - set_solver +Htok Hdisj HI1. - set_solver +Htok Hdisj HI1 / discriminate. } done. Qed. ... ... @@ -74,13 +74,13 @@ Module barrier_proto. split. - apply (non_empty_inhabited(State Low ∅)). by rewrite !mkSet_elem_of /=. - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI. destruct p; last done. solve_elem_of. destruct p; last done. set_solver. - move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep. inversion_clear Hstep as [T1 T2 Hdisj Hstep']. inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok]. destruct Htrans; move:Hs1 Hdisj Htok =>/=; first by destruct p. rewrite /= /tok /=. intros. solve_elem_of +Hdisj Htok. rewrite /= /tok /=. intros. set_solver +Hdisj Htok. Qed. End barrier_proto. ... ... @@ -162,23 +162,23 @@ Section proof. { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. } rewrite (sts_own_weaken ⊤ _ _ (i_states i ∩ low_states) _ ({[ Change i ]} ∪ {[ Send ]})). + apply pvs_mono. rewrite sts_ownS_op; first done. * solve_elem_of. * set_solver. * apply i_states_closed. * apply low_states_closed. + rewrite /= /tok /=. apply elem_of_equiv=>t. rewrite elem_of_difference elem_of_union. rewrite !mkSet_elem_of /change_tokens. (* TODO: destruct t; solve_elem_of does not work. What is the best way to do on? *) (* TODO: destruct t; set_solver does not work. What is the best way to do on? *) destruct t as [i'|]; last by naive_solver. split. * move=>[_ Hn]. left. destruct (decide (i = i')); first by subst i. exfalso. apply Hn. left. solve_elem_of. * move=>[[EQ]|?]; last discriminate. solve_elem_of. + apply elem_of_intersection. rewrite !mkSet_elem_of /=. solve_elem_of. exfalso. apply Hn. left. set_solver. * move=>[[EQ]|?]; last discriminate. set_solver. + apply elem_of_intersection. rewrite !mkSet_elem_of /=. set_solver. + apply sts.closed_op. * apply i_states_closed. * apply low_states_closed. * solve_elem_of. * set_solver. * apply (non_empty_inhabited (State Low {[ i ]})). apply elem_of_intersection. rewrite !mkSet_elem_of /=. solve_elem_of. rewrite !mkSet_elem_of /=. set_solver. Qed. Lemma signal_spec l P (Q : val → iProp) : ... ... @@ -199,7 +199,7 @@ Section proof. erewrite later_sep. apply sep_mono_r. apply later_intro. } apply wand_intro_l. rewrite -(exist_intro (State High I)). rewrite -(exist_intro ∅). rewrite const_equiv /=; last first. { constructor; first constructor; rewrite /= /tok /=; solve_elem_of. } { constructor; first constructor; rewrite /= /tok /=; set_solver. } rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r. rewrite !assoc [(_ ★ P)%I]comm !assoc -2!assoc. apply sep_mono; last first. ... ...
 ... ... @@ -207,7 +207,7 @@ Ltac decompose_empty := repeat occurrences of [(∪)], [(∩)], [(∖)], [(<\$>)], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into [A → x ∈ X ∨ False]. *) Ltac unfold_elem_of := Ltac set_unfold := repeat_on_hyps (fun H => repeat match type of H with | context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq in H ... ... @@ -251,21 +251,21 @@ Ltac unfold_elem_of := end. (** 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. *) Tactic Notation "solve_elem_of" tactic3(tac) := Tactic Notation "set_solver" tactic3(tac) := setoid_subst; decompose_empty; unfold_elem_of; set_unfold; naive_solver tac. Tactic Notation "solve_elem_of" "-" hyp_list(Hs) "/" tactic3(tac) := clear Hs; solve_elem_of tac. Tactic Notation "solve_elem_of" "+" hyp_list(Hs) "/" tactic3(tac) := revert Hs; clear; solve_elem_of tac. Tactic Notation "solve_elem_of" := solve_elem_of eauto. Tactic Notation "solve_elem_of" "-" hyp_list(Hs) := clear Hs; solve_elem_of. Tactic Notation "solve_elem_of" "+" hyp_list(Hs) := revert Hs; clear; solve_elem_of. Tactic Notation "set_solver" "-" hyp_list(Hs) "/" tactic3(tac) := clear Hs; set_solver tac. Tactic Notation "set_solver" "+" hyp_list(Hs) "/" tactic3(tac) := revert Hs; clear; set_solver tac. Tactic Notation "set_solver" := set_solver eauto. Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver. Tactic Notation "set_solver" "+" hyp_list(Hs) := revert Hs; clear; set_solver. (** * More theorems *) Section collection. ... ... @@ -273,7 +273,7 @@ Section collection. Implicit Types X Y : 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 : Proper ((≡) ==> (≡) ==> (≡)) (@difference C _). Proof. ... ... @@ -281,23 +281,23 @@ Section collection. by rewrite !elem_of_difference, HX, HY. Qed. 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]}. Proof. solve_elem_of. Qed. Proof. set_solver. Qed. 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 ≡ ∅. Proof. solve_elem_of. Qed. Proof. set_solver. Qed. 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. Proof. solve_elem_of. Qed. Proof. set_solver. Qed. 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. Proof. solve_elem_of. Qed. Proof. set_solver. Qed. Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y. Proof. solve_elem_of. Qed. Proof. set_solver. Qed. Section leibniz. Context `{!LeibnizEquiv C}. ... ... @@ -334,10 +334,10 @@ Section collection. Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅. Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x. destruct (decide (x ∈ X)); solve_elem_of. destruct (decide (x ∈ X)); set_solver. Qed. 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}. Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Proof. unfold_leibniz. apply union_difference. Qed. ... ... @@ -396,33 +396,33 @@ Section NoDup. Proof. firstorder. Qed. 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 ∅. 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. 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 : 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. Proof. unfold elem_of_upto. solve_elem_of. Qed. Proof. unfold elem_of_upto. set_solver. Qed. 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 : ¬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 : x ∉ X → set_NoDup ({[ x ]} ∪ X) → ¬elem_of_upto x X. Proof. intros Hin Hnodup [y [??]]. rewrite (Hnodup x y) in Hin; solve_elem_of. rewrite (Hnodup x y) in Hin; set_solver. Qed. 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. Proof. unfold set_NoDup. solve_elem_of. Qed. Proof. unfold set_NoDup. set_solver. Qed. End NoDup. (** * Quantifiers *) ... ... @@ -433,27 +433,27 @@ Section quantifiers. Definition set_Exists X := ∃ x, x ∈ X ∧ P x. 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. 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). 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. 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. Proof. unfold set_Forall. solve_elem_of. Qed. Proof. unfold set_Forall. set_solver. Qed. 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. 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). 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). Proof. unfold set_Exists. solve_elem_of. Qed. Proof. unfold set_Exists. set_solver. Qed. Lemma set_Exists_union_inv X 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. Section more_quantifiers. ... ... @@ -510,7 +510,7 @@ Section fresh. Qed. Lemma Forall_fresh_subseteq X 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. Proof. revert X. induction n; simpl; auto. Qed. ... ... @@ -518,12 +518,12 @@ Section fresh. Proof. revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|]. rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|]. apply IH in Hin; solve_elem_of. apply IH in Hin; set_solver. Qed. Lemma NoDup_fresh_list n X : NoDup (fresh_list n X). Proof. 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. Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X). Proof. ... ... @@ -537,50 +537,50 @@ Section collection_monad. Global Instance collection_fmap_mono {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} : 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} : 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} : 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} : 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} : 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. Proof. solve_elem_of. Qed. Proof. set_solver. Qed. 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) : 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) : 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) : 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) : 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 : l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k. Proof. split. - revert l. induction k; solve_elem_of. - induction 1; solve_elem_of. - revert l. induction k; set_solver. - induction 1; set_solver. Qed. Lemma collection_mapM_length {A B} (f : A → M B) l 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 : Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l. Proof. ... ... @@ -606,7 +606,7 @@ Section finite. Context `{SimpleCollection A B}. Global Instance set_finite_subseteq : 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 _). Proof. by intros X Y [??]; split; apply set_finite_subseteq. Qed. Lemma empty_finite : set_finite ∅. ... ... @@ -619,9 +619,9 @@ Section finite. rewrite elem_of_union, elem_of_app; naive_solver. Qed. 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. Proof. intros [l ?]; exists l; solve_elem_of. Qed. Proof. intros [l ?]; exists l; set_solver. Qed. End finite. Section more_finite. ... ... @@ -636,6 +636,6 @@ Section more_finite. set_finite Y → set_finite (X ∖ Y) → set_finite X. Proof. 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. End more_finite.
 ... ... @@ -41,7 +41,7 @@ Qed. Lemma elements_singleton x : elements {[ x ]} = [x]. Proof. 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. Lemma elements_contains X Y : X ⊆ Y → elements X `contains` elements Y. Proof. ... ... @@ -90,7 +90,7 @@ Proof. intros E. destruct (size_pos_elem_of X); auto with lia. exists x. apply elem_of_equiv. split. - rewrite elem_of_singleton. eauto using size_singleton_inv. - solve_elem_of. - set_solver. Qed. Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y. Proof. ... ... @@ -98,7 +98,7 @@ Proof. apply Permutation_length, NoDup_Permutation. - 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. Qed. Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. ... ... @@ -121,15 +121,15 @@ Next Obligation. Qed. Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). Proof. rewrite <-size_union by solve_elem_of. setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by solve_elem_of. rewrite <-union_difference, (comm (∪)); solve_elem_of. rewrite <-size_union by set_solver. setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by set_solver.