幼稚園の庭

説明

この課題では、図をもとに、幼稚園のクラスのどの子どもがどの植物を担当しているかを判定します。

クラスには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......................

窓に一番近い1列目には、violetとradishがあります。 2列目には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の学生向けの演習