1 files changed, 42 insertions, 0 deletions
diff --git a/Common/List.lean b/Common/List.lean
index 1c029e7..704f8b2 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -70,3 +70,45 @@ def drop_while_length_le (list : List α) (f : α → Bool) : (list.dropWhile f)
     case h_1 a as _  _ =>
       have := drop_while_length_le as f
       exact Nat.le_trans this (Nat.le_succ as.length)
+
+def mapWithProof {α : Type u} {β : Type v} (list : List α) (f : (e : α) → (e ∈ list) → β) : List β :=
+  worker list f []
+where
+  worker : (list : List α) → ((e : α) → (e ∈ list) → β) → List β → List β
+  | [], _, bs => bs.reverse
+  | a :: as, f, bs =>
+    let g : (e : α) → (e ∈ as) → β := λ e h ↦ f e (List.mem_cons_of_mem a h)
+    worker as g (f a (List.mem_cons_self _ _) :: bs)
+
+protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : List α) (f : (e : α) → (e ∈ list) → β) (acc : List β) : list.length + acc.length = (List.mapWithProof.worker list f acc).length := by
+  induction list generalizing acc
+  case nil => unfold mapWithProof.worker; simp only [length_nil, Nat.zero_add, length_reverse]
+  case cons l ls hi =>
+    unfold mapWithProof.worker
+    have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self _ _) :: acc)
+    simp_arith[←hi]
+
+theorem length_mapWithProof {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list.length = (list.mapWithProof f).length :=
+  List.length_mapWithProof_Aux list f []
+
+theorem mapWithProof_nil {α : Type u} {β : Type v} {f : (e : α) → (e ∈ []) → β} : [].mapWithProof f = [] := rfl
+
+theorem mapWithProof_neNilIffNeNil {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list ≠ [] ↔ (list.mapWithProof f) ≠ [] :=
+  ⟨
+    λh₁ ↦ List.length_pos.mp $ length_mapWithProof.subst (List.length_pos.mpr h₁),
+    λh₁ ↦ List.length_pos.mp $ length_mapWithProof.substr (List.length_pos.mpr h₁)
+  ⟩
+
+theorem map_ne_nil {α : Type u} {β : Type v} {list : List α} {f : α → β} : list ≠ [] ↔ list.map f ≠ [] :=
+  ⟨
+    λh₁ ↦ λh₂ ↦ absurd (List.map_eq_nil_iff.mp h₂) h₁,
+    λh₁ ↦ λh₂ ↦ absurd (List.map_eq_nil_iff.mpr h₂) h₁,
+  ⟩
+
+def min [Min α] (l : List α) (_h : l ≠ []) : α :=
+  match l with
+  | a :: as => as.foldl Min.min a
+
+def max [Max α] (l : List α) (_h : l ≠ []) : α :=
+  match l with
+  | a :: as => as.foldl Max.max a