Coq-практикум

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

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

Осень 2024 г.

Занятия проходят в 9:00 в ауд. 16-03, по следующим субботам: 5, 12, 19, 26 октября; 30 ноября; 7, 14 декабря.

Материалы: методическая брошюра; официальный сайт Coq; задачи на индукцию по натуральным числам.
Код с занятий: class1.v (05.10), class2.v (12.10), class3.v (19.10), class4.v (26.10), class6.v (07.12)
Контрольная работа № 1: формулировки заданий. Тактикой auto пользоваться нельзя! Срок сдачи: 25 октября 2024 г., 23:00 (МСК). Решения задач нужно прислать по электронной почте преподавателю: sk@mi-ras.ru.
Контрольная работа № 2. Сформулируйте и докажите в Coq:
1. \( 2 \cdot (1 + 3 + 9 + \ldots + 3^{n-1}) + 1 = 3^n \)
2. \(\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\)
3. Докажите, что \( (n+2)! \geqslant 3^n \) для любого натурального \(n\)
4. \( (x+6)^4 + 23 x^4 \) делится на 24 при любом целом \(x\)
5. \( (x-1)^2 \sum\limits_{k=1}^n k x^{k-1} = nx^{n+1} - (n+1) x^n + 1\) при любом целом \(x\) и натуральном \(n\)
Срок сдачи: 1 декабря 2024 г., 23:00 (МСК). Решения задач нужно прислать по электронной почте преподавателю: sk@mi-ras.ru.
Домашнее задание на извлечение кода. Студенты кафедры математической логики могут выбрать задачу 1 или задачу 2. Студенты других кафедр могут выбрать любую из задач 1, 2, 3.
1. Алгоритм Евклида: в типе nat или в типе Z.
2. Сортировка.
3. Число, не делящееся на данные.
Желательно сдать до 20 декабря.

Ниже приведены материалы прошлых лет (в т.ч. видеозаписи занятий, проводившихся онлайн).

Осень 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).