幼儿园花园

说明

你的任务是：给定一张图示，判断幼儿园班里的每个孩子负责哪些植物。

班里有 12 个孩子：

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

这里种着四种不同的种子：

每个孩子分到四个杯子，每行两个：

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

老师按照孩子名字的字母顺序来分配杯子，也就是说 Alice 排在最前面，Larry 排在最后。

下面是一张示例图示，表示 Alice 的植物：

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

在离窗户最近的第一行，她有一株 violet 和一株 radish。 第二行，她有一株 radish 和一些 grass。

你的程序会按从左到右的顺序收到这些植物，从离窗户最近的那一行开始。 据此，它应该能判断出每株植物分别属于哪个学生。

例如，如果告诉它花园长这样：

[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 的学生编写的练习。