====== TD Preuves : Types ======

===== Sans récursion =====

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

===== Récursives =====

  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.
  
===== Arbres binaires =====

  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.