CS301. Теория языков программирования

Балл №1: 

Для получения одного балла необходимо в лабораторной № 1 нужно до конца пройти Functional Programming in Coq (Basics).

Балл №2:

Для получения одного балла необходимо в лабораторной № 2 решить задания всего подраздела Proof by Induction    (Induction).

Балл №3:

Для получения одного балла необходимо в лабораторной № 3 решить задания всего подраздела Working with Structured Data    (Lists).

Балл №4:

Доказать теорему, сформулированную на лекции о том, что количество констант в терме меньше или равно размеру этого терма. Код приведен в файле Example.v. Учтите, что в реализации использьзуется список (seq), а не множество. Для списка выполняется условие |s1 ++ s2| = |s1| + |s2|. А для множества |s1| + |s2| <= |s1 ++ s2| (Так как при объединении множеств, если в них были одинаковые элементы, то они заменяться на один в их объединении, в отличии от списков).

Для для доказательства может быть полезна библиотека ssrnat. При необходимости можно доказать вспомогательные леммы или ввести аксиомы (но не злоупотреблять аксиомами).

• Первый доказавший - 1 бонусный балл
• Второй доказавший  - 0.75 бонусных балла
• Третий доказавший  - 0.5 бонусных балла

Срок сдачи неограничен (до конца семестра).

Балл №5:

Решение дополнительного задания (в Coq) в контрольной работе 1 при условии выполнения всех остальных заданий контрольной №1.

Для получения одного балла необходимо в лабораторной № 5 решить задания всего подраздела More Basic Tactics    (Tactics)

Балл №7: 

Для получения одного балла необходимо в лабораторной № 6 решить задания всего подраздела Logic in Coq    (Logic)

Балл №8: 

Для получения одного балла необходимо в лабораторной № 8 решить из подраздела  Inductively Defined Propositions    (IndProp) не только задания с ОДНОЙ и ДВУМЯ звездами, но и все задания с ТРЕМЯ звездами до раздела Case Study: Improving Reflection.

Балл №9:

Решение дополнительного задания (в Coq) в контрольной работе 1 при условии выполнения всех остальных заданий контрольной № 2.

Балл №10:

Решение дополнительного задания (в Coq) в контрольной работе 1 при условии выполнения всех остальных заданий контрольной №3.