diff options
Diffstat (limited to 'Common/List.lean')
| -rw-r--r-- | Common/List.lean | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/Common/List.lean b/Common/List.lean index 704f8b2..1c8f4a6 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -10,19 +10,20 @@ theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length simp constructor assumption - | true => simp_arith[hi] + | true => simp[hi] def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α | [] => [] | a :: as => let smallerPred := λ b ↦ pred b a let largerEqualPred := not ∘ smallerPred - have : List.length (List.filter smallerPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList] - have : List.length (List.filter largerEqualPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList] let smallers := as.filter smallerPred let biggers := as.filter largerEqualPred (quicksortBy pred smallers) ++ [a] ++ (quicksortBy pred biggers) termination_by l => l.length + decreasing_by + all_goals + simp +arith only [unattach_filter, unattach_attach, length_cons, gt_iff_lt, listFilterSmallerOrEqualList] def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt @@ -86,7 +87,7 @@ protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : Li 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] + 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 [] @@ -95,8 +96,8 @@ theorem mapWithProof_nil {α : Type u} {β : Type v} {f : (e : α) → (e ∈ [] 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₁) + λh₁ ↦ List.length_pos_iff.mp $ length_mapWithProof.subst (List.length_pos_iff.mpr h₁), + λh₁ ↦ List.length_pos_iff.mp $ length_mapWithProof.substr (List.length_pos_iff.mpr h₁) ⟩ theorem map_ne_nil {α : Type u} {β : Type v} {list : List α} {f : α → β} : list ≠ [] ↔ list.map f ≠ [] := |