diff options
Diffstat (limited to 'Common/List.lean')
| -rw-r--r-- | Common/List.lean | 16 |
1 files changed, 16 insertions, 0 deletions
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) |