(* Illustration d'une technique de preuve à connaître lorsque
   l'on a affaire à une fonction récursive avec accumulateur *)

Require Import List.

Print list.

Fixpoint long (u : list nat) : nat :=
  match u with
  | nil => 0
  | cons x u' => S (long u')
  end.

(* Version avec accumulateur *)
Fixpoint long2 (u : list nat) : nat -> nat :=
  fun a =>
    match u with
    | nil => a
    | cons x u' => long2 u' (S a)
    end.

(* On veut démontrer les théorème long2_long ci-dessous.
   Une tentative directe par récurrence sur u échoue :
   le cas où l'accumulateur vaut 0 dépend du cas où
   l'accumulateur vaut 1, et ainsi de suite.  *)

(* On commence donc par énoncer (en la devinant) une propriété
   indiquant ce que rend long2, non seulement pour toutes
   les listes u, mais aussi pour tous les accumulateurs a. *)
Lemma long2_plus : forall u a, long2 u a = long u + a.
Proof.
  intros u a.
(* ATTENTION, POINT CLÉ : à ce stade une récurrence sur u
   ne permettra pas d'effectuer la preuve, car l'accumulateur
   reste fixé à une valeur constante a (de même que dans une tentative
   directe de prouver long2_long, l'accumulateur reste fixé à 0). *)
   (* On remet a dans la propriété à démontrer par récurrence au moyen
   de la tactique revert, qui a l'effet opposé de intro. *)
  revert a.
(* Remarque dans le cas présent, il suffisait, dès le départ de n'efffectuer
   qu'une seule introduction : examiner le but courant,   puis recommencer depuis le début
   avec Undo 2, et observer qu'une seule intro donne le même but *)
  Undo 2.
  intro u.
  induction u as [ | x u' Hu'].
  (* Observer les sous-buts obtenus : ils comportent bien une quantification sur a *)
  - intro a.
    cbn [long long2]. cbn. reflexivity.
  - intro a'.
    cbn [long long2]. cbn.
    Check (Hu' (S a')).
    rewrite (Hu' (S a')).
    Check plus_n_Sm.
    Check (plus_n_Sm (long u') a').
    rewrite (plus_n_Sm (long u') a').
    reflexivity.
Qed.

(* Le théorème désiré est un simple corollaire du précédent. *)
Theorem long2_long : forall u, long2 u 0 = long u.
Proof.
  intro u.
  rewrite (long2_plus u 0). rewrite <- (plus_n_O (long u)).
  reflexivity.
Qed.

(* Remarque : dans les scripts ci-dessus on a explicité les arguments
   des lemmes d'égalité utiles, comme plus_n_O, etc.
   Rappel : en pratique, on laisse Coq les deviner (cela suffit en général),
   par exemple on écrit simplement :
   rewrite <- plus_n_O.
 *)