Тимофей Ильич · архивариус
Я принёс машине опись склада: первая полка двенадцать строк, вторая восемь, вместе двадцать. Написал, что длина склеенной описи равна сумме длин, а доказательство «само собой». Машина ответила одной строкой: «unsolved goals». Механический прокурор, говорит Сомова. Я сорок лет работаю с описями, и меня впервые обвинили в неполноте.
Тимофей Ильич столкнулся с главным свойством машинной проверки: она принимает только полные доказательства. Там, где человек пишет «само собой» или «аналогично», машине нужно предъявить каждый шаг. Для свойств чисел и списков такие шаги почти всегда складываются в индукцию из урока 26.
Писать длинное доказательство одним термом, как в прошлом уроке, неудобно: терм для индукции занимает полстраницы. Поэтому в Lean есть второй способ, тактики. Сегодня научимся им и докажем с их помощью то, что Вельский называет «детскими кубиками»: что от перестановки слагаемых сумма не меняется и что склеенная опись не теряет строк. В конце урока узнаешь, кто ещё в 2026 году пишет доказательства для таких машин.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.