Instalați Coq urmând instrucțiunile de aici: https://coq.inria.fr/. Dacă
întâmpinați probleme, cereți ajutorului profesorului de laborator.
Exerciții
de antrenament (se rezolvă împreună cu profesorul de laborator):
Definiți un tip de date algebric pentru zilele săptămânii.
Definiți o funcție de egalitate peste acest tip de date.
Exerciții propuse:
Definiți o funcție care returnează ziua următoare. (1 punct)
Definiți tipul de date boolean. (1 punct)
Definiți funcțiile: negație, conjuncție, disjuncție peste tipul de
date boolean definit la exercițiul precedent. (2 puncte)
Bonus
Definiți un tip de date care simulează numere naturale
reprezentate pe 8 biți. Pentru acest tip de date scrieți funcții
pentru adunare, scădere, înmulțire, împărțire întreagă și restul
împărțirii (modulo). Identificați pentru fiecare funcție cazurile de
excepție (de exemplu, scăderi care dau valori negative, împărțiri la
zero) și stabiliți niște convenții pentru acele cazuri (de exemplu,
pot sa returnez mereu zero atunci când o scădere returnează o valoare
negativă). (5 puncte)
