MIPT-Coq-24-Lect-13

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: метод рефлексии, индуктивные "спецификации" булевозначных предикатов, разрешимые предикаты; индуктивное определение перестановок; индуктивное определение неубывания; спецификация алгоритма сортировки.