Laboratorium z systemu Coq

System Coq wraz z dokumentacja dostepny jest pod adresem http://coq.inria.fr
(dla korzystających z Coq'a pod Fedorą: coq z rpm'a po 1 nocy przestaje dzialac :) Słowem kluczowym jest "prelink". Aby obejść problem, nalezy przeczytac to.

Zaliczenie

Aby zaliczyć laboratorium z Coqa należy zrobić (przynajmniej) jedną z dwóch rzeczy:

albo zrobić do końca zadanie 7, w szczególności zrealizować taktykę dowodzenia tautologii intuicjonistycznych przez refleksję,
albo dowieść twierdzenie Zeckendorfa o tym, że każda liczba naturalna może być przedstawiona w jednoznaczny sposób jako suma różnych niekolejnych liczb Fibonacciego.

Pierwszy temat to typowe ćwiczenie z Coqa, po tylu tygodniach walki z ćwiczeniem 6 nie powinno nikomu sprawić zbyt dużych kłopotów. Ewentualnie prosze sobie zalozyc poprawnosc reguly ciecia dla systemu Gentzena.
Drugi temat jest niewątpliwie większym wyzwaniem. Jestem prawie pewien, że twierdzenia Zeckendorfa nikt jeszcze w Coqu nie sformalizował. Jeśli komuś się ten temat spodoba, to na pewno można zrobić z niego temat pracy magisterskiej.

Termin wykonania zadania: 30 czerwca 2006

Egzamin

Egzamin odbył się we wtorek 27 czerwca.
Treść zadań
Rozwiązanie zadania 4:

punkt 1 (eq_subst + eq_unique -> eq_elim)
punkt 2 (JMeq_elim -> JMeq_subst + JMeq_unique)
punkt 3 (JMeq -> eq)
punkt 4 (eq -> JMeq)

Zadanie to zostało napisane po lekturze doktoratu Conora McBride'a (Rozdział 5). A oto komentarz autora, tłumaczący nazwę równości:

It is now time to reveal the deﬁnition of , the ‘John Major’ equality relation (footnote:
John Major was the last ever leader of the Conservative Party to be Prime Minister
(1990 to 1997) of the United Kingdom, in case he has slipped your mind). John
Major’s ‘classless society’ widened people’s aspirations to equality, but also the gap
between rich and poor. After all, aspiring to be equal to others than oneself is the
politics of envy. In much the same way, forms equations between members of any
type, but they cannot be treated as equals (ie substituted) unless they are of the same
type. Just as before, each thing is only equal to itself.

Laboratorium z systemu Coq

1. Zapoznanie sie z systemem, podstawowe komendy, taktyki...

2. Wstep do definicji indukcyjnych

3. Definicje indukcyjne (c.d.)

4. Definicje indukcyjne - dowodzenie przez indukcje

5. Szachownica

6. Intuicjonistyczna logika zdaniowa

7. Intuicjonistyczna logika zdaniowa (ciag dalszy)

Zaliczenie

Egzamin