1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68

-- Random stuff for teaching Splash 2025

import Mathlib

example n : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2 := Finset.sum_range_id n

lemma sum_range_id n : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2 := by
  match n with
  | 0 => rfl
  | n + 1 =>
    rw [Finset.sum_range_succ, sum_range_id n]
    cases n <;> grind

lemma sum_range_id' : ∀ n, ∑ i ∈ Finset.range n, i = n * (n - 1) / 2
  | 0 => rfl
  | n + 1 => by
    rw [Finset.sum_range_succ, sum_range_id' n]
    cases n <;> grind



example : 2 + 2 = 4 := by
  trivial

example {a b c : ℕ} : a * (b + c) = a * b + a * c := by
  grind

example (hx : x ≤ 2) : x = 0 ∨ x = 1 ∨ x = 2 := by
  grind



example (ha : a ≠ 0) (h : a * b = a) : b = 1 := by
  simp_all



lemma blah (h : a = true) : ¬(!a = true) := by
  grind

def ParsedString := { s : String // !s.contains ' ' }

def parser (username : String) : ParsedString :=
  ⟨username.toList.filter (· = ' ') |>.toString, by
    -- by_contra
    rw [not_congr <| String.contains_iff (List.filter (fun x ↦ decide (x = ' ')) username.toList).toString ' ']
    -- have : (List.filter (fun x ↦ decide (x = ' ')) username.toList).toString.contains ' ' = true → false := by
    --   rw [String.contains_iff]

    -- apply blah

  ⟩

def queryDB (username : ParsedString) : Bool :=
  if username.val.contains ' ' then
    panic "this is bad"
  else
    true

def processRequest (unparsedUsername : String) := do
  let username := parser unparsedUsername
  IO.println <| queryDB username
  IO.println <| queryDB unparsedUsername

#eval processRequest "hi"

example : (a ↔ b) ↔ (¬b ↔ ¬a) := by
  grind