add strain exercise

config.json

@@ -314,6 +314,14 @@
         "prerequisites": [],
         "difficulty": 3
       },
+      {
+        "slug": "strain",
+        "name": "Strain",
+        "uuid": "b22117f8-5c1e-4988-8ffa-a6ddb0a9026a",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 3
+      },
       {
         "slug": "sublist",
         "name": "Sublist",

exercises/practice/strain/.docs/instructions.append.md

@@ -0,0 +1,11 @@
+# Instructions append
+
+## Typeclasses
+
+This exercise requires that a type class `Partition` be defined with two methods: `keep` and `discard`.
+
+[This chapter][introduction] provides a good introduction to the topic. 
+You might also want to check a [language reference][type-class-reference].
+
+[introduction]: https://lean-lang.org/functional_programming_in_lean/Overloading-and-Type-Classes/#type-classes
+[type-class-reference]: https://lean-lang.org/doc/reference/latest/Type-Classes/#type-classes

exercises/practice/strain/.docs/instructions.md

@@ -0,0 +1,29 @@
+# Instructions
+
+Implement the `keep` and `discard` operation on collections.
+Given a collection and a predicate on the collection's elements, `keep` returns a new collection containing those elements where the predicate is true, while `discard` returns a new collection containing those elements where the predicate is false.
+
+For example, given the collection of numbers:
+
+- 1, 2, 3, 4, 5
+
+And the predicate:
+
+- is the number even?
+
+Then your keep operation should produce:
+
+- 2, 4
+
+While your discard operation should produce:
+
+- 1, 3, 5
+
+Note that the union of keep and discard is all the elements.
+
+The functions may be called `keep` and `discard`, or they may need different names in order to not clash with existing functions or concepts in your language.
+
+## Restrictions
+
+Keep your hands off that filter/reject/whatchamacallit functionality provided by your standard library!
+Solve this one yourself using other basic tools instead.

exercises/practice/strain/.meta/Example.lean

@@ -0,0 +1,11 @@
+namespace Strain
+
+class Partition (α : Type u) (β : Type v) where
+  keep : (α → Bool) → β → β
+  discard : (α → Bool) → β → β
+
+instance {α : Type u} : Partition α (List α) where
+  keep fn xs := xs.foldr (init := []) fun x acc => if fn x then x :: acc else acc
+  discard fn xs := xs.foldr (init := []) fun x acc => if fn x then acc else x :: acc
+
+end Strain

exercises/practice/strain/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "Strain.lean"
+    ],
+    "test": [
+      "StrainTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Implement the `keep` and `discard` operation on collections.",
+  "source": "Conversation with James Edward Gray II",
+  "source_url": "http://graysoftinc.com/"
+}

exercises/practice/strain/.meta/tests.toml

@@ -0,0 +1,52 @@
+# This is an auto-generated file.
+#
+# Regenerating this file via `configlet sync` will:
+# - Recreate every `description` key/value pair
+# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
+# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
+# - Preserve any other key/value pair
+#
+# As user-added comments (using the # character) will be removed when this file
+# is regenerated, comments can be added via a `comment` key.
+
+[26af8c32-ba6a-4eb3-aa0a-ebd8f136e003]
+description = "keep on empty list returns empty list"
+
+[f535cb4d-e99b-472a-bd52-9fa0ffccf454]
+description = "keeps everything"
+
+[950b8e8e-f628-42a8-85e2-9b30f09cde38]
+description = "keeps nothing"
+
+[92694259-6e76-470c-af87-156bdf75018a]
+description = "keeps first and last"
+
+[938f7867-bfc7-449e-a21b-7b00cbb56994]
+description = "keeps neither first nor last"
+
+[8908e351-4437-4d2b-a0f7-770811e48816]
+description = "keeps strings"
+
+[2728036b-102a-4f1e-a3ef-eac6160d876a]
+description = "keeps lists"
+
+[ef16beb9-8d84-451a-996a-14e80607fce6]
+description = "discard on empty list returns empty list"
+
+[2f42f9bc-8e06-4afe-a222-051b5d8cd12a]
+description = "discards everything"
+
+[ca990fdd-08c2-4f95-aa50-e0f5e1d6802b]
+description = "discards nothing"
+
+[71595dae-d283-48ca-a52b-45fa96819d2f]
+description = "discards first and last"
+
+[ae141f79-f86d-4567-b407-919eaca0f3dd]
+description = "discards neither first nor last"
+
+[daf25b36-a59f-4f29-bcfe-302eb4e43609]
+description = "discards strings"
+
+[a38d03f9-95ad-4459-80d1-48e937e4acaf]
+description = "discards lists"

exercises/practice/strain/Strain.lean

@@ -0,0 +1,14 @@
+namespace Strain
+
+/-
+  Define here a typeclass `Partition` with the methods `keep` and `discard`, following the semantics laid out in the instructions.
+
+  You must also define an instance of that typeclass for `List α`, where `α` is a type variable.
+  This instance must be defined in the current namespace.
+
+  Try to avoid using `List.filter` or similar library functions in your implementation.
+
+  Refer to the test file for more information.
+-/
+
+end Strain

exercises/practice/strain/StrainTest.lean

@@ -0,0 +1,157 @@
+import LeanTest
+import Strain
+
+open LeanTest
+
+structure StrainWrapper α where
+  list : List α
+  deriving BEq, Repr
+
+instance {α} : Strain.Partition α (StrainWrapper α) where
+  keep fn wrapper := ⟨Strain.Partition.keep fn wrapper.list⟩
+  discard fn wrapper := ⟨Strain.Partition.discard fn wrapper.list⟩
+
+def strainTests : TestSuite :=
+  (TestSuite.empty "Strain")
+  |>.addTest "keep on empty list returns empty list" (do
+      let input : StrainWrapper Nat := ⟨[]⟩
+      return assertEqual ⟨[]⟩ (Strain.Partition.keep (fun (_ : Nat) => true) input))
+  |>.addTest "keeps everything" (do
+      let input : StrainWrapper Nat := ⟨[
+        1,
+        3,
+        5
+      ]⟩
+      return assertEqual ⟨[
+        1,
+        3,
+        5
+      ]⟩ (Strain.Partition.keep (fun (_ : Nat) => true) input))
+  |>.addTest "keeps nothing" (do
+      let input : StrainWrapper Nat := ⟨[
+        1,
+        3,
+        5
+      ]⟩
+      return assertEqual ⟨[]⟩ (Strain.Partition.keep (fun (_ : Nat) => false) input))
+  |>.addTest "keeps first and last" (do
+      let input : StrainWrapper Nat := ⟨[
+        1,
+        2,
+        3
+      ]⟩
+      return assertEqual ⟨[
+        1,
+        3
+      ]⟩ (Strain.Partition.keep (fun (x : Nat) => x % 2 == 1) input))
+  |>.addTest "keeps neither first nor last" (do
+      let input : StrainWrapper Nat := ⟨[
+        1,
+        2,
+        3
+      ]⟩
+      return assertEqual ⟨[
+        2
+      ]⟩ (Strain.Partition.keep (fun (x : Nat) => x % 2 == 0) input))
+  |>.addTest "keeps strings" (do
+      let input : StrainWrapper String := ⟨[
+        "apple",
+        "zebra",
+        "banana",
+        "zombies",
+        "cherimoya",
+        "zealot"
+      ]⟩
+      return assertEqual ⟨[
+        "zebra",
+        "zombies",
+        "zealot"
+      ]⟩ (Strain.Partition.keep (fun (x : String) => x.startsWith 'z') input))
+  |>.addTest "keeps lists" (do
+      let input : StrainWrapper (List Nat) := ⟨[
+        [1, 2, 3],
+        [5, 5, 5],
+        [5, 1, 2],
+        [2, 1, 2],
+        [1, 5, 2],
+        [2, 2, 1],
+        [1, 2, 5]
+      ]⟩
+      return assertEqual ⟨[
+        [5, 5, 5],
+        [5, 1, 2],
+        [1, 5, 2],
+        [1, 2, 5]
+      ]⟩ (Strain.Partition.keep (fun (x : (List Nat)) => x.contains 5) input))
+  |>.addTest "discard on empty list returns empty list" (do
+      let input : StrainWrapper Nat := ⟨[]⟩
+      return assertEqual ⟨[]⟩ (Strain.Partition.discard (fun (_ : Nat) => true) input))
+  |>.addTest "discards everything" (do
+      let input : StrainWrapper Nat := ⟨[
+        1,
+        3,
+        5
+      ]⟩
+      return assertEqual ⟨[]⟩ (Strain.Partition.discard (fun (_ : Nat) => true) input))
+  |>.addTest "discards nothing" (do
+      let input : StrainWrapper Nat := ⟨[
+        1,
+        3,
+        5
+      ]⟩
+      return assertEqual ⟨[
+        1,
+        3,
+        5
+      ]⟩ (Strain.Partition.discard (fun (_ : Nat) => false) input))
+  |>.addTest "discards first and last" (do
+      let input : StrainWrapper Nat := ⟨[
+        1,
+        2,
+        3
+      ]⟩
+      return assertEqual ⟨[
+        2
+      ]⟩ (Strain.Partition.discard (fun (x : Nat) => x % 2 == 1) input))
+  |>.addTest "discards neither first nor last" (do
+      let input : StrainWrapper Nat := ⟨[
+        1,
+        2,
+        3
+      ]⟩
+      return assertEqual ⟨[
+        1,
+        3
+      ]⟩ (Strain.Partition.discard (fun (x : Nat) => x % 2 == 0) input))
+  |>.addTest "discards strings" (do
+      let input : StrainWrapper String := ⟨[
+        "apple",
+        "zebra",
+        "banana",
+        "zombies",
+        "cherimoya",
+        "zealot"
+      ]⟩
+      return assertEqual ⟨[
+        "apple",
+        "banana",
+        "cherimoya"
+      ]⟩ (Strain.Partition.discard (fun (x : String) => x.startsWith 'z') input))
+  |>.addTest "discards lists" (do
+      let input : StrainWrapper (List Nat) := ⟨[
+        [1, 2, 3],
+        [5, 5, 5],
+        [5, 1, 2],
+        [2, 1, 2],
+        [1, 5, 2],
+        [2, 2, 1],
+        [1, 2, 5]
+      ]⟩
+      return assertEqual ⟨[
+        [1, 2, 3],
+        [2, 1, 2],
+        [2, 2, 1]
+      ]⟩ (Strain.Partition.discard (fun (x : (List Nat)) => x.contains 5) input))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [strainTests]

exercises/practice/strain/lakefile.toml

@@ -0,0 +1,15 @@
+name = "strain"
+version = "0.1.0"
+defaultTargets = ["StrainTest"]
+testDriver = "StrainTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "Strain"
+
+[[lean_exe]]
+name = "StrainTest"
+root = "StrainTest"

exercises/practice/strain/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0

exercises/practice/strain/vendor/LeanTest/LeanTest.lean

@@ -0,0 +1,4 @@
+-- This module serves as the root of the `LeanTest` library.
+-- Import modules here that should be built as part of the library.
+import LeanTest.Assertions
+import LeanTest.Test