(*****************************************************************************)
(*                                                                           *)
(*                   Arithmétique: preuves d'algorithmes.                    *)
(*                                                                           *)
(*****************************************************************************)

Section Arithmetique.

(*                                                                              
 L'ensemble Nat des entiers de Peano.                                           
                                                                                
 C'est un ensemble qu'on définit par récurrence.                                
 Il est constitué d'une constante, o, et de ses successeurs, obtenus par        
 la fonction s: Nat={o, (s o), (s (s o)), ...}                                  
                                                                                
*)                                                                              

Inductive Nat : Set := o | s (n : Nat).

Check (s (s o)).
Check Nat.

(*                                                                              
  C'est exactement l'ensemble des termes  construits avec la signature {o,s}.   
                                                                                
  Une première propriété facile:                                                
*)                                                                              

Lemma tout_entier_a_un_successeur : forall n : Nat, exists m : Nat, m = s n.

(*                                                                              
 L'ensemble Nat est défini par récurrence, aussi on va pouvoir faire            
 de démonstrations par cas (destruct) ou par récurrence (induction)
 des propriétés de ses éléments.               
 Un premier exemple de démonstration :                            
*)                                                                              

Lemma tout_entier_est_soit_0_soit_a_un_predecesseur :
 forall n : Nat, n = o \/ (exists m : Nat, n = s m).

(*                                                                              
 La structure récursive de Nat permet aussi de définir des fonctions par        
 récurrence, i.e. des fonctions récursives.                                     
                                                                                
 Définissons par exemple la fonction "double" qui à x associe 2x:               
 si x=o, (double x)=o                                                           
 si x=(s n), (double x) = (s (s (double n)))                                    
*)                                                                              

Fixpoint double (n : Nat) : Nat :=
  match n with o => o | s n1 => s (s (double n1)) end.

(*                                                                              
 La construction "Fixpoint" permet de définir des fonctions récursives.         
                                                                                
 "double (n:Nat) : Nat" signifie qu'on définit une fonction nommée "double"        
 définie par récurrence sur son argument n, de type Nat, et qui rend un élément 
 de Nat.                                                                        
                                                                                
 "match n with ... ... end" signifie que le résultat est un objet de type        
  Nat, calculé selon les valeurs possibles de n, qui sont ici données par les   
  deux formes que n peut avoir (puisque c'est un élément de Nat): soit o, soit  
 (s n1).                                                                        
                                                                                
 On donne les valeurs voulues dans chacun de ces cas à l'intérieur de cette     
 structure.                                                                     
*)                                                                              

(*                                                                              
 Cette fonction est vraiment un algorithme de calcul:                           
*)                                                                              

Eval compute in (double (s (s o))).

(*                                                                              
 Et on peut montrer qu'elle a des propriétés:                                   
*)                                                                              

Lemma double_prop1 : forall n : Nat, double (s n) = s (s (double n)).

(*                                                                              
 Définissons maintenant l'addition (en mettant en commentaire des               
 indications sur les cas traités, pour la compréhension de la définition).      
 C'est une définition par récurrence sur son second argument:                   
*)                                                                              

Fixpoint add (n m : Nat) {struct m} : Nat :=
  match m with
  | o => n
  | s m1 => s (add n m1)
  end.

Eval compute in (add (s (s o)) (s o)).

(*                                                                              
 Montrons maintenant quelques propriétés de l'addition.                         
*)                                                                              

Lemma add_o_neutre_a_droite : forall n : Nat, add n o = n.

Lemma add_o_neutre_a_gauche : forall n : Nat, add o n = n.

(*                                                                              
 Dans le lemme suivant, on peut faire une récurrence sur n ou sur m.            
 Le bon choix est m, car l'addition est définie par récurrence sur son          
 second argument. Si on choisit n, on a du mal...                               
*)                                                                              

Lemma add_sn_m : forall n m : Nat, add (s n) m = add n (s m).

(*                                                                              
 Revenons à notre fonction double:                                              
*)                                                                              

Lemma double_add : forall n : Nat, double n = add n n.

(*                                                                              
 Montrons maintenant que notre addition est commutative:                        
*)                                                                              

Lemma add_commutative : forall n m : Nat, add n m = add m n.

(*                                                                              
 Les premiers lemmes que l'on a démontrés semblent un peu triviaux...Mais sans  
 eux, on aurait eu un mal fou à démontrer la commutativité. Du moins on se      
 serait aperçu au cours de la preuve de leur utilité!                           
                                                                                
 Maintenant l'associativité:                                                    
*)                                                                              

Lemma add_associative : forall a b c : Nat, add a (add b c) = add (add a b) c.

(*                                                                              
 La multiplication:                                                             
*)                                                                              

Fixpoint mul (n m : Nat) {struct m} : Nat :=
  match m with
  | o => o
  | s m1 => add (mul n m1) n
  end.

Check (mul (s (s (s o))) (s (s o))).

(*                                                                              
 Quelques propriétés:                                                           
*)                                                                              

Lemma mul_o_absorbant_a_droite : forall n : Nat, mul n o = o.

Lemma mul_o_absorbant_a_gauche : forall n : Nat, mul o n = o.

(*                                                                              
 La puissance:                                                                  
*)                                                                              

Fixpoint puis (n m : Nat) {struct m} : Nat :=
  match m with
  | o => s o
  | s m1 => mul (puis n m1) n
  end.

End Arithmetique.