Update 4 Chapter9.lean

Author: Darlan369

Fad/Chapter9.lean

@@ -4,41 +4,27 @@ import Fad.«Chapter1-Ex»
 
 namespace Chapter9
 
-def picks {a : Type} : List a → List (a × List a)
+def picks {a : Type} : List a → List (a × List a) -- 1 ou 7
 | []      => []
 | x :: xs =>
   (x, xs) :: ((picks xs).map (λ p => (p.1, x :: p.2)))
 
-def wrap {α : Type} (a : α) : List α := [a]
+def wrap {α : Type} (a : α) : List α := [a] -- 1-Ex
 
-partial def until' (p: a → Bool) (f: a → a) (x : a) : a :=
+partial def until' (p: a → Bool) (f: a → a) (x : a) : a := -- 1
   if p x then x
   else until' p f (f x)
 
-def foldr1 {a : Type} [Inhabited a] (f : a → a → a) : List a → a
+def foldr1 {a : Type} [Inhabited a] (f : a → a → a) : List a → a -- 7
   | []    => default
   | x::xs => xs.foldr f x
 
-def minWith {a b : Type} [LE b] [Inhabited a]
+def minWith {a b : Type} [LE b] [Inhabited a] -- 7
   [DecidableRel (α := b) (· ≤ ·)]
   (f : a → b) (as : List a) : a :=
   let smaller f x y := cond (f x ≤ f y) x y
   foldr1 (smaller f) as
 
-
-#eval foldr1  (fun a b => a + b ) [1,2,3,4,5,6]
-
-def qsort₂ [Ord a] (f : a → a → Ordering) : List a → List a
-  | []        => []
-  | (x :: xs) =>
-    let p := xs.partition (λ z => f z x = Ordering.lt)
-    (qsort₂ f p.1) ++ [x] ++ (qsort₂ f p.2)
- termination_by xs => xs.length
- decreasing_by
-  all_goals simp
-   [List.partition_eq_filter_filter,
-    List.length_filter_le, Nat.lt_add_one_of_le]
-
 /- 9.1 Graphs and spanning trees -/
 
 abbrev Vertex := Nat