Skip to content
Snippets Groups Projects

Draft: Very preliminary version of a quick start guide for sets.

Open Draft: Very preliminary version of a quick start guide for sets.
robbert/set_guide into master
14 unresolved threads
Open Robbert Krebbers requested to merge robbert/set_guide into master
14 unresolved threads

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
guides/sets.v 0 → 100644
36 Lemma some_stuff (X Y Z : gset nat) :
37 X ∪ Y ∩ X ∪ Z ∩ X = (Y ∪ X ∪ Z ∖ ∅ ∪ X) ∩ X.
38 Proof. set_solver. Qed.
39
40 Lemma some_stuff_poly `{Countable A} (X Y Z : gset nat) :
41 X ∪ Y ∩ X ∪ Z ∩ X = (Y ∪ X ∪ Z ∖ ∅ ∪ X) ∩ X.
42 Proof. set_solver. Qed.
43
44 (** If you want to search for lemmas, search for the operations, not [gset]
45 since all lemmas are overloaded. *)
46
47 Search difference intersection.
48
49 (** Some important notes:
50
51 - The lemmas look a bit dounting because of the additional arguments due to
  • Simon Gregersen
    Simon Gregersen @simongregersen
    Contributor
    Suggested change
    51 - The lemmas look a bit dounting because of the additional arguments due to
    51 - The lemmas look a bit daunting because of the additional arguments due to
  • Ralf Jung
    Ralf Jung @jung
    Owner

    Also it'd be good to print such a lemma statement here, so people can read this without having an active Coq buffer.

  • Please register or sign in to reply
  • Simon Gregersen
    Simon Gregersen @simongregersen started a thread on the diff
    • guides/sets.v 0 → 100644
    19 - [union], notation [∪]
    20 - [intersection], notation [∩]
    21 - [difference], notation [∖]
    22 *)
    23
    24 (* Let us try to type check some stuff. *)
    25
    26 Check {[ 10 ]} : gset nat.
    27
    28 Check {[ [10] ]} : gset (list nat).
    29
    30 Check {[ {[ 10 ]} ]} : gset (gset nat).
    31
    32 Check (λ X : gset nat, X ∪ {[ 10 ]}).
    33
    34 (** And let write some lemmas. The most useful tactic is [set_solver]. *)
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    66 set_map S X.
    67 Definition until_n (n : nat) : gset nat :=
    68 set_seq 0 n.
    69
    70 (** Keep in mind that [filter], [set_map], [set_seq], etc are overloaded via
    71 type classes. So, you need sufficient type information in your definitions and
    72 you won't find much about them when searching for [gset]. *)
    73
    74 (** When computing with sets, always make sure to cast the result that you want
    75 to display is a simple type like [nat], [list nat], [bool], etc. The result
    76 of a [gset] computation is a big sigma type with lots of noise, so it won't be
    77 pretty (or useful) to look at. *)
    78
    79 Eval vm_compute in (elements (add_one (evens {[ 10; 11; 14 ]}))).
    80 Eval vm_compute in (elements (evens (until_n 40))).
    81 (** [elements] converts a set to a list. They are not sorted, but you can do
  • Paolo G. Giarrusso
    Paolo G. Giarrusso @Blaisorblade started a thread on the diff
    • guides/sets.v 0 → 100644
    9 Check gset.
    10
    11 (* All the set operations are overloaded via type classes, but there are
    12 instances for [gset]. The most important operations are:
    13
    14 - [elem_of], notation [∈]
    15 - [subseteq], notation [⊆]
    16 - [subset], notation [⊂]
    17 - [empty], notation [∅]
    18 - [singleton], notation [ {[ x ]} ]
    19 - [union], notation [∪]
    20 - [intersection], notation [∩]
    21 - [difference], notation [∖]
    22 *)
    23
    24 (* Let us try to type check some stuff. *)
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    73
    74 (** When computing with sets, always make sure to cast the result that you want
    75 to display is a simple type like [nat], [list nat], [bool], etc. The result
    76 of a [gset] computation is a big sigma type with lots of noise, so it won't be
    77 pretty (or useful) to look at. *)
    78
    79 Eval vm_compute in (elements (add_one (evens {[ 10; 11; 14 ]}))).
    80 Eval vm_compute in (elements (evens (until_n 40))).
    81 (** [elements] converts a set to a list. They are not sorted, but you can do
    82 that yourself. *)
    83 Eval vm_compute in (merge_sort (≤) (elements (evens (until_n 40)))).
    84 Eval vm_compute in (fresh ({[ 10; 12 ]} : gset nat)).
    85 Eval vm_compute in (size ({[ 10; 12 ]} : gset nat)).
    86 (** You can use [bool_decide] to turn decidable [Prop]s into [bool]s. *)
    87 Eval vm_compute in bool_decide (10 ∈ evens {[ 10; 11 ]}).
    88 Eval vm_compute in (bool_decide ({[ 10; 14; 17 ]} ⊂ until_n 40)).
  • Ralf Jung
    Ralf Jung @jung
    Owner
    • It would be good to give this a bit more structure (e.g. via coqdoc sections).
    • Suggested folder name: docs
    • Mention the guides in that folder in the README
    • add this to Makefile
    Edited by Ralf Jung
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    1 From stdpp Require Import gmap sorting.
    2
    3 (* [gset K] is the type of sets you probably want to use. It enjoys good
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    29
    30 Check {[ {[ 10 ]} ]} : gset (gset nat).
    31
    32 Check (λ X : gset nat, X ∪ {[ 10 ]}).
    33
    34 (** And let write some lemmas. The most useful tactic is [set_solver]. *)
    35
    36 Lemma some_stuff (X Y Z : gset nat) :
    37 X ∪ Y ∩ X ∪ Z ∩ X = (Y ∪ X ∪ Z ∖ ∅ ∪ X) ∩ X.
    38 Proof. set_solver. Qed.
    39
    40 Lemma some_stuff_poly `{Countable A} (X Y Z : gset nat) :
    41 X ∪ Y ∩ X ∪ Z ∩ X = (Y ∪ X ∪ Z ∖ ∅ ∪ X) ∩ X.
    42 Proof. set_solver. Qed.
    43
    44 (** If you want to search for lemmas, search for the operations, not [gset]
    • Ralf Jung
      Ralf Jung @jung
      Owner
      Suggested change
      44 (** If you want to search for lemmas, search for the operations, not [gset]
      44 (** If you want to search for lemmas, search for the operations (using their typeclass names), not [gset]
    • Please register or sign in to reply
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    27
    28 Check {[ [10] ]} : gset (list nat).
    29
    30 Check {[ {[ 10 ]} ]} : gset (gset nat).
    31
    32 Check (λ X : gset nat, X ∪ {[ 10 ]}).
    33
    34 (** And let write some lemmas. The most useful tactic is [set_solver]. *)
    35
    36 Lemma some_stuff (X Y Z : gset nat) :
    37 X ∪ Y ∩ X ∪ Z ∩ X = (Y ∪ X ∪ Z ∖ ∅ ∪ X) ∩ X.
    38 Proof. set_solver. Qed.
    39
    40 Lemma some_stuff_poly `{Countable A} (X Y Z : gset nat) :
    41 X ∪ Y ∩ X ∪ Z ∩ X = (Y ∪ X ∪ Z ∖ ∅ ∪ X) ∩ X.
    42 Proof. set_solver. Qed.
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    47 Search difference intersection.
    48
    49 (** Some important notes:
    50
    51 - The lemmas look a bit dounting because of the additional arguments due to
    52 type classes, but these arguments can mostly be ignored
    53 - There are both lemmas about Leibniz equality [=] and setoid equality [≡].
    54 The first ones are suffixed [_L]. For [gset] you always want to use [=] (and
    55 thus the [_L] lemmas) because we have [X ≡ Y ↔ X = Y]. This is not the case
    56 for other implementations of sets, like [propset A := A → Prop] or
    57 [listset A := list A], hence [≡] is useful in the general case. *)
    58
    59 (** Some other examples *)
    60
    61 Definition evens (X : gset nat) : gset nat :=
    62 filter (λ x, (2 | x)) X.
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    49 (** Some important notes:
    50
    51 - The lemmas look a bit dounting because of the additional arguments due to
    52 type classes, but these arguments can mostly be ignored
    53 - There are both lemmas about Leibniz equality [=] and setoid equality [≡].
    54 The first ones are suffixed [_L]. For [gset] you always want to use [=] (and
    55 thus the [_L] lemmas) because we have [X ≡ Y ↔ X = Y]. This is not the case
    56 for other implementations of sets, like [propset A := A → Prop] or
    57 [listset A := list A], hence [≡] is useful in the general case. *)
    58
    59 (** Some other examples *)
    60
    61 Definition evens (X : gset nat) : gset nat :=
    62 filter (λ x, (2 | x)) X.
    63 Definition intersection_alt (X Y : gset nat) : gset nat :=
    64 filter (.∈ Y) X.
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    57 [listset A := list A], hence [≡] is useful in the general case. *)
    58
    59 (** Some other examples *)
    60
    61 Definition evens (X : gset nat) : gset nat :=
    62 filter (λ x, (2 | x)) X.
    63 Definition intersection_alt (X Y : gset nat) : gset nat :=
    64 filter (.∈ Y) X.
    65 Definition add_one (X : gset nat) : gset nat :=
    66 set_map S X.
    67 Definition until_n (n : nat) : gset nat :=
    68 set_seq 0 n.
    69
    70 (** Keep in mind that [filter], [set_map], [set_seq], etc are overloaded via
    71 type classes. So, you need sufficient type information in your definitions and
    72 you won't find much about them when searching for [gset]. *)
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    68 set_seq 0 n.
    69
    70 (** Keep in mind that [filter], [set_map], [set_seq], etc are overloaded via
    71 type classes. So, you need sufficient type information in your definitions and
    72 you won't find much about them when searching for [gset]. *)
    73
    74 (** When computing with sets, always make sure to cast the result that you want
    75 to display is a simple type like [nat], [list nat], [bool], etc. The result
    76 of a [gset] computation is a big sigma type with lots of noise, so it won't be
    77 pretty (or useful) to look at. *)
    78
    79 Eval vm_compute in (elements (add_one (evens {[ 10; 11; 14 ]}))).
    80 Eval vm_compute in (elements (evens (until_n 40))).
    81 (** [elements] converts a set to a list. They are not sorted, but you can do
    82 that yourself. *)
    83 Eval vm_compute in (merge_sort (≤) (elements (evens (until_n 40)))).
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • guides/sets.v 0 → 100644
    76 of a [gset] computation is a big sigma type with lots of noise, so it won't be
    77 pretty (or useful) to look at. *)
    78
    79 Eval vm_compute in (elements (add_one (evens {[ 10; 11; 14 ]}))).
    80 Eval vm_compute in (elements (evens (until_n 40))).
    81 (** [elements] converts a set to a list. They are not sorted, but you can do
    82 that yourself. *)
    83 Eval vm_compute in (merge_sort (≤) (elements (evens (until_n 40)))).
    84 Eval vm_compute in (fresh ({[ 10; 12 ]} : gset nat)).
    85 Eval vm_compute in (size ({[ 10; 12 ]} : gset nat)).
    86 (** You can use [bool_decide] to turn decidable [Prop]s into [bool]s. *)
    87 Eval vm_compute in bool_decide (10 ∈ evens {[ 10; 11 ]}).
    88 Eval vm_compute in (bool_decide ({[ 10; 14; 17 ]} ⊂ until_n 40)).
    89 Eval vm_compute in (bool_decide (set_Forall (λ x, (2 | x)) (evens (until_n 40)))).
    90
    91 (** Want to know more:
  • Ralf Jung added S-waiting-for-author label

    added S-waiting-for-author label

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers started a thread on the diff
    • guides/sets.v 0 → 100644
    25
    26 Check {[ 10 ]} : gset nat.
    27
    28 Check {[ [10] ]} : gset (list nat).
    29
    30 Check {[ {[ 10 ]} ]} : gset (gset nat).
    31
    32 Check (λ X : gset nat, X ∪ {[ 10 ]}).
    33
    34 (** And let write some lemmas. The most useful tactic is [set_solver]. *)
    35
    36 Lemma some_stuff (X Y Z : gset nat) :
    37 X ∪ Y ∩ X ∪ Z ∩ X = (Y ∪ X ∪ Z ∖ ∅ ∪ X) ∩ X.
    38 Proof. set_solver. Qed.
    39
    40 Lemma some_stuff_poly `{Countable A} (X Y Z : gset nat) :
  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers
    Author Owner

    Comment for myself: Also include a bit about defining Countable instances for custom types.

    • Please register or sign in to reply