Skip to content

Commit d7960a8

Browse files
oxe-ioxe-i
authored
add custom-set (#151)
1 parent 66d0a5a commit d7960a8

File tree

14 files changed

+772
-0
lines changed

14 files changed

+772
-0
lines changed

‎config.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -586,6 +586,14 @@
586586
"prerequisites": [],
587587
"difficulty": 7
588588
},
589+
{
590+
"slug": "custom-set",
591+
"name": "Custom Set",
592+
"uuid": "d643def0-b87f-44b9-ab31-787d94d4f6a0",
593+
"practices": [],
594+
"prerequisites": [],
595+
"difficulty": 7
596+
},
589597
{
590598
"slug": "pythagorean-triplet",
591599
"name": "Pythagorean Triplet",

‎exercises/practice/custom-set/.docs/instructions.md‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
# Instructions
2+
3+
Create a custom set type.
4+
5+
Sometimes it is necessary to define a custom data structure of some type, like a set.
6+
In this exercise you will define your own set.
7+
How it works internally doesn't matter, as long as it behaves like a set of unique elements.

‎exercises/practice/custom-set/.meta/Example.lean‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
namespace CustomSet
2+
3+
abbrev Size := Nat
4+
5+
inductive Set where
6+
| nil : Set
7+
| node : Size → Nat → Set → Set → Set
8+
deriving Repr, Inhabited
9+
10+
instance : EmptyCollection Set :=
11+
⟨ .nil ⟩ -- takes care of ∅
12+
13+
private def Set.size : Set → Size
14+
| .nil => 0
15+
| .node s _ _ _ => s
16+
17+
private def Set.contains : Set → Nat → Bool
18+
| .nil, _ => false
19+
| .node _ x l r, e => e == x || if e < x then l.contains e else r.contains e
20+
21+
private def Set.foldl {α} (fn : α → Nat → α) (init : α) (set : Set) : α :=
22+
match set with
23+
| .nil => init
24+
| .node _ x l r =>
25+
let leftAcc := l.foldl fn init
26+
let acc := fn leftAcc x
27+
r.foldl fn acc
28+
29+
instance : BEq Set where -- takes care of == and !=
30+
beq s1 s2 := s1.size == s2.size && s1.foldl (fun acc x => acc && s2.contains x) true
31+
32+
instance : Membership Nat Set where -- takes care of ∈ and ∉
33+
mem s n := s.contains n
34+
35+
instance (a : Nat) (s : Set) : Decidable (a ∈ s) := by
36+
simp [Membership.mem]
37+
exact inferInstance
38+
39+
private def Set.subset (set1 set2 : Set) : Bool :=
40+
set1.foldl (fun acc x => acc && set2.contains x) true
41+
42+
instance : HasSubset Set where
43+
Subset s1 s2 := s1.subset s2
44+
45+
instance (s1 s2 : Set) : Decidable (s1 ⊆ s2) := by
46+
simp [HasSubset.Subset]
47+
exact inferInstance
48+
49+
notation a " ⊈ " b => ¬(a ⊆ b)
50+
51+
private def Set.addHelper (e : Nat) (s : Set) : Set :=
52+
match s with
53+
| .nil => .node 1 e .nil .nil
54+
| .node s x l r =>
55+
if e < x
56+
then Set.node (s + 1) x (l.addHelper e) r
57+
else Set.node (s + 1) x l (r.addHelper e)
58+
59+
def Set.add (elem : Nat) (set : Set) : Set :=
60+
if elem ∈ set then set
61+
else set.addHelper elem
62+
63+
def Set.ofList (xs : List Nat) : Set :=
64+
xs.foldl (fun acc x => acc.add x) ∅
65+
66+
instance : Inter Set where -- takes care of ∩
67+
inter s1 s2 := s1.foldl (fun acc x => if s2.contains x then acc.add x else acc) ∅
68+
69+
instance : Union Set where -- takes care of ∪
70+
union s1 s2 := s1.foldl (fun acc x => acc.add x) s2
71+
72+
instance : SDiff Set where -- takes care of \
73+
sdiff s1 s2 := s1.foldl (fun acc x => if s2.contains x then acc else acc.add x) ∅
74+
75+
def Set.disjoint (set1 set2 : Set) : Bool :=
76+
set1.foldl (fun acc x => acc && !set2.contains x) true
77+
78+
end CustomSet

‎exercises/practice/custom-set/.meta/config.json‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
{
2+
"authors": [
3+
"oxe-i"
4+
],
5+
"files": {
6+
"solution": [
7+
"CustomSet.lean"
8+
],
9+
"test": [
10+
"CustomSetTest.lean"
11+
],
12+
"example": [
13+
".meta/Example.lean"
14+
]
15+
},
16+
"blurb": "Create a custom set type."
17+
}

‎exercises/practice/custom-set/.meta/tests.toml‎

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
# This is an auto-generated file.
2+
#
3+
# Regenerating this file via `configlet sync` will:
4+
# - Recreate every `description` key/value pair
5+
# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
6+
# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
7+
# - Preserve any other key/value pair
8+
#
9+
# As user-added comments (using the # character) will be removed when this file
10+
# is regenerated, comments can be added via a `comment` key.
11+
12+
[20c5f855-f83a-44a7-abdd-fe75c6cf022b]
13+
description = "Returns true if the set contains no elements -> sets with no elements are empty"
14+
15+
[d506485d-5706-40db-b7d8-5ceb5acf88d2]
16+
description = "Returns true if the set contains no elements -> sets with elements are not empty"
17+
18+
[759b9740-3417-44c3-8ca3-262b3c281043]
19+
description = "Sets can report if they contain an element -> nothing is contained in an empty set"
20+
21+
[f83cd2d1-2a85-41bc-b6be-80adbff4be49]
22+
description = "Sets can report if they contain an element -> when the element is in the set"
23+
24+
[93423fc0-44d0-4bc0-a2ac-376de8d7af34]
25+
description = "Sets can report if they contain an element -> when the element is not in the set"
26+
27+
[c392923a-637b-4495-b28e-34742cd6157a]
28+
description = "A set is a subset if all of its elements are contained in the other set -> empty set is a subset of another empty set"
29+
30+
[5635b113-be8c-4c6f-b9a9-23c485193917]
31+
description = "A set is a subset if all of its elements are contained in the other set -> empty set is a subset of non-empty set"
32+
33+
[832eda58-6d6e-44e2-92c2-be8cf0173cee]
34+
description = "A set is a subset if all of its elements are contained in the other set -> non-empty set is not a subset of empty set"
35+
36+
[c830c578-8f97-4036-b082-89feda876131]
37+
description = "A set is a subset if all of its elements are contained in the other set -> set is a subset of set with exact same elements"
38+
39+
[476a4a1c-0fd1-430f-aa65-5b70cbc810c5]
40+
description = "A set is a subset if all of its elements are contained in the other set -> set is a subset of larger set with same elements"
41+
42+
[d2498999-3e46-48e4-9660-1e20c3329d3d]
43+
description = "A set is a subset if all of its elements are contained in the other set -> set is not a subset of set that does not contain its elements"
44+
45+
[7d38155e-f472-4a7e-9ad8-5c1f8f95e4cc]
46+
description = "Sets are disjoint if they share no elements -> the empty set is disjoint with itself"
47+
48+
[7a2b3938-64b6-4b32-901a-fe16891998a6]
49+
description = "Sets are disjoint if they share no elements -> empty set is disjoint with non-empty set"
50+
51+
[589574a0-8b48-48ea-88b0-b652c5fe476f]
52+
description = "Sets are disjoint if they share no elements -> non-empty set is disjoint with empty set"
53+
54+
[febeaf4f-f180-4499-91fa-59165955a523]
55+
description = "Sets are disjoint if they share no elements -> sets are not disjoint if they share an element"
56+
57+
[0de20d2f-c952-468a-88c8-5e056740f020]
58+
description = "Sets are disjoint if they share no elements -> sets are disjoint if they share no elements"
59+
60+
[4bd24adb-45da-4320-9ff6-38c044e9dff8]
61+
description = "Sets with the same elements are equal -> empty sets are equal"
62+
63+
[f65c0a0e-6632-4b2d-b82c-b7c6da2ec224]
64+
description = "Sets with the same elements are equal -> empty set is not equal to non-empty set"
65+
66+
[81e53307-7683-4b1e-a30c-7e49155fe3ca]
67+
description = "Sets with the same elements are equal -> non-empty set is not equal to empty set"
68+
69+
[d57c5d7c-a7f3-48cc-a162-6b488c0fbbd0]
70+
description = "Sets with the same elements are equal -> sets with the same elements are equal"
71+
72+
[dd61bafc-6653-42cc-961a-ab071ee0ee85]
73+
description = "Sets with the same elements are equal -> sets with different elements are not equal"
74+
75+
[06059caf-9bf4-425e-aaff-88966cb3ea14]
76+
description = "Sets with the same elements are equal -> set is not equal to larger set with same elements"
77+
78+
[d4a1142f-09aa-4df9-8b83-4437dcf7ec24]
79+
description = "Sets with the same elements are equal -> set is equal to a set constructed from an array with duplicates"
80+
81+
[8a677c3c-a658-4d39-bb88-5b5b1a9659f4]
82+
description = "Unique elements can be added to a set -> add to empty set"
83+
84+
[0903dd45-904d-4cf2-bddd-0905e1a8d125]
85+
description = "Unique elements can be added to a set -> add to non-empty set"
86+
87+
[b0eb7bb7-5e5d-4733-b582-af771476cb99]
88+
description = "Unique elements can be added to a set -> adding an existing element does not change the set"
89+
90+
[893d5333-33b8-4151-a3d4-8f273358208a]
91+
description = "Intersection returns a set of all shared elements -> intersection of two empty sets is an empty set"
92+
93+
[d739940e-def2-41ab-a7bb-aaf60f7d782c]
94+
description = "Intersection returns a set of all shared elements -> intersection of an empty set and non-empty set is an empty set"
95+
96+
[3607d9d8-c895-4d6f-ac16-a14956e0a4b7]
97+
description = "Intersection returns a set of all shared elements -> intersection of a non-empty set and an empty set is an empty set"
98+
99+
[b5120abf-5b5e-41ab-aede-4de2ad85c34e]
100+
description = "Intersection returns a set of all shared elements -> intersection of two sets with no shared elements is an empty set"
101+
102+
[af21ca1b-fac9-499c-81c0-92a591653d49]
103+
description = "Intersection returns a set of all shared elements -> intersection of two sets with shared elements is a set of the shared elements"
104+
105+
[c5e6e2e4-50e9-4bc2-b89f-c518f015b57e]
106+
description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of two empty sets is an empty set"
107+
108+
[2024cc92-5c26-44ed-aafd-e6ca27d6fcd2]
109+
description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of empty set and non-empty set is an empty set"
110+
111+
[e79edee7-08aa-4c19-9382-f6820974b43e]
112+
description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of a non-empty set and an empty set is the non-empty set"
113+
114+
[c5ac673e-d707-4db5-8d69-7082c3a5437e]
115+
description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of two non-empty sets is a set of elements that are only in the first set"
116+
117+
[20d0a38f-7bb7-4c4a-ac15-90c7392ecf2b]
118+
description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference removes all duplicates in the first set"
119+
120+
[c45aed16-5494-455a-9033-5d4c93589dc6]
121+
description = "Union returns a set of all elements in either set -> union of empty sets is an empty set"
122+
123+
[9d258545-33c2-4fcb-a340-9f8aa69e7a41]
124+
description = "Union returns a set of all elements in either set -> union of an empty set and non-empty set is the non-empty set"
125+
126+
[3aade50c-80c7-4db8-853d-75bac5818b83]
127+
description = "Union returns a set of all elements in either set -> union of a non-empty set and empty set is the non-empty set"
128+
129+
[a00bb91f-c4b4-4844-8f77-c73e2e9df77c]
130+
description = "Union returns a set of all elements in either set -> union of non-empty sets contains all unique elements"

‎exercises/practice/custom-set/CustomSet.lean‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
namespace CustomSet
2+
3+
/-
4+
Define here a Set type
5+
6+
It must have operators defined with the following semantics:
7+
* ∈, ∉ : an element is, or is not, in a Set
8+
* ⊆, ⊈ : a Set is, or is not, a subset of another
9+
* ==, != : two Sets have, or don't have, the same elements
10+
* ∩ : gets the intersection of two Sets
11+
* ∪ : gets the union of two Sets
12+
* \ : gets the difference of two Sets
13+
* ∅ : references an empty Set
14+
15+
In addition, at least three other functions must be defined:
16+
* Set.ofList, that takes a List Nat and returns a Set
17+
* Set.add, that adds a Nat to a Set, returning the new Set
18+
* Set.disjoint, that checks if two Sets are, or are not, disjoint
19+
-/
20+
21+
end CustomSet

‎exercises/practice/custom-set/CustomSetTest.lean‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
import LeanTest
2+
import CustomSet
3+
4+
open LeanTest
5+
6+
def customSetTests : TestSuite :=
7+
(TestSuite.empty "CustomSet")
8+
|>.addTest "Returns true if the set contains no elements -> sets with no elements are empty" (do
9+
return assertEqual ∅ <| CustomSet.Set.ofList [])
10+
|>.addTest "Returns true if the set contains no elements -> sets with elements are not empty" (do
11+
return assertNotEqual ∅ <| CustomSet.Set.ofList [1])
12+
|>.addTest "Sets can report if they contain an element -> nothing is contained in an empty set" (do
13+
return assert <| decide <| 1 ∉ CustomSet.Set.ofList [])
14+
|>.addTest "Sets can report if they contain an element -> when the element is in the set" (do
15+
return assert <| decide <| 1 ∈ CustomSet.Set.ofList [1, 2, 3])
16+
|>.addTest "Sets can report if they contain an element -> when the element is not in the set" (do
17+
return assert <| decide <| 4 ∉ CustomSet.Set.ofList [1, 2, 3])
18+
|>.addTest "A set is a subset if all of its elements are contained in the other set -> empty set is a subset of another empty set" (do
19+
return assert <| decide <| CustomSet.Set.ofList [] ⊆ CustomSet.Set.ofList [])
20+
|>.addTest "A set is a subset if all of its elements are contained in the other set -> empty set is a subset of non-empty set" (do
21+
return assert <| decide <| CustomSet.Set.ofList [] ⊆ CustomSet.Set.ofList [1])
22+
|>.addTest "A set is a subset if all of its elements are contained in the other set -> non-empty set is not a subset of empty set" (do
23+
return assert <| decide <| CustomSet.Set.ofList [1] ⊈ CustomSet.Set.ofList [])
24+
|>.addTest "A set is a subset if all of its elements are contained in the other set -> set is a subset of set with exact same elements" (do
25+
return assert <| decide <| CustomSet.Set.ofList [1, 2, 3] ⊆ CustomSet.Set.ofList [1, 2, 3])
26+
|>.addTest "A set is a subset if all of its elements are contained in the other set -> set is a subset of larger set with same elements" (do
27+
return assert <| decide <| CustomSet.Set.ofList [1, 2, 3] ⊆ CustomSet.Set.ofList [4, 1, 2, 3])
28+
|>.addTest "A set is a subset if all of its elements are contained in the other set -> set is not a subset of set that does not contain its elements" (do
29+
return assert <| decide <| CustomSet.Set.ofList [1, 2, 3] ⊈ CustomSet.Set.ofList [4, 1, 3])
30+
|>.addTest "Sets are disjoint if they share no elements -> the empty set is disjoint with itself" (do
31+
return assertTrue <| (CustomSet.Set.ofList []).disjoint <| CustomSet.Set.ofList [])
32+
|>.addTest "Sets are disjoint if they share no elements -> empty set is disjoint with non-empty set" (do
33+
return assertTrue <| (CustomSet.Set.ofList []).disjoint <| CustomSet.Set.ofList [1])
34+
|>.addTest "Sets are disjoint if they share no elements -> non-empty set is disjoint with empty set" (do
35+
return assertTrue <| (CustomSet.Set.ofList [1]).disjoint <| CustomSet.Set.ofList [])
36+
|>.addTest "Sets are disjoint if they share no elements -> sets are not disjoint if they share an element" (do
37+
return assertFalse <| (CustomSet.Set.ofList [1, 2]).disjoint <| CustomSet.Set.ofList [2, 3])
38+
|>.addTest "Sets are disjoint if they share no elements -> sets are disjoint if they share no elements" (do
39+
return assertTrue <| (CustomSet.Set.ofList [1, 2]).disjoint <| CustomSet.Set.ofList [3, 4])
40+
|>.addTest "Sets with the same elements are equal -> empty sets are equal" (do
41+
return assert <| CustomSet.Set.ofList [] == CustomSet.Set.ofList [])
42+
|>.addTest "Sets with the same elements are equal -> empty set is not equal to non-empty set" (do
43+
return assert <| CustomSet.Set.ofList [] != CustomSet.Set.ofList [1, 2, 3])
44+
|>.addTest "Sets with the same elements are equal -> non-empty set is not equal to empty set" (do
45+
return assert <| CustomSet.Set.ofList [1, 2, 3] != CustomSet.Set.ofList [])
46+
|>.addTest "Sets with the same elements are equal -> sets with the same elements are equal" (do
47+
return assert <| CustomSet.Set.ofList [1, 2] == CustomSet.Set.ofList [2, 1])
48+
|>.addTest "Sets with the same elements are equal -> sets with different elements are not equal" (do
49+
return assert <| CustomSet.Set.ofList [1, 2, 3] != CustomSet.Set.ofList [1, 2, 4])
50+
|>.addTest "Sets with the same elements are equal -> set is not equal to larger set with same elements" (do
51+
return assert <| CustomSet.Set.ofList [1, 2, 3] != CustomSet.Set.ofList [1, 2, 3, 4])
52+
|>.addTest "Sets with the same elements are equal -> set is equal to a set constructed from an array with duplicates" (do
53+
return assert <| CustomSet.Set.ofList [1] == CustomSet.Set.ofList [1, 1])
54+
|>.addTest "Unique elements can be added to a set -> add to empty set" (do
55+
return assertEqual (CustomSet.Set.ofList [3]) <| (CustomSet.Set.ofList []).add 3)
56+
|>.addTest "Unique elements can be added to a set -> add to non-empty set" (do
57+
return assertEqual (CustomSet.Set.ofList [1, 2, 3, 4]) <| (CustomSet.Set.ofList [1, 2, 4]).add 3)
58+
|>.addTest "Unique elements can be added to a set -> adding an existing element does not change the set" (do
59+
return assertEqual (CustomSet.Set.ofList [1, 2, 3]) <| (CustomSet.Set.ofList [1, 2, 3]).add 3)
60+
|>.addTest "Intersection returns a set of all shared elements -> intersection of two empty sets is an empty set" (do
61+
return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] ∩ CustomSet.Set.ofList [])
62+
|>.addTest "Intersection returns a set of all shared elements -> intersection of an empty set and non-empty set is an empty set" (do
63+
return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] ∩ CustomSet.Set.ofList [3, 2, 5])
64+
|>.addTest "Intersection returns a set of all shared elements -> intersection of a non-empty set and an empty set is an empty set" (do
65+
return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [1, 2, 3, 4] ∩ CustomSet.Set.ofList [])
66+
|>.addTest "Intersection returns a set of all shared elements -> intersection of two sets with no shared elements is an empty set" (do
67+
return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [1, 2, 3] ∩ CustomSet.Set.ofList [4, 5, 6])
68+
|>.addTest "Intersection returns a set of all shared elements -> intersection of two sets with shared elements is a set of the shared elements" (do
69+
return assertEqual (CustomSet.Set.ofList [2, 3]) <| CustomSet.Set.ofList [1, 2, 3, 4] ∩ CustomSet.Set.ofList [3, 2, 5])
70+
|>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of two empty sets is an empty set" (do
71+
return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] \ CustomSet.Set.ofList [])
72+
|>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of empty set and non-empty set is an empty set" (do
73+
return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] \ CustomSet.Set.ofList [3, 2, 5])
74+
|>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of a non-empty set and an empty set is the non-empty set" (do
75+
return assertEqual (CustomSet.Set.ofList [1, 2, 3, 4]) <| CustomSet.Set.ofList [1, 2, 3, 4] \ CustomSet.Set.ofList [])
76+
|>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of two non-empty sets is a set of elements that are only in the first set" (do
77+
return assertEqual (CustomSet.Set.ofList [1, 3]) <| CustomSet.Set.ofList [3, 2, 1] \ CustomSet.Set.ofList [2, 4])
78+
|>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference removes all duplicates in the first set" (do
79+
return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [1, 1] \ CustomSet.Set.ofList [1])
80+
|>.addTest "Union returns a set of all elements in either set -> union of empty sets is an empty set" (do
81+
return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] ∪ CustomSet.Set.ofList [])
82+
|>.addTest "Union returns a set of all elements in either set -> union of an empty set and non-empty set is the non-empty set" (do
83+
return assertEqual (CustomSet.Set.ofList [2]) <| CustomSet.Set.ofList [] ∪ CustomSet.Set.ofList [2])
84+
|>.addTest "Union returns a set of all elements in either set -> union of a non-empty set and empty set is the non-empty set" (do
85+
return assertEqual (CustomSet.Set.ofList [1, 3]) <| CustomSet.Set.ofList [1, 3] ∪ CustomSet.Set.ofList [])
86+
|>.addTest "Union returns a set of all elements in either set -> union of non-empty sets contains all unique elements" (do
87+
return assertEqual (CustomSet.Set.ofList [3, 2, 1]) <| CustomSet.Set.ofList [1, 3] ∪ CustomSet.Set.ofList [2, 3])
88+
89+
def main : IO UInt32 := do
90+
runTestSuitesWithExitCode [customSetTests]

0 commit comments

Comments
 (0)