From 35eb64fff2a0fb20ed30fdb3e593dd37b6ca420f Mon Sep 17 00:00:00 2001 From: spinylobster Date: Mon, 22 Jul 2024 23:26:39 +0900 Subject: [PATCH 1/2] =?UTF-8?q?2024/7/22=20=E3=81=AE=E3=82=BC=E3=83=9F?= =?UTF-8?q?=E3=81=AE=E6=88=90=E6=9E=9C?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Src/Problem50.lean | 94 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 94 insertions(+) create mode 100644 Src/Problem50.lean diff --git a/Src/Problem50.lean b/Src/Problem50.lean new file mode 100644 index 0000000..e218deb --- /dev/null +++ b/Src/Problem50.lean @@ -0,0 +1,94 @@ +set_option autoImplicit false + +def plain := "BACADAEAFABBAAAGAH" + +def Encoder := Char → String + +def encoder₁ : Encoder + | 'A' => "000" | 'B' => "001" | 'C' => "010" | 'D' => "011" + | 'E' => "100" | 'F' => "101" | 'G' => "110" | 'H' => "111" + | _ => "" + +def encode (f : Encoder) (p : String) : String := + p.data.foldl (fun acc x => acc ++ f x) "" + +def encoder₂ : Encoder + | 'A' => "0" | 'B' => "100" | 'C' => "1010" | 'D' => "1011" + | 'E' => "1100" | 'F' => "1101" | 'G' => "1110" | 'H' => "1111" + | _ => "" + +#guard encode encoder₁ plain = + "001000010000011000100000101000001001000000000110000111" +#guard encode encoder₂ plain = + "100010100101101100011010100100000111001111" + +inductive HuffTree where + | Node (left : HuffTree) (right : HuffTree) + | Leaf (c : Char) (weight : Nat) +deriving Inhabited + +def HuffTree.toString' : HuffTree → String × Nat + | .Leaf c w => (c.toString, w) + | .Node l r => + let (ls, lw) := l.toString' + let (rs, rw) := r.toString' + (ls ++ rs, lw + rw) + +def HuffTree.toString (t : HuffTree) : String := + match t with + | .Leaf c w => s!"({c} {w})" + | .Node _ _ => + let (s, w) := t.toString' + let s' := " ".intercalate <| s.data.map (·.toString) + "({" ++ s' ++ "} " ++ ToString.toString w ++ ")" + +instance : ToString HuffTree := ⟨HuffTree.toString⟩ + +#eval "aaabc".data.eraseDups + +def String.freq (s : String) (c : Char) := s.data.filter (· == c) |>.length + +def String.toLeaves (s : String) : List HuffTree := + let allChars : List Char := s.data.eraseDups + allChars.map fun c => HuffTree.Leaf c (s.freq c) + +#eval plain.toLeaves +#eval HuffTree.Node (HuffTree.Leaf 'c' 1) (HuffTree.Leaf 'd' 1) + +variable {α : Type} + +/-- Insert an element in a way that +does not break the order of the sorted list. -/ +def orderedInsert (a : α) (ord : α → Nat) : List α → List α + | [] => [a] + | b :: l => + if ord a ≤ ord b then a :: b :: l + else b :: orderedInsert a ord l + +/-- insertion sort -/ +def insertionSort (ord : α → Nat) : List α → List α + | [] => [] + | b :: l => orderedInsert b ord <| insertionSort ord l + +def HuffTree.weight : HuffTree → Nat + | Leaf _ w => w + | Node l r => l.weight + r.weight + +def HuffTree.sort (trees : List HuffTree) : List HuffTree := insertionSort (HuffTree.weight) trees + +#eval plain.toLeaves |> HuffTree.sort + +partial def HuffTree.merge (leaves : List HuffTree) : List HuffTree := + let sorted := leaves |> HuffTree.sort + dbg_trace sorted + match sorted with + | [] => [] + | [tree] => [tree] + | t1 :: t2 :: rest => + let t' := HuffTree.Node t1 t2 + HuffTree.merge (t' :: rest) + +def HuffTree.ofString (msg : String) : HuffTree := + msg.toLeaves |> HuffTree.merge |>.head! + +#eval HuffTree.ofString plain From 0e95dccd6b1160dd996949b7a6f7f36d5c7e685a Mon Sep 17 00:00:00 2001 From: spinylobster Date: Mon, 29 Jul 2024 22:51:19 +0900 Subject: [PATCH 2/2] solve 50 --- Src/Problem50.lean | 43 ++++++++++++++----------------------------- 1 file changed, 14 insertions(+), 29 deletions(-) diff --git a/Src/Problem50.lean b/Src/Problem50.lean index e218deb..87adbf9 100644 --- a/Src/Problem50.lean +++ b/Src/Problem50.lean @@ -1,27 +1,5 @@ set_option autoImplicit false -def plain := "BACADAEAFABBAAAGAH" - -def Encoder := Char → String - -def encoder₁ : Encoder - | 'A' => "000" | 'B' => "001" | 'C' => "010" | 'D' => "011" - | 'E' => "100" | 'F' => "101" | 'G' => "110" | 'H' => "111" - | _ => "" - -def encode (f : Encoder) (p : String) : String := - p.data.foldl (fun acc x => acc ++ f x) "" - -def encoder₂ : Encoder - | 'A' => "0" | 'B' => "100" | 'C' => "1010" | 'D' => "1011" - | 'E' => "1100" | 'F' => "1101" | 'G' => "1110" | 'H' => "1111" - | _ => "" - -#guard encode encoder₁ plain = - "001000010000011000100000101000001001000000000110000111" -#guard encode encoder₂ plain = - "100010100101101100011010100100000111001111" - inductive HuffTree where | Node (left : HuffTree) (right : HuffTree) | Leaf (c : Char) (weight : Nat) @@ -44,15 +22,12 @@ def HuffTree.toString (t : HuffTree) : String := instance : ToString HuffTree := ⟨HuffTree.toString⟩ -#eval "aaabc".data.eraseDups - def String.freq (s : String) (c : Char) := s.data.filter (· == c) |>.length def String.toLeaves (s : String) : List HuffTree := let allChars : List Char := s.data.eraseDups allChars.map fun c => HuffTree.Leaf c (s.freq c) -#eval plain.toLeaves #eval HuffTree.Node (HuffTree.Leaf 'c' 1) (HuffTree.Leaf 'd' 1) variable {α : Type} @@ -76,11 +51,8 @@ def HuffTree.weight : HuffTree → Nat def HuffTree.sort (trees : List HuffTree) : List HuffTree := insertionSort (HuffTree.weight) trees -#eval plain.toLeaves |> HuffTree.sort - partial def HuffTree.merge (leaves : List HuffTree) : List HuffTree := let sorted := leaves |> HuffTree.sort - dbg_trace sorted match sorted with | [] => [] | [tree] => [tree] @@ -91,4 +63,17 @@ partial def HuffTree.merge (leaves : List HuffTree) : List HuffTree := def HuffTree.ofString (msg : String) : HuffTree := msg.toLeaves |> HuffTree.merge |>.head! -#eval HuffTree.ofString plain +def HuffTree.encode (c : Char) : HuffTree → Option String + | .Leaf c' _ => if c = c' then some "" else none + | .Node l r => + match r.encode c with + | none => l.encode c |>.map ("0" ++ ·) + | some s => "1" ++ s + +def huffman (input : List (Char × Nat)) : List (Char × String) := + let leaves : List HuffTree := input.map (fun (c, w) => HuffTree.Leaf c w) + let tree : HuffTree := HuffTree.merge leaves |>.head! + input.map (fun (c, _) => (c, tree.encode c |>.get!)) + +#guard huffman [('a',45),('b',13),('c',12),('d',16),('e',9),('f',5)] = + [('a',"0"),('b',"101"),('c',"100"),('d',"111"),('e',"1101"),('f',"1100")]