Automatisation de la tactique : procédure de décision simple

Question

J'essaie d'automatiser une procédure de décision pour savoir si un caractère ASCII est un espace blanc ou non. Voici ce que j'ai actuellement.

Require Import Ascii String.

Scheme Equality for ascii.

Definition IsWhitespace (c : ascii) := (c = "009"%char) \/ (c = "032"%char).

Definition isWhitespace (c : ascii) : {IsWhitespace c} + {not (IsWhitespace c)}.
Proof.
  unfold IsWhitespace.
  pose proof (ascii_eq_dec c "009"%char) as [H1|H1];
  pose proof (ascii_eq_dec c "032"%char) as [H2|H2];
  auto.
  right. intros [H3|H3]; auto.
Admitted.

Quelle serait une bonne approche pour rendre la preuve plus concise ?

Answer 1

Souvent, rendre une preuve plus automatisée implique d'écrire un peu plus de code qu'au départ, afin de pouvoir traiter plus de cas. En adoptant cette approche, j'ai adapté une partie du code passe-partout de fiat-crypto :

Require Import Coq.Strings.Ascii Coq.Strings.String.

Class Decidable (P : Prop) := dec : {P} + {~P}.
Arguments dec _ {_}.
Notation DecidableRel R := (forall x y, Decidable (R x y)).

Global Instance dec_or {A B} {HA : Decidable A} {HB : Decidable B} : Decidable (A \/ B).
Proof. hnf in *; tauto. Defined.
Global Instance dec_eq_ascii : DecidableRel (@eq ascii) := ascii_dec.

Avec cette phrase passe-partout, votre preuve devient

Definition IsWhitespace (c : ascii) := (c = "009"%char) \/ (c = "032"%char).
Definition isWhitespace (c : ascii) : Decidable (IsWhitespace c) := _.

ce qui est à peu près aussi court qu'une preuve puisse l'être. (Notez que := _ est la même chose que . Proof. exact _. Defined. qui est lui-même identique à . Proof. typeclasses eauto. Defined. .)

Notez que ceci est assez similaire à la preuve d'ejgallego, puisque tauto est la même chose que intuition fail .

Notez également que l'original boilerplate en fiat-crypto est beaucoup plus long, mais aussi plus puissant que la simple utilisation de l'option hnf in *; tauto et traite quelques dizaines de propositions décidables différentes.

Answer 2

Dans l'esprit de la réponse de Jason, nous pouvons bien sûr utiliser certaines bibliothèques traitant de l'égalité décidable pour arriver à votre résultat :

Cela permettra de déclarer ascii comme un type avec une égalité décidable :

From Coq Require Import Ascii String ssreflect ssrfun ssrbool.
From mathcomp Require Import eqtype ssrnat.

Lemma ascii_NK : cancel N_of_ascii ascii_of_N.
Proof. exact: ascii_N_embedding. Qed.

Definition ascii_eqMixin := CanEqMixin ascii_NK.
Canonical ascii_eqType := EqType _ ascii_eqMixin.

Dans ce style, vous déclarez généralement que vos propriétés sont des propositions décidables et qu'il n'y a donc rien à prouver :

Definition IsWhitespaceb (c : ascii) := [|| c == "009"%char | c == " "%char].

Cependant, si vous le souhaitez, vous pouvez bien sûr récupérer la partie non informatique :

Definition IsWhitespace (c : ascii) := (c = "009"%char) \/ (c = "032"%char).

Lemma whitespaceP c : reflect (IsWhitespace c) (IsWhitespaceb c).
Proof. exact: pred2P. Qed.

Il est bien sûr possible de recourir à davantage d'automatisation.

Answer 3

La preuve est presque la plus concise qui soit ! Tout au plus, ce que vous pouvez faire, c'est appeler une tactique plus puissante telle que intuition :

Definition isWhitespace (c : ascii) : {IsWhitespace c} + {not (IsWhitespace c)}.
Proof.
now unfold IsWhitespace;
    case (ascii_eq_dec c "009"%char);
    case (ascii_eq_dec c " "%char); intuition.