幼兒園花園

說明

你的任務是：給定一張圖，判斷幼兒園班級裡每個小朋友負責照顧哪些植物。

班上有 12 個小朋友：

• Alice、Bob、Charlie、David、Eve、Fred、Ginny、Harriet、Ileana、Joseph、Kincaid 和 Larry。

這裡種了 4 種不同的種子：

每個小朋友分到 4 個杯子，每一排 2 個：

[window][window][window]
........................ # each dot represents a cup
........................

老師會依照小朋友名字的字母順序分配杯子，所以 Alice 排在最前面，Larry 排在最後。

以下是 Alice 的植物範例圖：

[window][window][window]
VR......................
RG......................

第一排最靠近窗戶，她有一株紫羅蘭和一株蘿蔔。第二排則有一株蘿蔔和一些草。

你的程式會收到植物的排列，從最靠近窗戶的那一排開始，由左到右讀取。根據這些資訊，它就能判斷哪些植物屬於哪個小朋友。

舉例來說，如果告訴它花園長這樣：

[window][window][window]
VRCGVVRVCGGCCGVRGCVCGCGV
VRCCCGCRRGVCGCRVVCVGCGCV

那麼問到 Alice 的植物時，它應該給出：

• Violets, radishes, violets, radishes

而問到 Bob 的植物時，則會得到：

• Clover, grass, clover, clover

向量

plants函式的回傳值是Vector Plant 4。

向量代表長度固定的陣列。 這個長度也可以在執行階段決定。 可以把向量想成一個組合：一個Array，加上一個證明，證明這個陣列具有所需的長度。 這表示你必須提供這個證明，才能建構出一個Vector。

這一章對 Lean 的定理證明提供了很好的入門介紹。 如果想更深入，Lean 官網把這本書列為官方資源。

Lean 提供了許多策略，可以自動完成整個證明或其中一部分。 你可能會想查看語言參考文件。

---

出處

由 JumpstartLab 團隊為 The Turing School of Software and Design 的學生所設計的練習。