I'm trying to automate a decision procedure for whether an ASCII character is whitespace or not. Here is what I currently have.
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.
What would be a good approach for making the proof more concise?
Frequently, making a proof more automated involves writing a bit more code than you started with, so that you can handle more cases. Taking this approach, I adapted some boilerplate from 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.
With this boilerplate, your proof becomes
Definition IsWhitespace (c : ascii) := (c = "009"%char) \/ (c = "032"%char).
Definition isWhitespace (c : ascii) : Decidable (IsWhitespace c) := _.
which is about as short as a proof can be. (Note that := _ is the same as . Proof. exact _. Defined., which itself is the same as . Proof. typeclasses eauto. Defined..)
Note that this is fairly similar to ejgallego's proof, since tauto is the same as intuition fail.
Note also that the original boilerplate in fiat-crypto is much longer, but also more powerful than simply using hnf in *; tauto, and handles a few dozen different sorts of decidable propositions.