Вступ
Клас у дитячому садку вивчає вирощування рослин.
Вихователю спало на думку дати класу насіння, щоб посадити його та виростити в землі.
Для цього діти розставили маленькі скляночки на підвіконнях і посадили в кожну скляночку один вид рослини.
Діти могли обрати свої улюблені з чотирьох доступних видів насіння: grass, clover, radishes і violets.
Вказівки
Визначте за діаграмою, за які рослини відповідає кожна дитина в класі дитячого садка.
У класі 12 дітей:
- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid і 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......................
У першому рядку, найближчому до вікон, у неї є фіалка і редиска.
У другому рядку в неї редиска і трохи трави.
Програма отримає рослини зліва направо, починаючи з рядка, найближчого до вікон.
З цього вона зможе визначити, які рослини належать кожній дитині.
Наприклад, якщо сказано, що садок має такий вигляд:
[window][window][window]
VRCGVVRVCGGCCGVRGCVCGCGV
VRCCCGCRRGVCGCRVVCVGCGCV
Тоді, якщо запитати про рослини Alice, вона повинна повернути:
- Violets, radishes, violets, radishes
А якщо запитати про рослини Bob, то отримаємо:
- Clover, grass, clover, clover
Вектори
Поверненим значенням функції plants є Vector Plant 4.
Вектори являють собою масиви з фіксованою довжиною.
Цю довжину можна також визначити під час виконання.
Їх можна уявити як пару, що складається з Array і доведення того, що масив має потрібну довжину.
Це означає, що для створення Vector потрібно надати це доведення.
Цей розділ дає добрий вступ до доведення теорем у Lean.
Для глибшого занурення ця книжка вказана як офіційний ресурс на сайті Lean.
Lean пропонує багато тактик, які можуть автоматизувати доведення або його частини.
Можливо, варто звернутися до довідника з мови.
