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

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

证明几乎是最简洁的了！最多只能调用更强大的战术如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.

Answer 2

通常，要使证明更加自动化，需要编写比开始时多一点的代码，这样您就可以处理更多的案例。采用这种方法，我从 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 更长，但也更强大，并且可以处理几十种不同类型的可判定命题。

Answer 3

遵循 Jason 回答的精神，我们当然可以使用一些处理可判定相等性的库来得出您的结果：

这会将 ascii 声明为具有可判定相等性的类型：

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.

在这种风格中，通常你声明你的属性是可判定的命题，所以没有什么可以证明的：

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

但是如果你愿意，你当然可以恢复非计算性的：

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

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

当然可以使用更多的自动化。

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

Tactic automation: simple decision procedure

coq

coq-tactic