MIPT-Coq-24-Lect-12
Интерактивное доказывание теорем (Coq) в МФТИ. Темы: индукция по спискам (продолжение); индуктивные определения предикатов (семейств множеств) и принципы индукции для них; примеры доказательств; тактики inversion, remember, change, eapply; индуктивное определение порядка натуральных чисел.
Интерактивное доказывание теорем (Coq) в МФТИ. Темы: индукция по спискам (продолжение); индуктивные определения предикатов (семейств множеств) и принципы индукции для них; примеры доказательств; тактики inversion, remember, change, eapply; индуктивное определение порядка натуральных чисел.