(** * Discrimination forte et inversion *)

(** ** Contexte *)

(** On reprend la relation coulsuiv sur les couleurs *)
Inductive coul : Set :=
| violet : coul
| indigo : coul
| bleu : coul
| vert : coul
| jaune : coul
| orange : coul
| rouge : coul
.

Inductive coulsuiv : coul -> coul -> Prop :=
| CSv : coulsuiv vert orange
| CSo : coulsuiv orange rouge
| CSr : coulsuiv rouge vert
.

(* ====================================================================== *)
(** ** Discrimination *)

(** Déjà vu : égalités contagieuses *)
Lemma discrim_vert_orange :
  vert = orange -> forall {X: Set}, forall x y: X, x = y.
Proof.
  intros e X x y.
  pose (f c := match c with vert => x | _  => y end).
  change x with (f vert). rewrite e. cbn. reflexivity.
Qed.

(** Égalités super-contagieuses.
    On peut même aller plus loin, c'est à dire prouver
    n'importe quoi à partir d'une telle égalité
    Idée : rewrite non plus sur une valeur, mais sur une
    proposition.
    En l'occurence on va remplacer P par une proposition
    prouvée. Ici on prend l'hypothèse e, mais
    on pourrait aussi prendre 0 = 0.
    Remarque :
    changement d'"étage" dans l'immeuble des valeurs et des types.
    On a déjà utilisé cela pour la fonction ouf_ouf, avec Set au lieu
    de Prop.
 *)
(** Attention, ici on considère rouge = orange *)
Lemma discrim_rouge_orange_fort :
  rouge = orange -> forall P: Prop, P.
Proof.
  intros e P.
  pose (f c := match c with rouge => P | _  => rouge = orange end).
  change (f rouge). rewrite e. cbv. exact e.
Qed.

(** Variante avec 0 = 0 *)
Lemma discrim_rouge_orange_fort_utilisant_0_egal_0 :
  rouge = orange -> forall P: Prop, P.
Proof.
  intros e P.
  pose (f c := match c with rouge => P | _  => 0 = 0 end).
  change (f rouge). rewrite e. cbv. reflexivity.
Qed.

(** **** Tactique discriminate *)
(** Coq possède la tactique discriminate, basée sur un code semblable. *)
Lemma discrim_rouge_orange_fort_avec_discriminate :
  rouge = orange -> forall P: Prop, P.
Proof.
  intros e P. discriminate e.
Qed.

(** La tactique discriminate fonctionne dès que l'on a en hypothèse
    une égalité entre des expressions commençant par des constructeurs
    différents *)

(* ====================================================================== *)
(** ** Inversion *)

(** *** Les finesses cachées de destruct *)

(** **** Tactique revert *)
(** **** Combinateur de tactiques try *)
(** On commence par le lemme suivant *)
Lemma rouge_suit_orange :
  forall c1 c2 : coul, c1 = orange -> coulsuiv c1 c2 -> c2 = rouge.
  intros c1 c2 e1 cs.

  (** Étape 1 : raisonner par cas sur cs *)
  (** Cela va donner pour c1 et c2, respectivement
      - vert et orange,
      - orange et rouge,
      - rouge et vert.
      On observe que c1 est utilisé dans e1. Pour clarifier ce qui se passe,
      il est bon de remettre e1 dans la partie conclusion.
      Pour cela on effectue un "intro à l'envers",
      soit au moyen d'un refine approprie... *)
  refine ( (_ : c1 = orange -> c2 = rouge) e1); clear e1.
  Undo 1.
  (** ... soit au moyen de la tactique revert, qui effectue ce refine *)
  revert e1.

  (** L'égalité c1 = orange joue le rôle d'un cheval de Troie :
      l'analyse pas cas de cs fait entrer une information utile
      dans les sous-buts correspondant aux sous-cas. *)

  (** Pour bien comprendre le raisonnement par cas sur cs,
      on utilise refine (suivi de clear, facultatif).
      Par exemple dans le premier cas, c1 et c2 sont respectivement
      vert et orange, ce qu'on peut expliciter dans le script. *)
  refine (match cs with
          | CSv => _ : vert = orange -> orange = rouge
          | CSo => _
          | CSr => _
          end); clear.
  (** Il faut faire un intro e1 dans chaque cas, on va factoriser... *)
  Undo 1.
  (** ... et utiliser destruct, équivalent ici au match mais plus court *)
  destruct cs as [ | | ]; intro e1.

  (** En fait, la tactique destruct fait plus de travail :
      - recherche des hypothèses touchées par cs
      - revert de ces hypothèses
      - refine (match ... end),      C'EST LE COEUR
        suivi de clear
      - réintroduction des hypothèses provenant des revert
      Au total, toutes les subtilités logiques de l'étape 1 sont prises
      en compte dans une seule invocation de destruct !
 *)
  Undo 2.
  destruct cs as [ | | ].

  (** Étape 2 : résolution par discrimination et réflexivité *)
  - (* Égalité contagieuse habituelle *)
    rewrite (discrim_vert_orange e1 orange rouge). reflexivity.
  - reflexivity.
  - (* Égalité contagieuse "forte" *)
    apply (discrim_rouge_orange_fort e1).
    (** Ou bien avec la tactique discriminate *)
    Undo 1.
    discriminate e1.

  (** Résumons le tout par un script très court ;
      noter l'utilisation de try pour gérer tous les cas contagieux,
      ne laissant que le cas pertinent où c1 est rouge. *)
  Restart.

  intros c1 c2 e1 cs.
  destruct cs as [ | | ]; try discriminate e1.
  reflexivity.
Qed.


(** Enseignements tirés de ce qui précède
- on pourra désormais se débarrasser des buts "absurdes"
  du fait d'une égalité contagieuse en hypothèse au moyen de
  discriminate (ou mieux : try discriminate) ;
- le travail effectué par destruct est remarquable ;
  une preuve effectuée à la main explicitant bien
  toutes les étapes devrait montrer tous ces détails !
  en pratique, beaucoup de mathématiques sont écrites ;
- à savoir : le travail effectué par induction est semblable ;
- on a vu que cela était parfois néfaste, il est parfois
  indispensable de nettoyer préalablement un but avec clear
  pour éviter que des hypothèses parasites soient embarquées
  colatéralement dans les hypothèses de récurrence.
 *)

(** Après cette bonne nouvelle sur destruct, on pourrait croire
    que destruct marche comme désiré à tous les coups.
    Voici pourtant une tentative qui échoue.
    On va essayer de démontrer une variante du lemme ci-dessus,
    exprimée sans le truchement de c1 = orange. *)
(** On revient à rouge_suit_orange *)

Theorem rouge_suit_orange_court :
  forall c2, coulsuiv orange c2 -> c2 = rouge.
Proof.
  intros c2 cs.
  destruct cs as [ | | ].
  (** On n'a aucun moyen de continuer. *)
Abort.

(** Pour comprendre commençons par une observation préliminaire.
    On définit deux fonctions sur les entiers naturels.
 *)

Definition fonc1 (n : nat) :=
  match n with
  | O => vert
  | S p => rouge
  end.

Definition fonc2 (n : nat) :=
  match n with
  | O => orange
  | S p => vert
  end.

(** Et on démontre le lemme suivant *)
Example prelim_destruct :
  forall n m, coulsuiv (fonc1 (n+3*m)) (fonc2 (n+3*m)).
Proof.
  intros n m.
  (** On raisonne par cas sur l'expression (n+3*m), qui est
      - soit 0
      - soit S p  *)
  refine (match n+3*m with O => _ | S p => _ end). Undo 1.
  destruct (n+3*m) as [ | p].
  - cbv. apply CSv.
  - cbv. apply CSr.
Qed.

(** Le point à remarquer est que l'analyse par cas a eté effectuée
    sans tenir compte du fait qu'à l'origine, O ou (S p) était (n+3*m).
    On le voit car c'est un destruct simple qui s'écrit aussi bien
    avec un refine-match :
    refine (match n+3*m with O => _ | S p => _ end).
    L'identité entre (n+3*m) et O (ou S p) disparaît naturellement. *)

(** Et si l'expression est en réalité un constructeur ou une constante  ? *)
Example prelim_destruct_zero :
  coulsuiv (fonc1 0) (fonc2 0).
Proof.
  cbv. apply CSv.
  (** Mais, JUSTE A DES FINS D'OBSERVATION, on peut aussi raisonner
      par cas ; destruct (et le match sous-jacent) fonctionne exactement
      comme pour prelim_destruct *)
  Undo 2.
  destruct O as [ | p].
  - cbv. apply CSv.
  - cbv. apply CSr.
Qed.

(** On revient à rouge_suit_orange *)
Theorem rouge_suit_orange_court :
  forall c2, coulsuiv orange c2 -> c2 = rouge.
Proof.
  intros c2 cs.
  destruct cs as [ | | ].
  (** On n'a aucun moyen de continuer. *)
  Undo 1.
  (*  En fait le (match cs ... end) sous-jacent se contente
      d'identifier les 2 arguments de cs à respectivement :
      - vert et orange,
      - orange et rouge,
      - rouge et vert,
      et ce même si l'un de ces arguments est déjà orange,
      En fait, même si cela contrarie nos désirs, c'est NORMAL !
      C'est cohérent avec le comportement illustré sur
      prelim_destruct_zero.
   *)
  (** Pour revenir à destruct cs, il s'avère donc necessaire de
      "libérer" explicitement l'argument fixé à orange,
      intuitivement, de détacher cette information pour la placer
      dans un cheval de Troie.
      Autrement dit, se ramener à la situation du lemme rouge_suit_orange.
      Pour cela on va se donner un lemme souvenir. *)
Abort.

(** Un lemme qui va servir à introduire ledit cheval de Troie, i.e.,
    une nouvelle variable égale à orange. *)
Lemma souvenir_orange :
  forall (P : coul -> Prop),
    (forall c, c = orange -> P c) -> P orange.
Proof.
  intros P aj_eg.
  apply aj_eg.
  reflexivity.
Qed.

(** Version générale *)
Lemma souvenir :
  forall {X: Set} (y : X) (P : X -> Prop),
    (forall x, x = y -> P x) -> P y.
Proof.
  intros X y P aj_eg.
  apply aj_eg.
  reflexivity.
Qed.

(** Remarque.
    Dans certaines situations on souhaite effectuer une analyse par
    cas sur une expression tout en conservant l'expression d'origine.
    C'est utile notamment dans un des exercices sur la sémantique
    naturelle des langages WHILE et REPEAT.
    On considère ici l'expression (n+3*m) vue plus haut.
 *)
(** **** Tactique case_eq *)
(** **** Tactique pattern *)
Example prelim_destruct_souvenir :
  forall n m, coulsuiv (fonc1 (n+3*m)) (fonc2 (n+3*m)).
Proof.
  intros n m.
  (** La tactique case_eq donne les cas possibles de l'expression
      en argument, en conservant un égalité, introduite en suite
      sous le nom e. *)
  case_eq (n+3*m).
  - intros e. admit.
  - intros p e. admit.
  Undo 7.
  (** On peut obtenir le même effet au moyen du lemme souvenir. *)
  (** D'abord remplacer (n+3*m) par une variableb n3m,
      accompagnée d'une égalité e : n3m = n + 3*m.  *)
  (** Pour cela faire apparaître la propriété P *)
  change ((fun n3m : nat => coulsuiv (fonc1 n3m) (fonc2 n3m)) (n + 3 * m)).
  (** Remarque : ceci est aussi effectué par
      la tactique de conversion [pattern] *)
  Undo 1.
  pattern (n + 3 * m).
  apply souvenir. intros n3m e.
  destruct n3m as [ | p]; cbv.
  - apply CSv.
  - apply CSr.
Qed.

(** Utilisation de pattern et souvenir sur (coulsuiv orange c2) *)
Theorem rouge_suit_orange_court :
  forall c2, coulsuiv orange c2 -> c2 = rouge.
Proof.
  intro c2.
  (** Étape 1 : remplacer orange par une variable c1,
      accompagnée d'une égalité e1 : c1 = orange. *)
  pattern orange. apply souvenir. intros c1 e1 cs.

  (** Étape 2 : on procède comme vu dans rouge_suit_orange *)
  destruct cs as [ | | ]; try discriminate e1.
  reflexivity.
Qed.

(** Il est crucial d'observer que l'hypothèse (cs : coulsuiv orange c2)
    pose DEUX contraintes simultanées :
    - l'arbre de preuve évoqué par cs est a priori de l'une des
      trois formes indiquées par les constructeurs CSv, CSo et CSr
      (ce qui entraîne que les arguments considérés de coulsuiv
      sont respectivement soit vert et orange, soit orange et rouge,
      soit rouge et vert) ;
    - le premier argument de coulsuiv est en fait orange ;
      or, ici, le premier argument de CSv, CSo et CSr est toujours
      un constructeur (c'est vrai aussi du second argument mais cela
      n'intervient pas ici).
    C'est la combinaison de ces deux contraintes qui, au final, restreint
    le nombre de cas vraiment possibles pour cs à un seul, Cso, car les
    les autres reviennent à égaliser orange avec vert ou avec rouge,
    ce qui est "absurde" (aussi absurde que true = false ou 1 = 0).
    Mais pour faire valoir cela, avec un destruct cs, il faut préparer
    le terrain avec le lemme souvenir puis nettoyer les cas non désirés
    avec discriminate.

    La combinaison hypothèse dans un type inductif + argument
    fixé décrit par un constructeur est fréquente.
    Pour faciliter son traitement Coq comporte la tactique inversion,
    qui effectue un travail équivalent à ce qui vient d'être décrit.
    Illustrons la sur l'exemple précédent.
*)

(** **** Tactique inversion *)
Theorem rouge_suit_orange_court_avec_inversion :
  forall c2, coulsuiv orange c2 -> c2 = rouge.
Proof.
  intros c2 cs. inversion cs. reflexivity.
Qed.

(* ---------------------------------------------------------------------- *)
(** **** Et pour une couleur sans suivant ? *)

(** Si une couleur suit violet, c'est la fête. *)
Theorem rien_ne_suit_violet :
  forall c2, coulsuiv violet c2 -> forall P: Prop, P.
Proof.
  intros c2 cs P.
  (** La tactique inversion rend le résultat immédiatement. *)
  inversion cs.
  (** Mais essayons de comprendre pourquoi, par la technique précédente. *)
  Undo 1.
  revert cs. pattern violet. apply souvenir. intros c1 e1 cs.
  (** Les dans les trois cas prévus pour cs, c1 vaut vert, orange ou rouge ;
      l'égalité e1 devient super-contagieuse et les sous-buts se résolvent
      par discriminate. *)
  destruct cs as [ | | ].
  - discriminate.
  - discriminate.
  - discriminate.
Qed.

(* ---------------------------------------------------------------------- *)
(** Illustration sur un exemple plus intéressant *)
(** **** Tactique subst *)
Theorem coulsuiv3 :
  forall c1 c2 c3 c4,
    coulsuiv c1 c2 ->
    coulsuiv c2 c3 ->
    coulsuiv c3 c4 ->
    c4 = c1.
Proof.
  intros c1 c2 c3 c4 cs1 cs2 cs3.
  destruct cs1 as [ | | ].
  - inversion cs2.
    (** La tactique inversion a tendance à introduire des égalités
        qu'il est souvent préférable d'utiliser systématiquement pour
        nettoyer le but. On utilise la tactque subst à cet effet. *)
    subst.
    inversion cs3.
    reflexivity.
  - (** Il apparaît que tous les sous-buts se résolvent de la même
        manière, on va donc tout faire en une seule fois. *)
  Restart.

  intros c1 c2 c3 c4 cs1 cs2 cs3.
  destruct cs1 as [ | | ];
  inversion cs2; subst; inversion cs3; reflexivity.
Qed.

(* ====================================================================== *)
(** * Une autre façon d'effectuer l'inversion *)

(** Nous avons vu une manière explicite d'effectuer des inversions
    au moyen du lemme souvenir et d'usages répétés de discriminate.
    Chacun de ces usages de discriminate contient, de façon sous-jacente,
    une analyse par cas sur "l'argument pilote" c1 de
    cs : coulsuiv c1 c2.
    On propose ici un procédé plus élégant, qui effectue cette
    analyse une seule fois.
    Comme pour discrim_rouge_orange_fort, on va calculer une proposition
    pour chaque constructeur (couleur) ; ou plutôt un prédicat à un
    argument, correspondant à ce que donne la relation coulsuiv
    lorsque son "argument pilote" est fixé à une couleur donnée.

    On repart au début pour avoir tout sous les yeux.
 *)

Reset coulsuiv.

Inductive coulsuiv : coul -> coul -> Prop :=
| CSv : coulsuiv vert orange
| CSo : coulsuiv orange rouge
| CSr : coulsuiv rouge vert
.

(** Les prédicats obtenus en fixant l'argument pilote. *)
Inductive coulsuiv_vert : coul -> Prop :=
| CSv' : coulsuiv_vert orange.

Inductive coulsuiv_orange : coul -> Prop :=
| CSo' : coulsuiv_orange rouge.

Inductive coulsuiv_rouge : coul -> Prop :=
| CSr' : coulsuiv_rouge vert.

(** Pour les couleurs restantes il n'y a aucun constructeur. *)
Inductive coulsuiv_autre : coul -> Prop := .

(** Pour chaque couleur pilote on rend un des prédicats ci-dessus. *)
Definition dispatch (c: coul) : coul -> Prop :=
  match c with
  | vert => coulsuiv_vert
  | orange => coulsuiv_orange
  | rouge => coulsuiv_rouge
  | _ => coulsuiv_autre
  end.

(** Si on a (cs : coulsuiv c1 c2) en hypothèse, on en déduit
    le prédicat associé qui sera, suivant c1, soit coulsuiv_vert,
    soit coulsuiv_orange, etc.  *)
Definition coulsuiv_inv {c1 c2} (cs : coulsuiv c1 c2) : dispatch c1 c2 :=
  match cs with
  | CSv => CSv'
  | CSo => CSo'
  | CSr => CSr'
  end.

(** Utilisation : pour "inverser" une hypothèse telle que
    cs : coulsuiv orange x, au lieu de raisonner par cas sur cs
    (on a vu l'insuffisance de destruct cs), on raisonne par cas sur
    (coulsuiv_inv cs), de type coulsuiv_vert, qui ne possède
    que le seul constructeur CSv' fabriqué sur le même modèle que CSv :
    tout se passe comme si on avait fait un destruct cs effaçant les cas
    non pertinents.
 *)

Theorem coulsuiv3_alamain :
  forall c1 c2 c3 c4,
    coulsuiv c1 c2 ->
    coulsuiv c2 c3 ->
    coulsuiv c3 c4 ->
    c4 = c1.
Proof.
  intros c1 c2 c3 c4 cs1 cs2 cs3.
  (** Il y a 3 cas pour cs1 *)
  destruct cs1 as [ | | ].
  - Check (coulsuiv_inv cs2 : coulsuiv_orange c3).
    (** Remarquer que ce procédé n'engendre aucune égalité parasite :
        la seule preuve possible de coulsuiv_orange c3 impose
        que c3 soit rouge, ce qui est répercuté dans le nouveau obtenu *)
    destruct (coulsuiv_inv cs2).
    (** Idem sur cs3 qui impose, via coulsuiv_inv, que c4 soit vert *)
    destruct (coulsuiv_inv cs3).
    reflexivity.
    (** On recommence avec des tactiques systématiques. *)
    Restart.

  intros c1 c2 c3 c4 cs1 cs2 cs3.
  destruct cs1 as [ | | ];
  destruct (coulsuiv_inv cs2);
  destruct (coulsuiv_inv cs3);
  reflexivity.
Qed.

(** Pour le cas de violet, (coulsuiv_inv cs) est de type (coulsuiv_autre c2)
    qui n'a aucun constructeur ; dans l'analyse par cas, il y a donc 0 cas
    à considérer, autrement dit aucun sous-but : la résultion est immédiate,
    sans passer par des discriminate. *)
Theorem rien_ne_suit_violet :
  forall c2, coulsuiv violet c2 -> forall P: Prop, P.
Proof.
  intros c2 cs P.
  Check (coulsuiv_inv cs : coulsuiv_autre c2).
  (** Or violet n'a pas de suivant : le match comporte zéro cas. *)
  destruct (coulsuiv_inv cs).
  (** On le voit particulièrement bien avec un match explicite *)
  Undo 1.
  refine (match coulsuiv_inv cs with end).
Qed.

(* ------------------------------------------------------------------ *)
(** Exemple plus complexe *)
Reset coulsuiv.

(** On indique, en plus, que :
    - bleu est suivi par indigo,
    - indigo est suivi par violet,
    - indigo est également suivi toute couleur qui à la fois
      suit jaune et est égale à rouge,
    - jaune est suivi par jaune.
    (Ici, comme auparavant,
     aucune couleur ne suit violet).


  bleu --> indigo --> violet
                  \
                   +--> c   tq  jaune --> c  et  c = rouge
                        (donc branche morte)

  jaune --> jaune

  vert --> orange --> rouge +
   ^                       /
    \---------<-----------+

 *)

Inductive coulsuiv : coul -> coul -> Prop :=
| CSb  : coulsuiv bleu indigo
| CSi1 : coulsuiv indigo violet
| CSi2 : forall c, coulsuiv jaune c -> c = rouge -> coulsuiv indigo c
| CSj  : coulsuiv jaune jaune
| CSv  : coulsuiv vert orange
| CSo  : coulsuiv orange rouge
| CSr  : coulsuiv rouge vert
.

(* --------------------------- *)
(** Préparation des inversions *)

(** Les prédicats obtenus en fixant l'argument pilote. *)
(** Il y a donc pour indigo deux clauses *)
Inductive coulsuiv_bleu : coul -> Prop :=
| CSb'  : coulsuiv_bleu indigo.

Inductive coulsuiv_indigo : coul -> Prop :=
| CSi1' : coulsuiv_indigo violet
| CSi2' : forall c, coulsuiv jaune c -> c = rouge -> coulsuiv_indigo c.

Inductive coulsuiv_jaune : coul -> Prop :=
| CSj'  : coulsuiv_jaune jaune.

Inductive coulsuiv_vert : coul -> Prop :=
| CSv' : coulsuiv_vert orange.

Inductive coulsuiv_orange : coul -> Prop :=
| CSo' : coulsuiv_orange rouge.

Inductive coulsuiv_rouge : coul -> Prop :=
| CSr' : coulsuiv_rouge vert.

(** Pour la couleur restante il n'y a aucun constructeur. *)
Inductive coulsuiv_violet : coul -> Prop := .

(** Pour chaque couleur pilote on rend un des prédicats ci-dessus. *)
Definition dispatch (c: coul) : coul -> Prop :=
  match c with
  | indigo => coulsuiv_indigo
  | bleu => coulsuiv_bleu
  | jaune => coulsuiv_jaune
  | vert => coulsuiv_vert
  | orange => coulsuiv_orange
  | rouge => coulsuiv_rouge
  | violet => coulsuiv_violet
  end.

(** Si on a (cs : coulsuiv c1 c2) en hypothèse, on en déduit
    le prédicat associé qui sera, suivant c1, soit coulsuiv_vert,
    soit coulsuiv_orange, etc.  *)
Definition coulsuiv_inv {c1 c2} (cs : coulsuiv c1 c2) : dispatch c1 c2 :=
  match cs with
  | CSb => CSb'
  | CSi1 => CSi1'
  | CSi2 c cs e => CSi2' c cs e
  | CSj => CSj'
  | CSv => CSv'
  | CSo => CSo'
  | CSr => CSr'
  end.

(* --------------------------- *)

(** Le théorème coulsuiv3_alamain est toujours démontrable,
    mais avec plus de cas à considérer. *)

Theorem coulsuiv3_alamain :
  forall c1 c2 c3 c4,
    coulsuiv c1 c2 ->
    coulsuiv c2 c3 ->
    coulsuiv c3 c4 ->
    c4 = c1.
Proof.
  intros c1 c2 c3 c4 cs1 cs2 cs3.
  destruct cs1 as [ | | c cs1' e1 | | | | ].
  - (** Ici l'argument pilote de cs2 est indigo, la couleur
        qui suit bleu, selon l'hypothèse cs1 *)
    Check (coulsuiv_inv cs2 : coulsuiv_indigo c3).
    (** Une preuve de (coulsuiv_indigo c3) fournit à son tour 2 cas ;
        - CSi1', qui impose que c4 soit violet
        - CSi2', qui impose que c4 soit une couleur c,
          respectant (coulsuiv violet c) *)
    destruct (coulsuiv_inv cs2) as [ | c cs2' e2].
    + (** Ici l'argument pilote de cs3 est violet, la première couleur
          qui peut suivre bleu, selon l'hypothèse cs2 *)
      (** Or violet n'a pas de suivant : le match comporte zéro cas. *)
      destruct (coulsuiv_inv cs3) as [].
    + (** Observer le remplacement de c par jaune dans tout le contexte *)
      destruct (coulsuiv_inv cs2') as [cs2'].
      (** L'égalité e2 est devenue super-contagieuse. *)
      discriminate e2.
  - (** Encore une violette  *)
    destruct (coulsuiv_inv cs2) as [].
  - destruct (coulsuiv_inv cs1'). discriminate e1.
  - (** jaune est suivi par jaune, deux fois *)
    destruct (coulsuiv_inv cs2). destruct (coulsuiv_inv cs3). reflexivity.
  - destruct (coulsuiv_inv cs2); destruct (coulsuiv_inv cs3); reflexivity.
  - destruct (coulsuiv_inv cs2); destruct (coulsuiv_inv cs3); reflexivity.
  - destruct (coulsuiv_inv cs2); destruct (coulsuiv_inv cs3); reflexivity.
Qed.

(** On recommence avec des tactiques systématiques. *)
Reset coulsuiv3_alamain.
Theorem coulsuiv3_alamain :
  forall c1 c2 c3 c4,
    coulsuiv c1 c2 ->
    coulsuiv c2 c3 ->
    coulsuiv c3 c4 ->
    c4 = c1.
Proof.
  intros c1 c2 c3 c4 cs1 cs2 cs3.
  destruct cs1 as [ | | c cs1' e1 | | | | ];
    try (destruct (coulsuiv_inv cs2); destruct (coulsuiv_inv cs3); reflexivity).
  - destruct (coulsuiv_inv cs2) as [ | c cs2' e2].
    + destruct (coulsuiv_inv cs3) as [].
    + destruct (coulsuiv_inv cs2') as [cs2']. discriminate e2.
  - destruct (coulsuiv_inv cs1'). discriminate e1.
Qed.


(* ====================================================================== *)
(** Pour un exemple plus fourni : voir l'inversion explicite
    de SN dans cours07_SN.v *)

(** *** Le pour et le contre *)
(**
 La tactique inversion est très pratique car ne demande aucun travail
   préparatoire
 - elle introduit des hypothèses dont les noms sont difficiles à
   contrôler, ce qui est ennuyeux pour la robustesse des scripts
 - certaines de ces hypothèses sont des égalités qu'il convient
   d'éliminer immédiatenent avec subst ; mais pour des prédicats
   plus complexes que coulsuiv (comportant des composantes),
   on aura des hypothèses nommées H3, H28...
   et ces noms dépendent de l'algorithme de nommage de la version
   de Coq utilisée.

 À l'inverse, la technique d'inversion explicite présentée ici
   demande un travail préparatoire non trivial (à l'instar de
   coulsuiv_vert, CSv', etc.)
 - il n'y a aucune "magie noire", on se ramène à un seul match
   (celui de dispatch) plus celui correspondant ;
 - le comportement est prédictible et on peut facilement
   nommer les hypothèses créées ;
 - accessoirement, en interne (Show Proof), les preuves sont
   bien plus petites.


CONCLUSION pour LT :
 - par défaut, utiliser inversion ;
 - si on vous fournit les definitions préparatoires ad-hoc
   (exemple : pour SN), il est possible de les utiliser aussi ;
 - pour ceux qui aiment le sport, définir et utiliser des inversions
   explicites sera un GROS bonus. Facultatif évidemment.
*)