战术自动化:简单的决策程序

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.

另请注意,fiat-crypto中的原始样板比单纯使用更长,但也更强大hnf in *; tauto,并处理几十种不同类型的可判定命题.