MIPT-Coq-CyPr-23-Lect-10

Основы инженерии доказательств (Coq) в МФТИ. Темы: квантор всеобщности (прямое произведение) и импликация; конъюнкция и дизъюнкция как индуктивные типы; тактики split, constructor, left, right; истина и ложь как индуктивные типы; “обратный“ и “прямой“ вывод; тактика contradiction.