MIPT-Coq-24-Lect-08
Интерактивное доказывание теорем (Coq) в МФТИ. Темы: конъюнкция, дизъюнкция, истина, ложь и квантор существования как семейства индуктивных типов; конструкторы как "аксиомы введения"; proof irrelevance, принципы индукции для типов сорта Prop как "аксиомы удаления"; тактики split, left, right, exists; тактика apply для прямых и обратных рассуждений; (вопрос слушателя:) область видимости "объявленных, но не определенных" термов, команды Parameter/Axiom и Variable/Hypothesis.
Интерактивное доказывание теорем (Coq) в МФТИ. Темы: конъюнкция, дизъюнкция, истина, ложь и квантор существования как семейства индуктивных типов; конструкторы как "аксиомы введения"; proof irrelevance, принципы индукции для типов сорта Prop как "аксиомы удаления"; тактики split, left, right, exists; тактика apply для прямых и обратных рассуждений; (вопрос слушателя:) область видимости "объявленных, но не определенных" термов, команды Parameter/Axiom и Variable/Hypothesis.