add custom exercise reverse-list

config.json

@@ -274,6 +274,14 @@
         "prerequisites": [],
         "difficulty": 3
       },
+      {
+        "slug": "reverse-list",
+        "name": "reverse-list",
+        "uuid": "367e9ad0-d3a1-403a-9c05-fc53a246c63b",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 3
+      },
       {
         "slug": "rotational-cipher",
         "name": "Rotational Cipher",

exercises/practice/reverse-list/.docs/instructions.md

@@ -0,0 +1,17 @@
+# Instructions
+
+Your task is to prove the equality between a custom list reversing function and the built-in `List.reverse`.
+
+Due to the nature of this exercise, instead of relying on traditional runtime tests, the proof is checked by a theorem `check`.
+You may consider the test passing if this theorem typechecks.
+
+If you work locally or in Lean's [online playground][playground], you will get instant feedback on whether any theorem succeeds or fails, and why it fails, through Lean InfoView.
+It is an invaluable tool, capable of showing all local values in use by your proof, and your current goal.
+
+[playground]: https://live.lean-lang.org/
+
+~~~~exercism/caution
+The `sorry` tactic makes any proof appear to be correct. 
+For this reason, the `check` theorem might appear to automatically typecheck before any proof is actually written.
+Once you remove `sorry` from your proof, Lean InfoView will show the correct feedback.
+~~~~

exercises/practice/reverse-list/.meta/Example.lean

@@ -0,0 +1,13 @@
+import Spec
+
+namespace ReverseList
+
+@[csimp]
+theorem custom_reverse_eq_spec_reverse : @Spec.custom_reverse = @List.reverse := by
+  funext α
+  funext xs
+  induction xs with
+  | nil         => rfl
+  | cons x xs' ir => simpa [Spec.custom_reverse, List.reverse_cons] using ir
+
+end ReverseList

exercises/practice/reverse-list/.meta/config.json

@@ -0,0 +1,21 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "ReverseList.lean"
+    ],
+    "test": [
+      "ReverseListTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ],
+    "editor": [
+      "Spec.lean"
+    ]
+  },
+  "icon": "array-loops",
+  "blurb": "Prove equality between a custom function and the built-in List.reverse function."
+}

exercises/practice/reverse-list/ReverseList.lean

@@ -0,0 +1,9 @@
+import Spec
+
+namespace ReverseList
+
+@[csimp]
+theorem custom_reverse_eq_spec_reverse: @Spec.custom_reverse = @List.reverse := by
+  sorry --remove this line and implement the proof
+
+end ReverseList

exercises/practice/reverse-list/ReverseListTest.lean

@@ -0,0 +1,10 @@
+import LeanTest
+import ReverseList
+
+open LeanTest
+
+theorem check: @Spec.custom_reverse = @List.reverse := by
+  exact ReverseList.custom_reverse_eq_spec_reverse
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode []

exercises/practice/reverse-list/Spec.lean

@@ -0,0 +1,7 @@
+namespace Spec
+
+def custom_reverse {α : Type u} : List α → List α
+  | []      => []
+  | x :: xs => custom_reverse xs ++ [x]
+
+end Spec

exercises/practice/reverse-list/lakefile.toml

@@ -0,0 +1,20 @@
+name = "reverse-list"
+version = "0.1.0"
+defaultTargets = ["ReverseListTest"]
+testDriver = "ReverseListTest"
+moreLeanArgs = [ "-DwarningAsError=true" ]
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "ReverseList"
+
+[[lean_lib]]
+name = "Spec"
+
+[[lean_exe]]
+name = "ReverseListTest"
+root = "ReverseListTest"
+

exercises/practice/reverse-list/lean-toolchain

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

exercises/practice/reverse-list/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

exercises/practice/reverse-list/vendor/LeanTest/LeanTest/Assertions.lean

@@ -0,0 +1,166 @@
+/-
+Assertion functions for unit testing.
+-/
+
+namespace LeanTest
+
+/-- Result of a test assertion -/
+inductive AssertionResult where
+  | success : AssertionResult
+  | failure (message : String) : AssertionResult
+  deriving Repr, BEq
+
+namespace AssertionResult
+
+def isSuccess : AssertionResult → Bool
+  | success => true
+  | failure _ => false
+
+def getMessage : AssertionResult → String
+  | success => "Assertion passed"
+  | failure msg => msg
+
+end AssertionResult
+
+/-- Assert that a boolean condition is true -/
+def assert (condition : Bool) (message : String := "Assertion failed") : AssertionResult :=
+  if condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that two values are equal -/
+def assertEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected == actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected: {repr expected}\nActual: {repr actual}"
+    else
+      s!"{message}\nExpected: {repr expected}\nActual: {repr actual}"
+    .failure msg
+
+/-- Assert that two values are not equal -/
+def assertNotEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected != actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected values to be different, but both were: {repr expected}"
+    else
+      s!"{message}\nExpected values to be different, but both were: {repr expected}"
+    .failure msg
+
+/-- Refute that a boolean condition is true (assert it's false) -/
+def refute (condition : Bool) (message : String := "Refute failed - condition was true") : AssertionResult :=
+  if !condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that a value is true -/
+def assertTrue (value : Bool) (message : String := "Expected true but got false") : AssertionResult :=
+  assert value message
+
+/-- Assert that a value is false -/
+def assertFalse (value : Bool) (message : String := "Expected false but got true") : AssertionResult :=
+  refute value message
+
+/-- Assert that an Option is some -/
+def assertSome [Repr α] (opt : Option α) (message : String := "Expected Some but got None") : AssertionResult :=
+  match opt with
+  | some _ => .success
+  | none => .failure message
+
+/-- Assert that an Option is none -/
+def assertNone [Repr α] (opt : Option α) (message : String := "") : AssertionResult :=
+  match opt with
+  | none => .success
+  | some val =>
+    let msg := if message.isEmpty then
+      s!"Expected None but got Some: {repr val}"
+    else
+      s!"{message}\nExpected None but got Some: {repr val}"
+    .failure msg
+
+/-- Assert that a list is empty -/
+def assertEmpty [Repr α] (list : List α) (message : String := "") : AssertionResult :=
+  match list with
+  | [] => .success
+  | _ =>
+    let msg := if message.isEmpty then
+      s!"Expected empty list but got: {repr list}"
+    else
+      s!"{message}\nExpected empty list but got: {repr list}"
+    .failure msg
+
+/-- Assert that a list contains an element -/
+def assertContains [BEq α] [Repr α] (list : List α) (element : α) (message : String := "") : AssertionResult :=
+  if list.contains element then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected list to contain {repr element}\nList: {repr list}"
+    else
+      s!"{message}\nExpected list to contain {repr element}\nList: {repr list}"
+    .failure msg
+
+/-- Assert that a value is within a range (inclusive) -/
+def assertInRange [LE α] [DecidableRel (· ≤ · : α → α → Prop)] [Repr α]
+    (value : α) (min : α) (max : α) (message : String := "") : AssertionResult :=
+  if min ≤ value ∧ value ≤ max then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected {repr value} to be in range [{repr min}, {repr max}]"
+    else
+      s!"{message}\nExpected {repr value} to be in range [{repr min}, {repr max}]"
+    .failure msg
+
+/-- Assert that an Except value is an error -/
+def assertError [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .error _ => .success
+  | .ok val =>
+    let msg := if message.isEmpty then
+      s!"Expected error but got Ok: {repr val}"
+    else
+      s!"{message}\nExpected error but got Ok: {repr val}"
+    .failure msg
+
+/-- Assert that an Except value is ok -/
+def assertOk [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .ok _ => .success
+  | .error err =>
+    let msg := if message.isEmpty then
+      s!"Expected Ok but got error: {repr err}"
+    else
+      s!"{message}\nExpected Ok but got error: {repr err}"
+    .failure msg
+
+/-- Assert that an IO action throws an error -/
+def assertThrows (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    let msg := if message.isEmpty then
+      "Expected IO action to throw an error, but it succeeded"
+    else
+      s!"{message}\nExpected IO action to throw an error, but it succeeded"
+    return .failure msg
+  catch _ =>
+    return .success
+
+/-- Assert that an IO action succeeds (doesn't throw) -/
+def assertSucceeds (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    return .success
+  catch e =>
+    let msg := if message.isEmpty then
+      s!"Expected IO action to succeed, but it threw: {e}"
+    else
+      s!"{message}\nExpected IO action to succeed, but it threw: {e}"
+    return .failure msg
+
+end LeanTest