Coq-практикум

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

Практикум проводится в осеннем полугодии для студентов 3-го курса кафедры математической логики и теории алгоритмов мехмата МГУ.
Осенью 2020 г. занятия проводятся дистанционно.
Для получения зачёта нужно выполнить указанные ниже задания.

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

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

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

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

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

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

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

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

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