TD Preuves : Types

On commence par une structure de données définie sans récursion : les mois (ou les jours)

Inductive positive : Set :=
I : positive
| C2X : positive
| C2XP1 : positive.

Definition un : positive := I.
Definition trois : positive := C2XP1 I.
Definition quatre: positive := C2X (C2X I).
Definition sept : positive := C2XP1 (trois).

Bon, on voit comment ça mmarche. Comment définir la fonction successeur? Une fonction avec filtration sur le constructeur (récursivement)

Fixpoint Sp (p:positive) : positive :=
match p with
(C2X a) => C2XP1 a
| (C2XP1 a) => C2X (Sp a)
| I => C2X I
end.

Q.8) définir la fonction f: x→ 2*x -1. L'utiliser pour définir Pp, prédécesseur

Fixpoint f (p:positive) : positive :=
match p with
  I => I
| (C2X a) => C2XP1 (f a) (* 2*a -> 4*a-1 = 2*(2a-1)+1  *)
| (C2XP1 a) => C2X a
end.

Definition Pp (p:positive) : positive :=
I => I
| CX2 a => f a
| CX2P1 a => C2X a
end.

Inductive arbre (A:Set) : Set :=
feuille : A -> arbre A
| noeud : A -> arbre A -> arbre A -> arbre A.

Rappels des définitions des nat et list avec leurs principes d'induction

Inductive list (A:Set) Set :=
Nil : list A
|Cons : list A -> A -> list A.