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.