remplissage anciennes notes pour la seance 3

seance3.md

@@ -5,15 +5,57 @@ Programmation Fonctionnelle en Coq (seance 3)
 
 ## Types inductifs avancés
 
-Détails à venir
+#### Ordinaux
+
+On peut encoder en Coq (certains) ordinaux, via le type suivant.
 
 ```coq
 Inductive ord :=
  | zero : ord
  | succ : ord -> ord
- | lim : (nat->ord) -> 
+ | lim : (nat->ord) -> ord.
+```
+
+Noter que cet inductif satisfait bien la contrainte de strict positivité: `lim` a un argument de type `nat->ord`, où `ord` apparaît bien à droite. Par contre un `lim:(ord->nat)->ord` serait refusé par Coq.
+
+On peut plonger dans ce type les entiers naturels `nat` habituels.
+Par exemple via une addition mixte `add : ord -> nat -> ord` :
+
+```coq
+Fixpoint add a n :=
+ match n with
+ | 0 => a
+ | S n => succ (add a n)
+end.
+Definition nat2ord n := add zero n.
+```
+
+Maintenant, on peut utiliser `lim` pour aller au delà des entiers usuels.
+
+```coq
+Definition omega := lim (add zero).
+Definition deuxomega := lim (add omega).
+
+Fixpoint nomega n :=
+ match n with
+ | 0 => zero
+ | S n => lim (add (nomega n))
+ end.
+ 
+Definition omegadeux := lim nomega.
+```
+
+Attention, l'égalité standard de Coq n'est pas celle qu'on veut utiliser sur ces ordinaux. Ainsi `add zero` et `add (succ zero)` sont deux suites différentes (les entiers à partir de 0 vs. les entiers à partir de 1). Donc pour Coq on pourra prouver que `lim (add zero) <> lim (succ zero)`, alors qu'on considère normalement qu'il s'agit de deux descriptions possibles de `omega`. Il faudra alors utiliser une égalité particulière sur `ord`, en fait une relation d'équivalence (on parle aussi d'égalité sétoide).
+
+#### Arbres d'arité variable
+
+```coq
+Inductive narbre :=
+ | Node : list narbre -> narbre.
 ```
 
+Plus besoin de constructeur "feuille", on utilise `Node []` à la place.
+
 ## Fix fix
 
 La fonction d'Ackermann est-elle structurellement décroissante ?
@@ -22,10 +64,42 @@ La fonction d'Ackermann est-elle structurellement décroissante ?
  - `ack (n+1) 0 = ack n 1`
  - `ack (n+1) (m+1) = ack n (ack (n+1) m)`
 
-Détails à venir
+Non si on utilise un seul point-fixe, en effet ni `n` ni `m` (pris isolément) ne garantie une décroissance. Mais il existe une ruse (assez classique maintenant) consistant à mettre un `fix` interne dans notre `Fixpoint` :
+
+```coq
+Fixpoint ack n :=
+ match n with
+ | 0 => S
+ | S n =>
+   fix ack_Sn m :=
+   match m with
+   | 0 => ack n 1
+   | S m => ack n (ack_Sn m)
+   end
+ end.
+
+Compute ack 3 5.
+```
 
 ## Principes d'induction
 
+A chaque nouveau type inductif, `Coq` génère automatiquement des fonctions particulières nommées principes d'induction. Normalement, pour un type `foo`, on dispose alors d'une fonction `foo_rect`. Cette fonction suit la forme du type inductif pour proposer une récurrence adapté à ce type.
+
+```coq
+Check nat_rect.
+Print nat_rect.
+```
+
+Exemples de programmation sur `nat` sans `Fixpoint` ni `match`, juste avec `nat_rect`:
+
+```coq
+Definition pred n : nat := nat_rect _ 0 (fun n h => n) n.
+Definition add n m : nat := nat_rect _ m (fun _ h => S h) n.
+```
+
+Dans ces deux derniers cas, le "prédicat" donné à `nat_rect` (son premier argument `_`) est en fait `fun _ => nat`, ce qui signifie qu'on utilise `nat_rect` de manière non-dépendante.
+
+
 ## Pseudo principes d'induction
 
-Exemple de `Pos.peano_rect`
+Exemple de `Pos.peano_rect` : on détourne (manuellement) la récurrence (binaire) sur le type `positive` pour fabriquer une récurrence unaire.