aula 2025-05-21

Author: arademaker

Fad/Chapter4.lean

@@ -1,4 +1,3 @@
-
 import Fad.Chapter1
 
 namespace Chapter4
@@ -227,63 +226,64 @@ def mkTree [LT α] [DecidableRel (α := α) (· < ·)]
          List.length_filter_le,
          Nat.lt_add_one_of_le]
 
-
 end BST1
 
 
 namespace BST2
 
-variable {α : Type}
+variable {a : Type} [LT a] [DecidableRel (α := a) (· < ·)]
 
-inductive Tree (α : Type) : Type
-| null : Tree α
-| node : Nat → (Tree α) → α → (Tree α) → Tree α
-deriving Nonempty
+inductive Tree (a : Type) : Type
+| null : Tree a
+| node : Nat → (Tree a) → a → (Tree a) → Tree a
+deriving Nonempty, Inhabited
 
 open Std.Format in
 
-def Tree.toFormat [ToString α] : (t : Tree α) → Std.Format
+def Tree.toFormat [ToString a] : (t : Tree a) → Std.Format
 | .null => Std.Format.text "."
 | .node _ t₁ x t₂ =>
   bracket "(" (f!"{x}" ++
    line ++ nest 2 t₁.toFormat ++ line ++ nest 2 t₂.toFormat) ")"
 
-instance [ToString α] : Repr (Tree α) where
+instance [ToString a] : Repr (Tree a) where
  reprPrec e _ := e.toFormat
 
-def Tree.height : Tree α → Nat
+def Tree.height : Tree a → Nat
  | .null => 0
  | .node x _ _ _ => x
 
-def Tree.flatten : Tree α → List α
+def Tree.flatten : Tree a → List a
 | null => []
 | node _ l x r => l.flatten ++ [x] ++ r.flatten
 
-def node (l : Tree α) (x : α) (r : Tree α): Tree α :=
+def node (l : Tree a) (x : a) (r : Tree a): Tree a :=
   Tree.node h l x r
  where h := 1 + (max l.height r.height)
 
-def bias : Tree α → Int
+def bias : Tree a → Int
  | .null => 0
  | .node _ l _ r => l.height - r.height
 
-def rotr : Tree α → Tree α
+def rotr : Tree a → Tree a
 | .null => .null
 | .node _ (.node _ ll y rl) x r => node ll y (node rl x r)
 | .node _ .null _ _ => .null
 
-def rotl : Tree α → Tree α
+def rotl : Tree a → Tree a
 | .null => .null
 | .node _ ll y (.node _ lrl z rrl) => node (node ll y lrl) z rrl
 | .node _ _ _ .null => .null
 
-def balance (t1 : Tree α)  (x : α)  (t2 : Tree α) : Tree α :=
+def balance (t1 : Tree a)  (x : a)  (t2 : Tree a) : Tree a :=
  if Int.natAbs (h1 - h2) ≤ 1 then
    node t1 x t2
- else if h1 == h2 + 2 then
+ else if h1 = h2 + 2 then
    rotateR t1 x t2
- else
+ else if h2 = h1 + 2 then
    rotateL t1 x t2
+ else
+   panic! "balance: impossible case"
  where
   h1 := t1.height
   h2 := t2.height
@@ -297,33 +297,45 @@ def balance (t1 : Tree α)  (x : α)  (t2 : Tree α) : Tree α :=
    else rotl (node t1 x (rotr t2))
 
 
-def insert {α : Type} [LT α] [DecidableRel (α := α) (· < ·)]
- : (x : α) -> Tree α -> Tree α
+def insert : (x : a) -> Tree a -> Tree a
  | x, .null => node .null x .null
  | x, .node h l y r =>
    if x < y then balance (insert x l) y r else
    if x > y then balance l y (insert x r) else .node h l y r
 
 
-def mkTree [LT α] [DecidableRel (α := α) (· < ·)] : (xs : List α) → Tree α :=
- Chapter1.foldr insert (.null : Tree α)
+def mkTree : (xs : List a) → Tree a :=
+ List.foldr insert (.null : Tree a)
 
+-- #eval balance (mkTree [1,2,3,4]) 4 (mkTree [])
 
-def balanceR (t₁ : Tree α) (x : α) (t₂ : Tree α) : Tree α :=
+def balanceR (t₁ : Tree a) (x : a) (t₂ : Tree a) : Tree a :=
  match t₁ with
  | Tree.null => Tree.null
  | Tree.node _ l y r =>
    if r.height ≥ t₂.height + 2
    then balance l y (balanceR r x t₂)
    else balance l y (node r x t₂)
 
+-- def balanceL ...
+-- def gbalance ...
+
+def mktree : List a → Tree a :=
+  List.foldr insert Tree.null
+
+def sort : List a → List a :=
+  Tree.flatten ∘ mkTree
+
+#eval sort [3, 2, 1, 4, 5, 5] -- bug with duplicated elements!
+
 end BST2
 
 namespace DSet
 open BST2 (insert node)
 
 abbrev Set a := BST2.Tree a
 
+
 def member {a : Type} [LT a] [DecidableRel (α := a) (· < ·)] (x : a) : Set a → Bool
 | .null => false
 | .node _ l y r =>

Fad/Chapter5-Ex.lean

@@ -11,8 +11,11 @@ namespace Chapter5
 section
 open Quicksort
 
-theorem qsort₀_eq_qsort₁ [h₁ : LT β] [h₂ : DecidableRel (α := β) (· < ·)]
-(xs : List β) : qsort₀ xs = qsort₁ xs := by
+variable {a : Type} [h₁ : LT a] [h₂ : DecidableRel (α := a) (· < ·)]
+
+-- trocar cases para induction?
+
+theorem qsort₀_eq_qsort₁ (xs : List a) : qsort₀ xs = qsort₁ xs := by
   cases xs with
   | nil =>
     rw [qsort₀, Function.comp, mkTree, Tree.flatten]
@@ -29,10 +32,10 @@ theorem qsort₀_eq_qsort₁ [h₁ : LT β] [h₂ : DecidableRel (α := β) (·
     have h₂ := qsort₀_eq_qsort₁ (List.filter (not ∘ fun x => decide (x < a)) as)
     rw [h₁, h₂]
 termination_by xs.length
-  decreasing_by
-    all_goals simp
-    all_goals rw [Nat.lt_add_one_iff]
-    all_goals simp [List.length_filter_le]
+decreasing_by
+  all_goals simp
+  all_goals rw [Nat.lt_add_one_iff]
+  all_goals simp [List.length_filter_le]
 
 end
 

Fad/Chapter5.lean

@@ -5,11 +5,13 @@ namespace Chapter5
 
 namespace Quicksort
 
+variable {a : Type} [h₁ : LT a] [h₂ : DecidableRel (α := a) (· < ·)]
+
 inductive Tree a where
 | null : Tree a
 | node : (Tree a) → a → (Tree a) → Tree a
 
-def mkTree [LT a] [DecidableRel (α := a) (· < ·)] : List a → Tree a
+def mkTree: List a → Tree a
 | [] => Tree.null
 | x :: xs =>
   let p := xs.partition (. < x)
@@ -25,10 +27,10 @@ def Tree.flatten : Tree a → List a
 | null => []
 | node l x r => l.flatten ++ [x] ++ r.flatten
 
-def qsort₀ [LT a] [DecidableRel (α := a) (· < ·)] : List a → List a :=
+def qsort₀ : List a → List a :=
  Tree.flatten ∘ mkTree
 
-def qsort₁ [h₁ : LT a] [h₂ : DecidableRel (α := a) (· < ·)] : List a → List a
+def qsort₁ : List a → List a
  | []        => []
  | (x :: xs) =>
   let p := xs.partition (· < x)
@@ -39,6 +41,7 @@ def qsort₁ [h₁ : LT a] [h₂ : DecidableRel (α := a) (· < ·)] : List a 
    [List.partition_eq_filter_filter,
     List.length_filter_le, Nat.lt_add_one_of_le]
 
+
 def qsort₂ [Ord a] (f : a → a → Ordering) : List a → List a
   | []        => []
   | (x :: xs) =>
@@ -78,6 +81,7 @@ instance (a b : Person) : Decidable (a < b) :=
 def people := [
   Person.mk "Alice" 23,
   Person.mk "Bob" 25,
+  Person.mk "Bob" 25,
   Person.mk "Eve" 22]
 
 /-
@@ -88,7 +92,7 @@ def people := [
 end Quicksort
 
 
-namespace S52 -- Mergesort
+namespace Mergesort
 
 inductive Tree (α : Type) : Type where
  | null : Tree α
@@ -235,7 +239,7 @@ def msort₃ [LE a] [DecidableRel (α := a) (· ≤ ·)] : List a → List a
 #eval msort₁ ['a','b','a']
 -/
 
-end S52
+end Mergesort
 
 namespace Heapsort
 
@@ -247,7 +251,7 @@ inductive Tree (α : Type) : Type
 
 def flatten [LE a] [DecidableRel (α := a) (· ≤ ·)] : Tree a → List a
 | Tree.null       => []
-| Tree.node x u v => x :: S52.merge (flatten u) (flatten v)
+| Tree.node x u v => x :: Mergesort.merge (flatten u) (flatten v)
 
 
 open Std.Format in
@@ -264,5 +268,4 @@ instance [ToString a] : Repr (Tree a) where
 
 end Heapsort
 
-
 end Chapter5