مقدمه
کلاس مهدکودک در حال یادگیری درباره‌ی رشد گیاهان است.
معلم فکر کرد ایده‌ی خوبی است که به بچه‌های کلاس دانه بدهد تا در خاک بکارند و رشد دهند.
برای همین، بچه‌ها لیوان‌های کوچکی را کنار طاقچه‌های پنجره گذاشته‌اند و در هر لیوان یک نوع گیاه کاشته‌اند.
بچه‌ها توانستند از میان چهار نوع دانه‌ی موجود، نوع مورد علاقه‌شان را انتخاب کنند: چمن، شبدر، تربچه و بنفشه.
دستورالعمل‌ها
وظیفه‌ی شما این است که با در دست داشتن یک نمودار، مشخص کنید هر کودک در کلاس مهدکودک مسئول کدام گیاهان است.
در این کلاس ۱۲ کودک هستند:
- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid, and Larry.
چهار نوع مختلف بذر کاشته می‌شود:
| گیاه |
کدگذاری در نمودار |
| Grass |
G |
| Clover |
C |
| Radish |
R |
| Violet |
V |
هر کودک چهار لیوان دارد، دو تا در هر ردیف:
[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 تاکتیک‌های زیادی ارائه می‌دهد که می‌توانند یک اثبات یا بخش‌هایی از آن را خودکار کنند.
شاید بد نباشد نگاهی به مرجع زبان بیندازید.
