(* Éléments de correction à propos des entiers de Church *)
(* vus au premier TD                                     *)

Section EntiersDeChurch.

(* Coq est fondé sur le calcul des constructions ; il       *)
(* contient donc en particulier la lambda-calcul simplement *)
(* typé : il suffit de se restreindre au type Prop, et ne   *)
(* s'autoriser que le connecteur ->                         *)

(* On définit le type de base, que nous notons X            *)
Variable X : Prop.

Definition N0 := X -> X.
Definition N1 := (X->X)->(X->X).

(* On code les entiers par le type N1. Un élément de N1 est *)
(* une fonction qui prend en argument f:X->X et x:X et qui  *)
(* renvoie un élement de type X.                            *)
(* Essentiellement, on peut renvoyer x, ou bien n'importe   *)
(* quelle itération de f sur x. Cela permet de coder        *)
(* naturellement les entiers : l'entier n est codé par      *)
(* l'itération de f n fois.                                 *)

Definition O_ : N1 := (fun f x => x).
Definition S_ : N1 -> N1 := (fun n => (fun f x => f (n f x))).

(* On se définit quelques entiers en composant S et O :     *)
Definition I_ : N1 := S_ O_.
Definition II_ : N1 := S_ I_.
Definition III_ : N1 := S_ II_.
Definition IV_ : N1 := S_ III_.

(* On peut utiliser la tactique compute pour demander à Coq *)
(* de beta-réduire un terme. Cela nous permet de vérifier   *)
(* que 4 correspond bien à l'itération 4 fois :             *)
Eval compute in IV_.

(* L'addition et la multiplication se font naturellement :  *)
Definition addition : N1 -> N1 -> N1 :=
  fun n m => (fun f x => n f (m f x)).

(* Vérifions que 2 + 3 = 5 *)
Eval compute in addition II_ III_.

Definition multiplication : (N1 -> N1 -> N1) :=
  fun n m => (fun f x => n (m f) x).

(* Vérifions que 2*3 = 6 *)
Eval compute in multiplication II_ III_.

(* et 3*0 = 0... *)
Eval compute in multiplication III_ O_.

(* Pour faire la puissance, on aurait envie d'écrire quelque chose *)
(* comme ça : fun p n => n (multiplication p) I.                   *)
(* Le problème est que si p est de type N1,                        *)
(* (multiplication p) est de type N2 = N1->N1 et il faudrait donc  *)
(* que n soit de type N3 = (N1 -> N1) -> N1 -> N1                  *)
(* Le système F, en nous apportant le polymorphisme va nous        *)
(* permettre de résoudre ce problème.                              *)

End EntiersDeChurch.

Section EntierSystemeF.

(* Le système F correspond à Coq restreint au type Prop, avec les   *)
(* connecteurs forall et ->. Comme nous le verrons dans le deuxième *)
(* TP, nous pouvons coder toute la logique sous forme imprédicative *)
(* dand le système F. Pour l'instant, contentons-nous de coder les  *)
(* entiers, en prolongeant les idées de la première section.        *)

Definition N : Prop := forall (X:Prop), (X->X)->X->X.

Definition O : N := (fun X f x => x).
Definition S : N->N := (fun n => (fun X f x => (n X f (f x)))).

Definition I : N := S O.
Definition II : N := S I.
Definition III : N := S II.
Definition IV : N := S III.

Definition add : (N -> N -> N) :=
  fun n m => (fun X f x => n X f (m X f x)).

Definition mul : (N -> N -> N) :=
  fun n m => (fun X f x => n X (m X f) x).

Definition puissance : (N -> N -> N) :=
  fun p n => n N (mul p) (S O).

(* Vérifions que 3^2 = 9 *)
Eval compute in puissance III II.

(* et 3^0 = 1 *)
Eval compute in puissance III O.

(* et 2^1 = 2 *)
Eval compute in puissance II I.

(* Allons un peu plus loin... Nous allons montrer que la classe des    *)
(* fonctions sur les entiers écrivables en Système F est assez grande. *)
(* Pour commencer, montrons qu'on peut faire le prédecesseur.          *)

(* Pour faire le prédecesseur, il faut ruser. La solution proposée *)
(* ici n'est pas la plus concise, mais elle illustre bien l'idée   *)
(* à mettre en oeuvre :                                            *)
(* imaginons que nous sachions coder des valeurs booléennes T et F *)
(* de telle sorte que nous puissions écrire des If...Then...Else   *)
(* imaginons que nous puissions coder des couples de la forme      *)
(* (n,b) où n est entier et b un booléen.                          *)
(* Soit alors la fonction définie pour tout n par :                *)
(*    Phi(n,F) = (n,T) et Phi(n,T) = (n+1, T)                      *)
(* Alors, on a (0,F) -> (0,T) -> (1,T) -> ... -> (n,T)             *)
(* et donc, en itérant n fois Phi, on obtient un couple dont la    *)
(* première composante est le prédecesseur de n.                   *)

(* Il ne nous reste plus qu'à coder !                              *)

(* Comment coder les booléens ? Si b est un booléen, et si M et N  *)
(* sont deux termes de même type T, on veut pouvoir faire          *)
(* l'instruction "If b Then M Else N". Nous codons cette           *)
(* instruction dans b : autrement dit,                             *)
(* bMN = M si b est vrai    et    bMN = N si b est faux            *)
(* Ceci conduit naturellement aux définitions suivantes :          *)
Definition bool : Prop := forall X:Prop, X -> X -> X.
Definition T : bool := fun X x y => x.
Definition F : bool := fun X x y => y.


(* De la même façon, un couple de type N x my_bool est codé ainsi : *)
Definition couple : Prop := forall X:Prop, (N -> bool -> X) -> X.
Definition cons : N -> bool -> couple := fun n b => (fun X f => f n b).

(* Pour alléger les notations, on définit une notation infixe pour *)
(* le constructeur des couples :                                   *)
(* le couple (n,b) sera noté (n/b)                                 *)
Infix "/" := cons.

(* Les projections *)
Definition P1 : couple -> N := fun c => c N (fun n b => n).
Definition P2 : couple -> bool := fun c => c bool (fun n b => b).

Definition Phi :=
 fun c => let n := P1 c in
          let b := P2 c in  (*  c = (n,b)  *)
            b couple ((S n) / T) (n / T). (* Si b Alors (n+1,T) Sinon (n,T) *)

Definition pred : N -> N :=
 fun n => P1 (n couple Phi (O / F)).

(* et voilà : *)
Eval compute in pred (puissance II III).
Eval compute in (pred I).
Eval compute in O.

(* En fait, on peut coder n'importe quelle fonction récursive       *)
(* primitive :                                                      *)
(* de manière générale, le schéma de récurrence primitif peut être  *)
(* écrit de la façon suivante                                       *)
(* let rec f (n:N) = match n with                                   *)
(*      | 0 -> g                                                    *)
(*      | n+1 -> h (f n)                                            *)
(* Ceci donne :                                                     *)
(* Rec := fun (X :Prop) (g : X) (h : X -> X)                        *)
(*              => (f : N -> X)                                     *)

(* En dépliant la boucle de récurrence, on voit que                 *)
(*   f n = h (h (... (h g)...))                                     *)
(* ce qui est une itération n fois de la fonction h                 *)
Definition Rec : forall (X : Prop) (g : X) (h : X->X), N->X :=
  fun X g h => (fun n => n X h g).

(* En guise d'application, fournissons la factorielle :             *)
(* pour la factorielle, on a le cas n+1 -> (n+1)*(factorielle n)    *)
(* on a donc besoin de n+1 qui n'est pas donné par notre schéma.    *)
(* Qu'à cela ne tienne : on va faire une fonction f qui renvoie un  *)
(* couple d'entiers :                                               *)
(* Nous allons donc prendre f n = (factorielle n, n)                *)
(* ce qui donne n+1 -> (P1 (f n)) * ((P2 (f n))+1)                  *)

(* On code les couples d'entiers comme on avait fait pour N x bool :*)
Definition couple' : Prop := forall X:Prop, (N -> N -> X) -> X.
Definition cons' : N -> N -> couple' := fun n p => (fun X f => f n p).
Infix "/" := cons'.

Definition P1' : couple' -> N := fun c => c N (fun n b => n).
Definition P2' : couple' -> N := fun c => c N (fun n b => b).

Definition f : couple' -> couple' :=
  fun c => let fact := P1' c in
           let n := P2' c in
             mul fact (S n)  / (S n).

Definition factorielle : N -> N := fun n =>
  (* on a factorielle2 : N -> couple' *)
  (*      factorielle2(n) = (n!, n)   *)
  let factorielle2 := Rec _ (I/O) f in
    P1' (factorielle2 n).

(* et ça marche... *)
Eval compute in (factorielle III).

End EntierSystemeF.