タクティックオートメーション：簡単な決定手順

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) := _. 

になります。

tauto

注意がintuition failと同じであるので、これは、ejgallegoの証明にかなり類似していること（:= _が. Proof. typeclasses eauto. Defined.と同じである自体、. Proof. exact _. Defined.と同じである。注意してください）。

the original boilerplate in fiat-cryptoは、はるかに長く、単にhnf in *; tautoを使用するよりも強力であり、数十種類の異なる決定可能な命題を扱うことにも注意してください。

Answer 2

ほとんどの場合、証明は最も簡潔です。あなたは何ができるか、せいぜいなど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 3

ジェイソンの答えの精神に続いて、我々はもちろん、あなたの結果に到着する決定可能平等に対処するいくつかのライブラリを使用することができます。

これは決定可能平等とタイプとして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. 

さらにいくつかの自動化はもちろん使用できます。