From 0a20ac2020ab3ddaec01bb137c0b30a9a1452688 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 19 May 2026 04:02:44 +0000 Subject: [PATCH 1/6] Initial plan From 85f0877d02a4a346a0c15bb8fa40ce378ff49dd0 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 19 May 2026 04:25:00 +0000 Subject: [PATCH 2/6] Add Std.Queue introduction (LeanByExample/Type/Queue.lean) Agent-Logs-Url: https://github.com/lean-ja/lean-by-example/sessions/203320e9-e7e0-4178-b4b5-36a67bb938f1 Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com> --- LeanByExample/Type/Queue.lean | 113 ++++++++++++++++++++++++++++++++++ booksrc/SUMMARY.md | 1 + 2 files changed, 114 insertions(+) create mode 100644 LeanByExample/Type/Queue.lean diff --git a/LeanByExample/Type/Queue.lean b/LeanByExample/Type/Queue.lean new file mode 100644 index 00000000..c9423778 --- /dev/null +++ b/LeanByExample/Type/Queue.lean @@ -0,0 +1,113 @@ +/- # Queue + +`Std.Queue` は、永続的・関数型の **FIFO キュー(先入れ先出しキュー)** です。キューとは、「最初に追加した要素が最初に取り出される」データ構造です。 + +内部的には 2 本の `List` で実装されています。 + +```lean +structure Std.Queue (α : Type u) where + eList : List α + dList : List α +``` + +`dList` は次に取り出す側のリスト、`eList` は追加された要素を逆順に溜める側のリストです。キューの中身は `dList ++ eList.reverse` で表されます。 +-/ +import Std + +open Std + +/- ## 基本操作 + +`Queue` の基本操作を紹介します。 + +### 空のキュー + +`∅` で空のキューを作成できます。`isEmpty` 関数で空かどうかを判定できます。 +-/ + +/-⋆-//-- info: true -/ +#guard_msgs in --# +#eval (∅ : Queue Nat).isEmpty + +/- ### enqueue: 要素の追加 + +`Queue.enqueue` でキューの末尾に要素を追加できます。`toArray` で内容を配列として取り出せます。 +-/ + +/-⋆-//-- info: #[10, 20] -/ +#guard_msgs in --# +#eval ((∅ : Queue Nat).enqueue 10).enqueue 20 |>.toArray + +/- +```admonish warning title="enqueue の引数順" +`Queue.enqueue` の第1引数が追加する値、第2引数がキューです。そのため、`q.enqueue 10` というドット記法を使うと、実際には `Queue.enqueue 10 q` という呼び出しになります。これは `q` に `10` を末尾追加する操作です。 +``` +-/ + +/- ### dequeue?: 要素の取り出し + +`Queue.dequeue?` でキューの先頭から要素を取り出せます。キューが空の場合は `none` を、空でない場合は「取り出した値」と「残りのキュー」のペアを `some` で返します。 + +`do` 記法と組み合わせると、複数の要素を順番に取り出すことができます。 +-/ + +/-- キューから2つの要素を順番に取り出す -/ +def popTwo : Option (Nat × Nat) := do + let q := ((∅ : Queue Nat).enqueue 10).enqueue 20 + let (x, q) ← q.dequeue? + let (y, _) ← q.dequeue? + return (x, y) + +/-⋆-//-- info: some (10, 20) -/ +#guard_msgs in --# +#eval popTwo + +/- ## 計算量 + +`Queue` の各操作の計算量は次のとおりです。 + +* `enqueue` : O(1) +* `dequeue?` : 償却 O(1)、最悪 O(n) + +`dequeue?` の計算量が最悪 O(n) になるのは、`dList` が空になったとき内部で `eList.reverse` が実行されるためです。ただし、その後はしばらく O(1) で動作するため、全体の平均は O(1) です。 + +## 使用例 + +`Queue` は「取り出す順序を保ちたいが、純粋関数型で効率的に動作させたい」場面に適しています。典型的な応用例として、**幅優先探索 (BFS)** が挙げられます。 + +以下は `Queue` を使って二分木のノード値を幅優先順で列挙する例です。 +-/ + +/-- 二分木 -/ +inductive Tree (α : Type) where + | leaf : Tree α + | node (val : α) (left right : Tree α) : Tree α + +/-- `Queue` を使って二分木のノード値を幅優先順 (BFS) で列挙する -/ +partial def Tree.bfsValues (t : Tree α) : List α := + go ((∅ : Queue (Tree α)).enqueue t) [] + where + go (q : Queue (Tree α)) (acc : List α) : List α := + match q.dequeue? with + | none => acc.reverse + | some (.leaf, q') => go q' acc + | some (.node v left right, q') => + go ((q'.enqueue left).enqueue right) (v :: acc) + +/- 以下の二分木でテストします。 + +``` + 1 + / \ + 2 3 + / \ +4 5 +``` +-/ + +-- テスト用の二分木 +def sampleTree : Tree Nat := + .node 1 (.node 2 (.node 4 .leaf .leaf) (.node 5 .leaf .leaf)) (.node 3 .leaf .leaf) + +-- 幅優先順で列挙すると [1, 2, 3, 4, 5] になる +#guard Tree.bfsValues sampleTree = [1, 2, 3, 4, 5] diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 0a183aba..cf31e6ba 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -162,6 +162,7 @@ - [Option: 失敗するかもしれない計算](./Type/Option.md) - [Prod: 型の積](./Type/Prod.md) - [Prop: 命題全体](./Type/Prop.md) + - [Queue: キュー](./Type/Queue.md) - [Quotient: 同値関係による商](./Type/Quotient.md) - [StateM: 状態の書き換え](./Type/StateM.md) - [String: 文字列](./Type/String.md) From 3d2a125f4f8a105cb86388f8282f2eaffc44386e Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Mon, 25 May 2026 01:41:27 +0900 Subject: [PATCH 3/6] =?UTF-8?q?codex=20=E3=81=AB=E3=82=88=E3=82=8B?= =?UTF-8?q?=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Type/Queue.lean | 70 +++++++++++++++++++++++++++++------ 1 file changed, 59 insertions(+), 11 deletions(-) diff --git a/LeanByExample/Type/Queue.lean b/LeanByExample/Type/Queue.lean index c9423778..b59bb304 100644 --- a/LeanByExample/Type/Queue.lean +++ b/LeanByExample/Type/Queue.lean @@ -2,20 +2,41 @@ `Std.Queue` は、永続的・関数型の **FIFO キュー(先入れ先出しキュー)** です。キューとは、「最初に追加した要素が最初に取り出される」データ構造です。 -内部的には 2 本の `List` で実装されています。 +「永続的」というのは、`enqueue` や `dequeue?` が元のキューを破壊的に変更せず、新しいキューを返すという意味です。 -```lean -structure Std.Queue (α : Type u) where - eList : List α - dList : List α -``` - -`dList` は次に取り出す側のリスト、`eList` は追加された要素を逆順に溜める側のリストです。キューの中身は `dList ++ eList.reverse` で表されます。 +内部的には 2 本の `List` を持つ構造体として実装されています。 -/ import Std open Std +--#-- +/-- +info: structure Std.Queue.{u} (α : Type u) : Type u +number of parameters: 1 +fields: + Std.Queue.eList : List α := + [] + Std.Queue.dList : List α := + [] +constructor: + Std.Queue.mk.{u} {α : Type u} (eList dList : List α) : Queue α +-/ +#guard_msgs in #print Std.Queue +--#-- + +namespace Hidden --# + +structure Queue.{u} (α : Type u) where + eList : List α := [] + dList : List α := [] + +end Hidden --# + +/- +`dList` は次に取り出す側のリスト、`eList` は追加された要素を逆順に溜める側のリストです。キューの中身は `dList ++ eList.reverse` で表されます。 +-/ + /- ## 基本操作 `Queue` の基本操作を紹介します。 @@ -38,12 +59,29 @@ open Std #guard_msgs in --# #eval ((∅ : Queue Nat).enqueue 10).enqueue 20 |>.toArray +/- `enqueue` は元のキューを変更せず、新しいキューを返します。 -/ + +def emptyQueue : Queue Nat := ∅ + +def oneElementQueue : Queue Nat := emptyQueue.enqueue 10 + +#guard emptyQueue.isEmpty +#guard oneElementQueue.toArray = #[10] + /- ```admonish warning title="enqueue の引数順" -`Queue.enqueue` の第1引数が追加する値、第2引数がキューです。そのため、`q.enqueue 10` というドット記法を使うと、実際には `Queue.enqueue 10 q` という呼び出しになります。これは `q` に `10` を末尾追加する操作です。 +`Queue.enqueue` は第1引数に追加する値、第2引数にキューを取ります。そのため、`q.enqueue 10` というドット記法は、実際には `Queue.enqueue 10 q` という呼び出しになります。これは `q` に `10` を末尾追加する操作です。 ``` -/ +/-⋆-//-- info: Std.Queue.enqueue.{u} {α : Type u} (v : α) (q : Queue α) : Queue α -/ +#guard_msgs in --# +#check Queue.enqueue + +-- ドット記法ではキューが第2引数の位置に渡される +example (q : Queue Nat) : q.enqueue 10 = Queue.enqueue 10 q := by + rfl + /- ### dequeue?: 要素の取り出し `Queue.dequeue?` でキューの先頭から要素を取り出せます。キューが空の場合は `none` を、空でない場合は「取り出した値」と「残りのキュー」のペアを `some` で返します。 @@ -62,6 +100,16 @@ def popTwo : Option (Nat × Nat) := do #guard_msgs in --# #eval popTwo +-- 空のキューからは取り出せない +#guard (∅ : Queue Nat).dequeue? = none + +-- 取り出したあとのキューには、次に取り出される要素が残っている +#guard + let q := ((∅ : Queue Nat).enqueue 10).enqueue 20 + match q.dequeue? with + | none => false + | some (x, q') => x = 10 && q'.toArray == #[20] + /- ## 計算量 `Queue` の各操作の計算量は次のとおりです。 @@ -69,7 +117,7 @@ def popTwo : Option (Nat × Nat) := do * `enqueue` : O(1) * `dequeue?` : 償却 O(1)、最悪 O(n) -`dequeue?` の計算量が最悪 O(n) になるのは、`dList` が空になったとき内部で `eList.reverse` が実行されるためです。ただし、その後はしばらく O(1) で動作するため、全体の平均は O(1) です。 +`dequeue?` の計算量が最悪 O(n) になるのは、`dList` が空になったとき内部で `eList.reverse` が実行されるためです。ただし、いったん反転した要素はその後しばらく O(1) で取り出せるため、一連の操作全体では償却 O(1) になります。 ## 使用例 @@ -84,7 +132,7 @@ inductive Tree (α : Type) where | node (val : α) (left right : Tree α) : Tree α /-- `Queue` を使って二分木のノード値を幅優先順 (BFS) で列挙する -/ -partial def Tree.bfsValues (t : Tree α) : List α := +partial def Tree.bfsValues {α : Type} (t : Tree α) : List α := go ((∅ : Queue (Tree α)).enqueue t) [] where go (q : Queue (Tree α)) (acc : List α) : List α := From b70d6ab783924d072fc65ef75c23c9befdd69072 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 00:16:53 +0900 Subject: [PATCH 4/6] =?UTF-8?q?=E6=A0=A1=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Type/Queue.lean | 107 ++++++++++++---------------------- 1 file changed, 36 insertions(+), 71 deletions(-) diff --git a/LeanByExample/Type/Queue.lean b/LeanByExample/Type/Queue.lean index b59bb304..cc2e3832 100644 --- a/LeanByExample/Type/Queue.lean +++ b/LeanByExample/Type/Queue.lean @@ -1,15 +1,12 @@ /- # Queue -`Std.Queue` は、永続的・関数型の **FIFO キュー(先入れ先出しキュー)** です。キューとは、「最初に追加した要素が最初に取り出される」データ構造です。 - -「永続的」というのは、`enqueue` や `dequeue?` が元のキューを破壊的に変更せず、新しいキューを返すという意味です。 +`Std.Queue` は、**FIFO キュー(先入れ先出しキュー)** です。キューとは、「先に追加した要素が先に取り出される」データ構造のことで、たとえばレジ待ちの行列はキューの例になっています。 内部的には 2 本の `List` を持つ構造体として実装されています。 -/ import Std open Std - --#-- /-- info: structure Std.Queue.{u} (α : Type u) : Type u @@ -24,7 +21,6 @@ constructor: -/ #guard_msgs in #print Std.Queue --#-- - namespace Hidden --# structure Queue.{u} (α : Type u) where @@ -32,9 +28,10 @@ structure Queue.{u} (α : Type u) where dList : List α := [] end Hidden --# - /- -`dList` は次に取り出す側のリスト、`eList` は追加された要素を逆順に溜める側のリストです。キューの中身は `dList ++ eList.reverse` で表されます。 +`dList` は次に取り出す側のリスト、`eList` は追加された要素をスタック的に貯めていくリストです。 + +キューの中身は `dList ++ eList.reverse` と常に一致します。 -/ /- ## 基本操作 @@ -43,85 +40,55 @@ end Hidden --# ### 空のキュー -`∅` で空のキューを作成できます。`isEmpty` 関数で空かどうかを判定できます。 --/ - -/-⋆-//-- info: true -/ -#guard_msgs in --# -#eval (∅ : Queue Nat).isEmpty - -/- ### enqueue: 要素の追加 - -`Queue.enqueue` でキューの末尾に要素を追加できます。`toArray` で内容を配列として取り出せます。 +`empty` で空のキューを作成できるほか、`isEmpty` 関数で空かどうかを判定できます。`empty` のことを `∅` と書くこともできます。 -/ -/-⋆-//-- info: #[10, 20] -/ -#guard_msgs in --# -#eval ((∅ : Queue Nat).enqueue 10).enqueue 20 |>.toArray - -/- `enqueue` は元のキューを変更せず、新しいキューを返します。 -/ - -def emptyQueue : Queue Nat := ∅ +#guard (Queue.empty : Queue Nat).isEmpty -def oneElementQueue : Queue Nat := emptyQueue.enqueue 10 +#guard (∅ : Queue Nat).isEmpty -#guard emptyQueue.isEmpty -#guard oneElementQueue.toArray = #[10] +/- ### 要素の追加 -/- -```admonish warning title="enqueue の引数順" -`Queue.enqueue` は第1引数に追加する値、第2引数にキューを取ります。そのため、`q.enqueue 10` というドット記法は、実際には `Queue.enqueue 10 q` という呼び出しになります。これは `q` に `10` を末尾追加する操作です。 -``` +`enqueue` でキューの末尾に要素を追加できます。`toArray` で内容を配列として取り出せます。 -/ -/-⋆-//-- info: Std.Queue.enqueue.{u} {α : Type u} (v : α) (q : Queue α) : Queue α -/ +/-⋆-//-- info: #[10, 20] -/ #guard_msgs in --# -#check Queue.enqueue +#eval (∅ : Queue Nat) + |>.enqueue 10 + |>.enqueue 20 + |>.toArray --- ドット記法ではキューが第2引数の位置に渡される -example (q : Queue Nat) : q.enqueue 10 = Queue.enqueue 10 q := by - rfl +/- `enqueueAll` で、複数の要素をキューに追加できます。このとき順序が逆になることに注意してください。 -/ -/- ### dequeue?: 要素の取り出し +#guard + let q := (∅ : Queue Nat).enqueueAll [10, 20] + q.toArray = #[20, 10] -`Queue.dequeue?` でキューの先頭から要素を取り出せます。キューが空の場合は `none` を、空でない場合は「取り出した値」と「残りのキュー」のペアを `some` で返します。 +/- ### 要素の取り出し -`do` 記法と組み合わせると、複数の要素を順番に取り出すことができます。 +`Queue.dequeue?` でキューの先頭から要素を取り出せます。キューが空の場合は `none` を、空でない場合は「取り出した値」と「残りのキュー」のペアを `some` で包んで返します。 -/ /-- キューから2つの要素を順番に取り出す -/ -def popTwo : Option (Nat × Nat) := do - let q := ((∅ : Queue Nat).enqueue 10).enqueue 20 +def popTwo {α : Type} (q : Queue α) : Option (α × α) := do let (x, q) ← q.dequeue? let (y, _) ← q.dequeue? return (x, y) -/-⋆-//-- info: some (10, 20) -/ -#guard_msgs in --# -#eval popTwo - --- 空のキューからは取り出せない -#guard (∅ : Queue Nat).dequeue? = none - --- 取り出したあとのキューには、次に取り出される要素が残っている +-- 10 を入れて 20 を入れると、 +-- 取り出すときには 10 が出て次に 20 が出てくる #guard let q := ((∅ : Queue Nat).enqueue 10).enqueue 20 - match q.dequeue? with - | none => false - | some (x, q') => x = 10 && q'.toArray == #[20] + popTwo q = some (10, 20) -/- ## 計算量 - -`Queue` の各操作の計算量は次のとおりです。 - -* `enqueue` : O(1) -* `dequeue?` : 償却 O(1)、最悪 O(n) - -`dequeue?` の計算量が最悪 O(n) になるのは、`dList` が空になったとき内部で `eList.reverse` が実行されるためです。ただし、いったん反転した要素はその後しばらく O(1) で取り出せるため、一連の操作全体では償却 O(1) になります。 +-- 空のキューからは取り出せない +#guard (∅ : Queue Nat).dequeue? = none +/- ## 使用例 -`Queue` は「取り出す順序を保ちたいが、純粋関数型で効率的に動作させたい」場面に適しています。典型的な応用例として、**幅優先探索 (BFS)** が挙げられます。 +キューというデータ構造の典型的な応用例として、**幅優先探索 (BFS)** が挙げられます。 以下は `Queue` を使って二分木のノード値を幅優先順で列挙する例です。 -/ @@ -134,15 +101,15 @@ inductive Tree (α : Type) where /-- `Queue` を使って二分木のノード値を幅優先順 (BFS) で列挙する -/ partial def Tree.bfsValues {α : Type} (t : Tree α) : List α := go ((∅ : Queue (Tree α)).enqueue t) [] - where - go (q : Queue (Tree α)) (acc : List α) : List α := - match q.dequeue? with - | none => acc.reverse - | some (.leaf, q') => go q' acc - | some (.node v left right, q') => - go ((q'.enqueue left).enqueue right) (v :: acc) +where + go (q : Queue (Tree α)) (acc : List α) : List α := + match q.dequeue? with + | none => acc.reverse + | some (.leaf, q') => go q' acc + | some (.node v left right, q') => + go ((q'.enqueue left).enqueue right) (v :: acc) -/- 以下の二分木でテストします。 +/-- テスト用の二分木 ``` 1 @@ -152,8 +119,6 @@ partial def Tree.bfsValues {α : Type} (t : Tree α) : List α := 4 5 ``` -/ - --- テスト用の二分木 def sampleTree : Tree Nat := .node 1 (.node 2 (.node 4 .leaf .leaf) (.node 5 .leaf .leaf)) (.node 3 .leaf .leaf) From d57267b50373e198676af272da0e494393e53d10 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 00:37:33 +0900 Subject: [PATCH 5/6] =?UTF-8?q?=E5=B9=85=E5=84=AA=E5=85=88=E6=8E=A2?= =?UTF-8?q?=E7=B4=A2=E3=81=AE=E3=82=B3=E3=83=BC=E3=83=89=E3=82=92=20`do`?= =?UTF-8?q?=20=E6=A7=8B=E6=96=87=E3=81=A7=E6=9B=B8=E3=81=8D=E7=9B=B4?= =?UTF-8?q?=E3=81=99?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Type/Queue.lean | 37 +++++++++++++++++++++++++---------- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/LeanByExample/Type/Queue.lean b/LeanByExample/Type/Queue.lean index cc2e3832..be9a18e5 100644 --- a/LeanByExample/Type/Queue.lean +++ b/LeanByExample/Type/Queue.lean @@ -99,15 +99,32 @@ inductive Tree (α : Type) where | node (val : α) (left right : Tree α) : Tree α /-- `Queue` を使って二分木のノード値を幅優先順 (BFS) で列挙する -/ -partial def Tree.bfsValues {α : Type} (t : Tree α) : List α := - go ((∅ : Queue (Tree α)).enqueue t) [] -where - go (q : Queue (Tree α)) (acc : List α) : List α := - match q.dequeue? with - | none => acc.reverse - | some (.leaf, q') => go q' acc - | some (.node v left right, q') => - go ((q'.enqueue left).enqueue right) (v :: acc) +def Tree.bfsValues {α : Type} (t : Tree α) : Array α := Id.run do + -- キューを空の状態で初期化 + -- このキューは「これから訪問するべきノード」を管理する + let mut q : Queue (Tree α) := ∅ + let mut result : Array α := #[] + + -- ルートノードをキューに追加 + q := q.enqueue t + + -- キューが空になるまでループ + while !q.isEmpty do + let some (v, q') ← q.dequeue? + | unreachable! + + match v with + | .leaf => + -- 何も追加せずに次のループへ + q := q' + continue + | .node val left right => + result := result.push val + + -- 左の木、右の木の順にキューに追加 + q := q'.enqueue left |>.enqueue right + + return result /-- テスト用の二分木 @@ -123,4 +140,4 @@ def sampleTree : Tree Nat := .node 1 (.node 2 (.node 4 .leaf .leaf) (.node 5 .leaf .leaf)) (.node 3 .leaf .leaf) -- 幅優先順で列挙すると [1, 2, 3, 4, 5] になる -#guard Tree.bfsValues sampleTree = [1, 2, 3, 4, 5] +#guard Tree.bfsValues sampleTree = #[1, 2, 3, 4, 5] From 1e9e4877cb34918a5ff73fac1b827f601a13a35c Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 00:56:02 +0900 Subject: [PATCH 6/6] =?UTF-8?q?=E6=96=87=E7=AB=A0=E6=A0=A1=E6=AD=A3:=20?= =?UTF-8?q?=E5=86=85=E9=83=A8=E5=AE=9F=E8=A3=85=E3=81=AE=E8=A9=B1=E3=82=92?= =?UTF-8?q?=E5=BE=8C=E5=8D=8A=E3=81=AB=E7=A7=BB=E5=8B=95=E3=81=95=E3=81=9B?= =?UTF-8?q?=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Type/Queue.lean | 80 +++++++++++++++++++++++------------ 1 file changed, 52 insertions(+), 28 deletions(-) diff --git a/LeanByExample/Type/Queue.lean b/LeanByExample/Type/Queue.lean index be9a18e5..7e17f572 100644 --- a/LeanByExample/Type/Queue.lean +++ b/LeanByExample/Type/Queue.lean @@ -1,39 +1,12 @@ /- # Queue `Std.Queue` は、**FIFO キュー(先入れ先出しキュー)** です。キューとは、「先に追加した要素が先に取り出される」データ構造のことで、たとえばレジ待ちの行列はキューの例になっています。 - -内部的には 2 本の `List` を持つ構造体として実装されています。 -/ import Std open Std ---#-- -/-- -info: structure Std.Queue.{u} (α : Type u) : Type u -number of parameters: 1 -fields: - Std.Queue.eList : List α := - [] - Std.Queue.dList : List α := - [] -constructor: - Std.Queue.mk.{u} {α : Type u} (eList dList : List α) : Queue α --/ -#guard_msgs in #print Std.Queue ---#-- -namespace Hidden --# - -structure Queue.{u} (α : Type u) where - eList : List α := [] - dList : List α := [] - -end Hidden --# -/- -`dList` は次に取り出す側のリスト、`eList` は追加された要素をスタック的に貯めていくリストです。 - -キューの中身は `dList ++ eList.reverse` と常に一致します。 --/ +#check Queue /- ## 基本操作 `Queue` の基本操作を紹介します。 @@ -85,6 +58,57 @@ def popTwo {α : Type} (q : Queue α) : Option (α × α) := do -- 空のキューからは取り出せない #guard (∅ : Queue Nat).dequeue? = none +/- +## 内部実装 + +内部的には `Std.Queue` は２本の `List` を持つ構造体として実装されています。 +-/ +--#-- +/-- +info: structure Std.Queue.{u} (α : Type u) : Type u +number of parameters: 1 +fields: + Std.Queue.eList : List α := + [] + Std.Queue.dList : List α := + [] +constructor: + Std.Queue.mk.{u} {α : Type u} (eList dList : List α) : Queue α +-/ +#guard_msgs in #print Std.Queue +--#-- +namespace Hidden --# + +structure Queue.{u} (α : Type u) where + eList : List α := [] + dList : List α := [] + +end Hidden --# +/- +`Std.Queue` の２つのフィールドのそれぞれについて説明します。`eList` は追加された要素を貯めていくリストで、キューに追加された要素は `eList` の先頭に追加されます。 +-/ + +/-⋆-//-- info: { eList := [6, 5, 4, 3], dList := [1, 2] } -/ +#guard_msgs in --# +#eval + let q : Queue Nat := { eList := [5, 4, 3], dList := [1, 2] } + q.enqueue 6 + +/- `dList` は次に取り出す側のリストです。キューから要素を取り出すとき、まず `dList` の先頭から要素が取り出されます。 -/ + +/-⋆-//-- info: { eList := [5, 4, 3], dList := [2] } -/ +#guard_msgs in --# +#eval + let q : Queue Nat := { eList := [5, 4, 3], dList := [1, 2] } + let (_, q') := q.dequeue?.get! + q' + +/- キューの `toArray` による出力は `(dList ++ eList.reverse).toArray` と常に一致します。 -/ + +example {α : Type} (q : Queue α) + : (q.dList ++ q.eList.reverse).toArray = q.toArray := by + simp [Queue.toArray, List.append_toArray, List.reverse_toArray] + /- ## 使用例