add approaches and article to difference-of-squares

exercises/practice/difference-of-squares/.approaches/config.json

@@ -0,0 +1,35 @@
+{
+  "introduction": {
+    "authors": ["oxe-i"],
+    "contributors": []
+  },
+  "approaches": [
+    {
+      "uuid": "854dac53-adfd-46ad-8c64-46e401a46a37",
+      "slug": "recurse-numbers",
+      "title": "Recurse Over Numbers",
+      "blurb": "recurse over all numbers to sum them up.",
+      "authors": [
+        "oxe-i"
+      ]
+    },
+    {
+      "uuid": "3e4413e6-89cb-4e1e-8e83-89e84754dd0f",
+      "slug": "mathematical-formula",
+      "title": "Mathematical Formula",
+      "blurb": "calculate sums using known mathematical formulas.",
+      "authors": [
+        "oxe-i"
+      ]
+    },
+    {
+      "uuid": "0e48332a-1b9b-4322-b941-933d1c718d67",
+      "slug": "folding-over-range",
+      "title": "Folding Over Range",
+      "blurb": "use a fold to sum all numbers in a range.",
+      "authors": [
+        "oxe-i"
+      ]
+    }
+  ]
+}

exercises/practice/difference-of-squares/.approaches/folding-over-range/content.md

@@ -0,0 +1,63 @@
+# Folding Over Range
+
+In functional programming languages, a [fold][fold] is a common way to iterate over a collection while accumulating a result.
+
+A fold processes the elements of a collection one by one, updating an accumulator at each step. 
+To perform a fold, three things are needed:
+
+1. A collection of elements, often stored in a `List` or an `Array`.
+2. An initial value for the accumulator.
+3. A function that combines the current element with the accumulator to produce a new accumulator.
+
+For example, if we fold a collection of numbers using `0` as the initial value and addition as the combining function, the result will be the sum of all elements in the collection.
+
+Lean provides helper functions for `List` and `Array` that generate collections of sequential numbers, which can then be processed with a fold:
+
+```lean
+def squareOfSum (number : Nat) : Nat :=
+    let sum := (List.range' 1 number).foldl (fun acc x => acc + x) 0
+    sum ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    (List.range' 1 number).foldl (init := 0) fun acc x => acc + x^2
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+Both [List.range'][list-range'] and [Array.range'][array-range'] create collections of consecutive natural numbers.
+They take:
+
+- a starting value (the first argument, `1` in the example), and
+- a count (the second argument, `number`).
+
+The result is a collection containing `number` values starting from the initial value.
+
+An optional third argument specifies the _step size_, which determines how much each value increases relative to the previous one. 
+If omitted, the default step is `1`, producing consecutive numbers.
+
+Lean also defines a [fold directly for `Nat`][nat-fold]. 
+Instead of folding over an explicit collection, this function iterates from `0` up to (but not including) a given number.
+
+The folding function receives three arguments:
+
+1. the current index,
+2. a proof that the index is less than the bound, and
+3. the current accumulator.
+
+```lean
+def squareOfSum (number : Nat) : Nat :=
+    let sum := number.fold (init := 0) fun i _ acc => (i + 1) + acc
+    sum ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    number.fold (fun i _ acc => acc + (i + 1) ^ 2) 0
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+This approach avoids explicitly creating a collection and instead performs the iteration directly over the natural numbers, which can be more efficient.
+
+[fold]: https://en.wikipedia.org/wiki/Fold_(higher-order_function)
+[list-range']: https://lean-lang.org/doc/reference/latest/Basic-Types/Linked-Lists/#List___range___
+[array-range']: https://lean-lang.org/doc/reference/latest/Basic-Types/Arrays/#Array___range___
+[nat-fold]: https://lean-lang.org/doc/reference/latest/Basic-Types/Natural-Numbers/#Nat___fold

exercises/practice/difference-of-squares/.approaches/folding-over-range/snippet.txt

@@ -0,0 +1,6 @@
+def squareOfSum (number : Nat) : Nat :=
+    let sum := number.fold (init := 0) fun i _ acc => (i + 1) + acc
+    sum ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    number.fold (fun i _ acc => acc + (i + 1) ^ 2) 0

exercises/practice/difference-of-squares/.approaches/introduction.md

@@ -0,0 +1,75 @@
+# Introduction
+
+There are multiple ways to solve `difference-of-squares`.
+Some of them include:
+
+* Recursing over numbers.
+* Using known mathematical formulas.
+* Folding over a range of numbers.
+
+## Approach: Recursing over numbers
+
+Recurse over decreasing numbers until a base case is reached, accumulating the result:
+
+```lean
+def sumN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 
+    then acc 
+    else sumN (n - 1) (acc + n)
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumN number 0) ^ 2
+
+def sumSquareN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 
+    then acc 
+    else sumSquareN (n - 1) (acc + (n ^ 2))
+
+def sumOfSquares (number : Nat) : Nat :=
+    sumSquareN number 0
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+For more details, see the [recurse-numbers][recurse-numbers] approach.
+
+## Approach: Using mathematical formulas
+
+Compute the results directly using mathematical formulas:
+
+```lean
+def sumFirstNPositive (n : Nat) : Nat :=
+    n * (n + 1) / 2
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    (number * (number + 1) * (2 * number + 1)) / 6
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+For more details, see the [mathematical-formula][mathematical-formula] approach.
+
+## Approach: Folding over range
+
+Use a `fold` to iterate over a range of values and accumulate the result:
+
+```lean
+def squareOfSum (number : Nat) : Nat :=
+    let sum := number.fold (init := 0) fun i _ acc => (i + 1) + acc
+    sum ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    number.fold (fun i _ acc => acc + (i + 1) ^ 2) 0
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+For more details, see the [folding-over-range][folding-over-range] approach.
+
+[recurse-numbers]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/recurse-numbers
+[mathematical-formula]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/mathematical-formula
+[folding-over-range]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/folding-over-range

exercises/practice/difference-of-squares/.approaches/mathematical-formula/content.md

@@ -0,0 +1,27 @@
+# Mathematical Formula
+
+A possible way to solve this exercise is to use [known mathematical formulas][formulas]:
+
+* The sum of positive integers up to `n`, inclusive, is `n * (n + 1) / 2`.
+  Squaring that sum gives `squareOfSum`.
+* The sum of the squares of positive integers up to `n`, inclusive, is `n * (n + 1) * (2 * n + 1) / 6`.
+
+```lean
+def sumFirstNPositive (n : Nat) : Nat :=
+    n * (n + 1) / 2
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    (number * (number + 1) * (2 * number + 1)) / 6
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+This is probably the most efficient approach, since the problem reduces to a few constant multiplications and divisions, whereas the other approaches are `O(n)`.
+On the other hand, the solution becomes more opaque because these formulas are not obvious from the structure of the problem. 
+They require previous knowledge or further research.
+
+[formulas]: https://en.wikipedia.org/wiki/Triangular_number

exercises/practice/difference-of-squares/.approaches/mathematical-formula/snippet.txt

@@ -0,0 +1,5 @@
+def squareOfSum (number : Nat) : Nat :=
+    (number * (number + 1) / 2) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    (number * (number + 1) * (2 * number + 1)) / 6

exercises/practice/difference-of-squares/.approaches/recurse-numbers/content.md

@@ -0,0 +1,85 @@
+# Recurse All
+
+In functional languages like Lean, recursion often fills the same role as loops in other languages.
+It is the primary tool used to iterate over a group of elements or a range of values.
+
+This exercise can be solved using straightforward recursion:
+
+```lean
+def sumFirstNPositive (n : Nat) : Nat :=
+    match n with
+    | 0     => 0
+    | x + 1 => (x + 1) + sumFirstNPositive x 
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    match number with
+    | 0     => 0
+    | x + 1 => (x + 1) * (x + 1) + sumOfSquares x
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+In cases like this, where a function is defined as a simple pattern match on a value, there is an equivalent and more concise notation:
+
+```lean
+def sumFirstNPositive : Nat -> Nat
+    | 0     => 0
+    | x + 1 => (x + 1) + sumFirstNPositive x 
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares : Nat -> Nat
+    | 0     => 0
+    | x + 1 => (x + 1) * (x + 1) + sumOfSquares x
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+It is also possible to use `if...then...else` to achieve the same effect:
+
+```lean
+def sumN (n : Nat) :=
+    if n = 0 then 0 else n + sumN (n - 1)
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumN number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    if number = 0 then 0 else number ^ 2 + sumOfSquares (number - 1)
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+Both functions can also be made [tail-recursive][tail-call] by adding an extra accumulating parameter:
+
+```lean
+def sumN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 then acc else sumN (n - 1) (acc + n)
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumN number 0) ^ 2
+
+def sumSquareN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 then acc else sumSquareN (n - 1) (acc + (n ^ 2))
+
+def sumOfSquares (number : Nat) : Nat :=
+    sumSquareN number 0
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+A tail-recursive function may be optimized by the compiler so that it does not require additional stack space, making it as efficient as a loop.
+
+This approach has the advantage of being clear and self-documenting.
+The problem involves summing a range of numbers, and that is exactly what the code expresses.
+
+However, it is also inefficient, since it requires as many recursive calls as `number`, the argument to the functions. 
+Even a tail-recursive variant still requires iterating over all values from `0` up to `number`.
+
+[tail-call]: https://en.wikipedia.org/wiki/Tail_call

exercises/practice/difference-of-squares/.approaches/recurse-numbers/snippet.txt

@@ -0,0 +1,8 @@
+def sumN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 then acc else sumN (n - 1) (acc + n)
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumN number 0) ^ 2
+
+def sumOfSquares (number : Nat) (acc := 0) : Nat :=
+    if n = 0 then acc else sumSquareN (n - 1) (acc + (n ^ 2))

exercises/practice/difference-of-squares/.articles/config.json

@@ -0,0 +1,13 @@
+{
+  "articles": [
+    {
+      "uuid": "14152e49-e077-4a8e-a1c2-5812ebb5bbdd",
+      "slug": "formula-is-equivalent-to-recursion",
+      "title": "Proving that the mathematical formula and the recursive approaches are equivalent",
+      "blurb": "proving that the mathematical formula and the recursive approaches are equivalent.",
+      "authors": [
+        "oxe-i"
+      ]
+    }
+  ]
+}