add pascals-triangle exercise

config.json

@@ -634,6 +634,14 @@
         "prerequisites": [],
         "difficulty": 6
       },
+      {
+        "slug": "pascals-triangle",
+        "name": "Pascal's Triangle",
+        "uuid": "d37330c0-a6b9-4e24-b28d-0d4b1b2b35b0",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 6
+      },
       {
         "slug": "rail-fence-cipher",
         "name": "Rail Fence Cipher",

exercises/practice/pascals-triangle/.docs/instructions.md

@@ -0,0 +1,35 @@
+# Instructions
+
+Your task is to output the first N rows of Pascal's triangle.
+
+[Pascal's triangle][wikipedia] is a triangular array of positive integers.
+
+In Pascal's triangle, the number of values in a row is equal to its row number (which starts at one).
+Therefore, the first row has one value, the second row has two values, and so on.
+
+The first (topmost) row has a single value: `1`.
+Subsequent rows' values are computed by adding the numbers directly to the right and left of the current position in the previous row.
+
+If the previous row does _not_ have a value to the left or right of the current position (which only happens for the leftmost and rightmost positions), treat that position's value as zero (effectively "ignoring" it in the summation).
+
+## Example
+
+Let's look at the first 5 rows of Pascal's Triangle:
+
+```text
+    1
+   1 1
+  1 2 1
+ 1 3 3 1
+1 4 6 4 1
+```
+
+The topmost row has one value, which is `1`.
+
+The leftmost and rightmost values have only one preceding position to consider, which is the position to its right respectively to its left.
+With the topmost value being `1`, it follows from this that all the leftmost and rightmost values are also `1`.
+
+The other values all have two positions to consider.
+For example, the fifth row's (`1 4 6 4 1`) middle value is `6`, as the values to its left and right in the preceding row are `3` and `3`:
+
+[wikipedia]: https://en.wikipedia.org/wiki/Pascal%27s_triangle

exercises/practice/pascals-triangle/.docs/introduction.md

@@ -0,0 +1,22 @@
+# Introduction
+
+With the weather being great, you're not looking forward to spending an hour in a classroom.
+Annoyed, you enter the class room, where you notice a strangely satisfying triangle shape on the blackboard.
+Whilst waiting for your math teacher to arrive, you can't help but notice some patterns in the triangle: the outer values are all ones, each subsequent row has one more value than its previous row and the triangle is symmetrical.
+Weird!
+
+Not long after you sit down, your teacher enters the room and explains that this triangle is the famous [Pascal's triangle][wikipedia].
+
+Over the next hour, your teacher reveals some amazing things hidden in this triangle:
+
+- It can be used to compute how many ways you can pick K elements from N values.
+- It contains the Fibonacci sequence.
+- If you color odd and even numbers differently, you get a beautiful pattern called the [Sierpiński triangle][wikipedia-sierpinski-triangle].
+
+The teacher implores you and your classmates to look up other uses, and assures you that there are lots more!
+At that moment, the school bell rings.
+You realize that for the past hour, you were completely absorbed in learning about Pascal's triangle.
+You quickly grab your laptop from your bag and go outside, ready to enjoy both the sunshine _and_ the wonders of Pascal's triangle.
+
+[wikipedia]: https://en.wikipedia.org/wiki/Pascal%27s_triangle
+[wikipedia-sierpinski-triangle]: https://en.wikipedia.org/wiki/Sierpi%C5%84ski_triangle

exercises/practice/pascals-triangle/.meta/Example.lean

@@ -0,0 +1,23 @@
+namespace PascalsTriangle
+
+structure Triangle where
+  private mk ::
+  rows : IO.Ref (Array (Array Nat))
+
+def mkTriangle : IO Triangle := do
+  return {
+    rows := ← IO.mkRef #[ #[], #[1] ]
+  }
+
+private def buildRows (triangle : Triangle) (n : Nat) : IO (Array Nat) := do
+  let mut crt ← triangle.rows.get
+  while n ≥ crt.size do
+    let last := crt.back!
+    let next := (#[0] ++ last).zipWith (· + ·) (last.push 0)
+    crt := crt.push next
+  triangle.rows.set crt
+  return crt[n]!
+
+end PascalsTriangle
+
+notation triangle "(" n ")" => PascalsTriangle.buildRows triangle n

exercises/practice/pascals-triangle/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "PascalsTriangle.lean"
+    ],
+    "test": [
+      "PascalsTriangleTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Compute Pascal's triangle up to a given number of rows.",
+  "source": "Pascal's Triangle at Wolfram Math World",
+  "source_url": "https://www.wolframalpha.com/input/?i=Pascal%27s+triangle"
+}

exercises/practice/pascals-triangle/.meta/extra.json

@@ -0,0 +1,18 @@
+[
+  {
+    "description": "big row",
+    "property": "property",
+    "input": {
+      "count": 100
+    },
+    "expected": {}
+  },
+  {
+    "description": "very big row",
+    "property": "property",
+    "input": {
+      "count": 1000
+    },
+    "expected": {}
+  }
+]

exercises/practice/pascals-triangle/.meta/tests.toml

@@ -0,0 +1,34 @@
+# 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.
+
+[9920ce55-9629-46d5-85d6-4201f4a4234d]
+description = "zero rows"
+
+[70d643ce-a46d-4e93-af58-12d88dd01f21]
+description = "single row"
+
+[a6e5a2a2-fc9a-4b47-9f4f-ed9ad9fbe4bd]
+description = "two rows"
+
+[97206a99-79ba-4b04-b1c5-3c0fa1e16925]
+description = "three rows"
+
+[565a0431-c797-417c-a2c8-2935e01ce306]
+description = "four rows"
+
+[06f9ea50-9f51-4eb2-b9a9-c00975686c27]
+description = "five rows"
+
+[c3912965-ddb4-46a9-848e-3363e6b00b13]
+description = "six rows"
+
+[6cb26c66-7b57-4161-962c-81ec8c99f16b]
+description = "ten rows"

exercises/practice/pascals-triangle/PascalsTriangle.lean

@@ -0,0 +1,16 @@
+namespace PascalsTriangle
+
+/-
+  Define here a type `Triangle`.
+  Instances of this type are generated wrapped in a suitable monad, through a `mkTriangle` function.
+
+  There must be syntax defined for a `triangle(n)`, where `triangle` is an instance of `Triangle` and `n` is a `Nat`.
+  This syntax should return the `n-th` row of a Pascal's Triangle as an `Array Nat`, wrapped in a suitable monad.
+
+  Try to make your implementation as efficient as possible.
+  There are tests for larger rows that may time out.
+
+  Refer to the test file for more information.
+-/
+
+end PascalsTriangle

exercises/practice/pascals-triangle/PascalsTriangleTest.lean

@@ -0,0 +1,97 @@
+import LeanTest
+import PascalsTriangle
+
+open LeanTest
+
+instance : HAppend AssertionResult AssertionResult AssertionResult where
+    hAppend
+        | .success, .success => .success
+        | .failure msg, _    => .failure msg
+        | _, .failure msg    => .failure msg
+
+def pascalsTriangleTests : TestSuite :=
+  (TestSuite.empty "PascalsTriangle")
+  |>.addTest "zero rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      return result)
+  |>.addTest "single row" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      return result)
+  |>.addTest "two rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      return result)
+  |>.addTest "three rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      return result)
+  |>.addTest "four rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      result := result ++ assertEqual #[1, 3, 3, 1] (← triangle(4))
+      return result)
+  |>.addTest "five rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      result := result ++ assertEqual #[1, 3, 3, 1] (← triangle(4))
+      result := result ++ assertEqual #[1, 4, 6, 4, 1] (← triangle(5))
+      return result)
+  |>.addTest "six rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      result := result ++ assertEqual #[1, 3, 3, 1] (← triangle(4))
+      result := result ++ assertEqual #[1, 4, 6, 4, 1] (← triangle(5))
+      result := result ++ assertEqual #[1, 5, 10, 10, 5, 1] (← triangle(6))
+      return result)
+  |>.addTest "ten rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      result := result ++ assertEqual #[1, 3, 3, 1] (← triangle(4))
+      result := result ++ assertEqual #[1, 4, 6, 4, 1] (← triangle(5))
+      result := result ++ assertEqual #[1, 5, 10, 10, 5, 1] (← triangle(6))
+      result := result ++ assertEqual #[1, 6, 15, 20, 15, 6, 1] (← triangle(7))
+      result := result ++ assertEqual #[1, 7, 21, 35, 35, 21, 7, 1] (← triangle(8))
+      result := result ++ assertEqual #[1, 8, 28, 56, 70, 56, 28, 8, 1] (← triangle(9))
+      result := result ++ assertEqual #[1, 9, 36, 84, 126, 126, 84, 36, 9, 1] (← triangle(10))
+      return result)
+  |>.addTest "big row" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let row ← triangle(100)
+      let prev ← triangle(99)
+      let mut result := (assertEqual 100 row.size) ++ (assertEqual 99 prev.size)
+      result := result ++ (assertEqual 1 row[0]!) ++ (assertEqual 1 row[row.size - 1]!)
+      for i in [1:row.size - 1] do
+        result := result ++ assertEqual row[i]! (prev[i - 1]! + prev[i]!)
+      return result)
+  |>.addTest "very big row" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let row ← triangle(1000)
+      let prev ← triangle(999)
+      let mut result := (assertEqual 1000 row.size) ++ (assertEqual 999 prev.size)
+      result := result ++ (assertEqual 1 row[0]!) ++ (assertEqual 1 row[row.size - 1]!)
+      for i in [1:row.size - 1] do
+        result := result ++ assertEqual row[i]! (prev[i - 1]! + prev[i]!)
+      return result)
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [pascalsTriangleTests]

exercises/practice/pascals-triangle/lakefile.toml

@@ -0,0 +1,15 @@
+name = "pascals-triangle"
+version = "0.1.0"
+defaultTargets = ["PascalsTriangleTest"]
+testDriver = "PascalsTriangleTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "PascalsTriangle"
+
+[[lean_exe]]
+name = "PascalsTriangleTest"
+root = "PascalsTriangleTest"

exercises/practice/pascals-triangle/lean-toolchain

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

exercises/practice/pascals-triangle/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