MIPT-Coq-24-Lect-09
Интерактивное доказывание теорем (Coq) в МФТИ. Темы: зависимая сумма sig, "программистский" аналог квантора существования, подтипы; равенство как семейство индуктивных предикатов; тактики pattern, rewrite и reflexivity; неравенство термов индуктивного типа, тактики discriminate и inversion; некоторые трюки с равенством.
Интерактивное доказывание теорем (Coq) в МФТИ. Темы: зависимая сумма sig, "программистский" аналог квантора существования, подтипы; равенство как семейство индуктивных предикатов; тактики pattern, rewrite и reflexivity; неравенство термов индуктивного типа, тактики discriminate и inversion; некоторые трюки с равенством.