From b1c7ab96169f80f62c8f5025cf2ebd74e9128f71 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 24 Sep 2024 20:04:26 +0200
Subject: Day 12 Part 1.

God, I fell into the premature optimization trap here...
But I'm glad I did, that should make part 2 way easier.
---
 Common/List.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'Common/List.lean')

diff --git a/Common/List.lean b/Common/List.lean
index b34f1e2..1c029e7 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -54,3 +54,19 @@ def not_empty_iff_size_gt_zero {list : List α} : list.isEmpty = false ↔ list.
   match list with
   | [] => ⟨nofun, nofun⟩
   | l :: ls => ⟨λ_ ↦ (List.length_cons l ls).substr (Nat.succ_pos ls.length), λ_ => rfl⟩
+
+def ne_nil_of_not_empty {list : List α} : list.isEmpty = false ↔ list ≠ [] :=
+  match list with
+  | [] => ⟨nofun, nofun⟩
+  | _ :: _ => ⟨nofun, λ_ ↦ List.isEmpty_cons⟩
+
+def drop_while_length_le (list : List α) (f : α → Bool) : (list.dropWhile f).length ≤ list.length := by
+  unfold dropWhile
+  split
+  case h_1 => exact Nat.le_refl _
+  case h_2 =>
+    split
+    case h_2 => exact Nat.le_refl _
+    case h_1 a as _  _ =>
+      have := drop_while_length_le as f
+      exact Nat.le_trans this (Nat.le_succ as.length)
-- 
cgit v1.2.3