Inductive jour : Set :=
lundi : jour | mardi : jour | mercredi : jour |
jeudi : jour | vendredi : jour | samedi : jour |
dimanche : jour.

Inductive fonction : Set :=
 fid: fonction
|fconst: R -> fonction
|fsin: fonction
|fcos: fonction
|fexp: fonction
|fplus: fonction -> fonction -> fonction
|fmoins: fonction -> fonction -> fonction
|fmult: fonction -> fonction -> fonction
|fcomp: fonction -> fonction -> fonction
.

Ensuite, pour concretiser (interpréter) les fonctions, on interprète en matchant le constructeur:

Fixpoint interp (f:fonction) (x:R) : R :=
 match f with 
|fid => x
|fconst r => r
|fsin => sin x
|fcos => cos x
|fexp => exp x
|fplus f g => (interp f x) + (interp g x)
|fmoins f g => (interp f x) - (interp g x)
|fmult f g => (interp f x) * (interp g x)
|fcomp f g => interp f (interp g x)
end.

TD Preuves : Types

Exemple donné dans l'énoncé du projet certification (sans préciser un constructeur):

Definition paire_entiers := (nat * nat)%type.

Un seul constructeur, pour faire des couples:

Require Export ZArith.
Inductive GaussInt : Set :=
c : Z ->Z-> GaussInt.

deux fonctions jour→jour

Definition jour_suivant (j:jour) : jour :=
match j with
|lundi => mardi | mardi => mercredi | mercredi => jeudi
| jeudi => vendredi | vendredi => samedi 
| samedi => dimanche | dimanche => lundi
end.

Definition jour_precedent (j:jour) : jour :=
match j with
| mardi => lundi | mercredi => mardi | jeudi => mercredi
| vendredi => jeudi | samedi => vendredi 
| dimanche => samedi | lundi => dimanche
end.