Splash 2025

Changes

1 changed files (+68/-0)

• Splash.lean (new)
  • @@ -0,0 +1,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