coq - 战术自动化 : simple decision procedure

Question

我正在尝试自动确定 ASCII 字符是否为空格的决策过程。这是我目前拥有的。

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.

什么是使证明更简洁的好方法？

Answer 1

通常，使证明更加自动化需要编写比开始时更多的代码，以便您可以处理更多情况。采用这种方法，我改编了来自 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.

有了这个样板，你的证明就变成了

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

这与证明一样短。 (注意 := _ 与 . Proof. exact _. Defined. 相同，后者本身与 . Proof. typeclasses eauto. Defined. 相同。)

请注意，这与 ejgallego 的证明非常相似，因为 tauto与 intuition fail 相同.

另请注意 the original boilerplate in fiat-crypto更长，但也比简单地使用 hnf in *; tauto 更强大，并处理几十种不同类型的可判定命题。