Coq-практикум

Компьютерный практикум по автоматизированной проверке доказательств

Практикум проводится в осеннем полугодии для студентов 3-го курса кафедры математической логики и теории алгоритмов мехмата МГУ.

Осень 2021 г.

Занятие 27 ноября перенесено на 20 ноября.

Занятия проводятся дистанционно, подключение к Zoom осуществляется централизованно.
04.09.2021: видео, слайды, Coq-код. Домашнее задание: установить Coq и CoqIDE; задачи на с. 18–19 методической брошюры.
18.09.2021: видео, Coq-код. Задачи поинтереснее на дом: теорема Кантора; взаимная простота и делимость на простое.
Контрольная работа № 1: формулировки заданий. Тактикой auto пользоваться нельзя! Срок сдачи: 26 сентября 2021 г., 23:00 (МСК). Решения задач нужно прислать по электронной почте преподавателю: sk@mi-ras.ru.
02.10.2021: видео, Coq-код. Домашнее задание: индукция на натуральных числах, задачи №№ 1, 2, 8, 9.
16.10.2021: видео. Домашнее задание: индукция на натуральных числах, оставшиеся задачи.
30.10.2021: видео. Домашнее задание: 1) восстановить пропущенные доказательства prime3 и divis в coprimesZ_p1.v; 2) сформулируйте и докажите в Coq, что сумма кубов первых n натуральных чисел равна квадрату суммы первых n натуральных чисел; 3) сформулируйте и докажите в Coq, что число, десятичная запись которого состоит из 3ⁿ одинаковых цифр, делится на 3ⁿ.
Контрольная работа № 2. Сформулируйте и докажите в Coq:
1. \(\bigl(\sum\limits_{i=0}^{n-1} a_i\bigr) \cdot \bigl(\sum\limits_{j=0}^{m-1} b_j \bigr) = \sum\limits_{i=0}^{n-1} \sum\limits_{j=0}^{m-1} a_i b_j\)
2. \( n^3 \geqslant n + 10 \) при \( n \geqslant 3 \)
3. \( 6^n + 4 \) делится на 5 при любом натуральном \(n\)
4. \( (x+2)^3 + 5x^3 + 4 \) делится на 6 при любом целом \(x\)
5. \( (x-1)^2 \sum\limits_{k=1}^n k x^{k-1} = nx^{n+1} - (n+1) x^n + 1\) при любом целом \(x\) и натуральном \(n\)
Срок сдачи: 8 ноября 2021 г., 23:00 (МСК). Решения задач нужно прислать по электронной почте преподавателю: sk@mi-ras.ru.
13.11.2021: видео; Coq-код: easy_extract.v, easy_extract_Z.v, twin_extr_classic_2021.v, coprimesZ_short.v.
Домашнее задание на извлечение кода. Студенты кафедры математической логики могут выбрать задачу 1 или задачу 2. Студенты других кафедр могут выбрать любую из задач 1, 2, 3.
1. Алгоритм Евклида: в типе nat или в типе Z.
2. Сортировка.
3. Число, не делящееся на данные.
Желательно сдать до 10 декабря.
20.11.2021: видео; Coq-код: coinduc.v. Теоретическая задача: докажите, что существует всюду определённая вычислимая функция на натуральных числах, не представимая в Coq.

Материалы курса:

Брошюра «Компьютерный практикум по математической логике (Coq)» (В. Н. Крупский, С. Л. Кузнецов, версия 2013 года)
Задачи: индукция на натуральных числах (обновлено 27.10.2020).
Задачи поинтереснее (список пополняется)
Задачи на извлечение программного кода (каждый студент выбирает одну задачу):
1. алгоритм Евклида;
2. сортировка;
3. число, не делящееся на данные (задача только для студентов, не специализирующихся по кафедре математической логики и теории алгоритмов).
Ссылки на reference manual: извлечение кода, модуль Coq.Arith.Compare_dec.
Слайды 1-го и 2-го занятий
Домашняя страница Coq

Архив: осень 2020 г.

Осенью 2020 г. занятия проводились дистанционно.
01.09.2020: видео 1, видео 2, слайды, Coq-код. Домашнее задание: установить Coq и CoqIDE; задачи на с. 18–19 методической брошюры.
15.09.2020: видео 1, видео 2, Coq-код. Домашнее задание: докажите в Coq теорему Кантора в следующей формулировке:
```
Require Import Classical.
Theorem Cantor: forall A : Set, ~ exists f: (A -> Prop) -> A,
forall P Q : (A -> Prop), (f P = f Q -> P = Q).
```
Решение
29.09.2020: видео, Coq-код. Домашнее задание: задачи на индукцию, №№ 1, 2, 3, 5, 9.
13.10.2020: видео, Coq-код. Домашнее задание: задачи на индукцию, оставшиеся задачи.
27.10.2020: видео, Coq-код (решения задач №№ 7, 8, 10 на индукцию).
Домашнее задание:
1. Сформулируйте и докажите в Coq следующее утверждение: число, составленное (в десятичной записи) из \(3^n\) одинаковых цифр, делится на \(3^n\).
  Решение
2. Докажите в Coq, что квадрат суммы первых \(n\) натуральных чисел равен сумме кубов первых \(n\) натуральных чисел.
  Решение 1 (в типе nat). Решение 2 (в типе Z)
3. Докажите в Coq иррациональность \(\sqrt{2}\) в следующей формулировке:
```
Theorem sqrt2 : forall m n : nat, n > 0 -> m > 0 -> ~ (n*n = 2*m*m).
```
  Закон исключённого третьего использовать нельзя.
  Решение
4. Определим тип бинарных деревьев с натуральными числами в вершинах следующим образом:
```
Inductive tree :=
  | leaf : nat -> tree
  | node : tree -> nat -> tree -> tree.
```
  Определите на бинарных деревьях функцию mirror, меняющую местами левого и правого потомков у каждой внутренней вершины дерева. Определите также функцию map : (nat -> nat) -> tree -> tree, такую что map f применяет функцию f к числу в каждой вершине дерева. Докажите в Coq, что mirror и map f коммутируют.
  Решение
10.11.2020: видео.
24.11.2020: видео. Coq-код: sumbool.v; twin_extr_classic.v.
08.12.2020: видео. Coq-код: coinduc.v; wf.v; wf_coinduc.v.

Для получения зачёта нужно выполнить указанные ниже задания.

Домашнее задание: извлечение кода

Желательно сдать до пятницы 18 декабря.

Нужно решить одну (по своему выбору) из задач на извлечение программного кода:

алгоритм Евклида;
сортировка;
число, не делящееся на данные (задача только для студентов, не специализирующихся по кафедре математической логики и теории алгоритмов).

Пример: программа, выдающая по данному \(n \geqslant 3\) список из \(n\) различных натуральных чисел, каждое из которых делит их сумму — Coq-код.
Ссылки на reference manual: извлечение кода, модуль Coq.Arith.Compare_dec.

Контрольная работа №2

Срок сдачи: среда 28 октября, 23:00 (МСК).

Решения задач нужно прислать по электронной почте преподавателю: sk@mi-ras.ru.

Можно пользоваться любыми тактиками.

Сформулируйте и докажите в Coq: \(6^n + 4\) делится на 5 для любого \(n\).
Сформулируйте и докажите в Coq: \((1 + x + x^2 + \ldots + x^{n-1})(x-1) = x^n - 1\), где \(n \in \mathbb{N}, x \in \mathbb{Z}\).
Сформулируйте и докажите в Coq: \( 3^{n+1} \geqslant n + 3 \), где \( n \in \mathbb{N}\).
Сформулируйте и докажите в Coq: \( (n+1)! \geqslant 2^n\), где \( n \in \mathbb{N}\).

Контрольная работа №1

Срок сдачи: среда 30 сентября, 23:00 (МСК).

Решения задач нужно прислать по электронной почте преподавателю: sk@mi-ras.ru.

Тактикой auto пользоваться нельзя!

Theorem q1: forall A B : Prop, ((((A -> B) -> A) -> A) -> B) -> B.

Theorem q2: forall (A : Set) (P : A -> Prop),
((forall (x y : A), (P x -> P y)) -> (exists z : A, P z) 
-> forall t : A, P t).

Theorem q3: forall A B : Prop, (A \/ ~ B) /\ B -> A.

Require Import Classical.
Theorem q4: forall A B : Prop, (~ A -> B) -> ~ B -> A.

Theorem q5: forall (A : Set) (D : A -> Prop) (a : A),
exists d : A, (D d -> forall x : A, D x).