MIPT-Coq-CyPr-23-Lect-06

Основы инженерии доказательств (Coq) в МФТИ: дальнейшие примеры в импликативном фрагменте пропозициональной логики; контекст доказательства (“дано“) и цель (“требуется“); тактики intro(s), exact, assumption, apply; прозрачные и непрозрачные (opaque) определения термов; простейшая автоматизация, тактикалы; восстановление терма по тактикам.