Library coq9_inversion

Discrimination forte et inversion

Contexte

On reprend la relation coulsuiv sur les couleurs

Discrimination

Déjà vu : égalités contagieuses

Lemma discrim_vert_orange :
  vert = orange → ∀ {X: Set}, ∀ 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 → ∀ 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 → ∀ 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 → ∀ 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 :
∀ 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é

  -
    rewrite (discrim_vert_orange e1 orange rouge). reflexivity.
  - reflexivity.
  -
    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 :
  ∀ 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 :
∀ 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 :
  ∀ c2, coulsuiv orange c2 → c2 = rouge.
Proof.
  intros c2 cs.
  destruct cs as [ | | ].

On n'a aucun moyen de continuer.

Undo 1.

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 :
  ∀ (P : coul → Prop),
    (∀ c, c = orange → P c ) → P orange.
Proof.
  intros P aj_eg.
  apply aj_eg.
  reflexivity.
Qed.

Version générale

Lemma souvenir :
  ∀ {X: Set} (y : X) (P : X → Prop),
    (∀ 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 :
∀ 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 :
∀ 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 :
∀ 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 :
∀ c2, coulsuiv violet c2 → ∀ 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 :
  ∀ 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 :
  ∀ 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 :
  ∀ c2, coulsuiv violet c2 → ∀ 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 + ^ / \---------<-----------+

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' : ∀ 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.

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 :
  ∀ 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 :
  ∀ 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.