coq
検索とバリアントで既存のファクトを検索する

構文

• Search qualid. （* Coq 8.4以降のバージョンでは*）
• SearchAbout qualid. （*非推奨の同義語*）

パラメーター

備考

特定の識別子に関する事実

関連するすべての事実を確認するにはle前奏曲から関係を：

Coq < Search le.
le_n: forall n : nat, n <= n
le_S: forall n m : nat, n <= m -> n <= S m
...
max_l: forall n m : nat, m <= n -> Nat.max n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
...

表記< ：を含むすべての事実を検索するには、

Coq < Search "<".
exists_lt: forall (Q : nat -> Prop) (k l : nat), exists_between Q k l -> k < l
in_int_intro: forall p q r : nat, p <= r -> r < q -> in_int p q r
in_int_lt: forall p q r : nat, in_int p q r -> p < q
...

パターンの検索

仮説または結論のパターンを含むすべての事実を検索する：

Coq < Search (_ + O).
plus_n_O: forall n : nat, n = n + 0

_文字はワイルドカードとして機能し、複数回使用できます。

Coq < Search (S _ <= _).
le_S_n: forall n m : nat, S n <= S m -> n <= m
le_n_S: forall n m : nat, n <= m -> S n <= S m

また、非線形パターンを検索することもできます。

Coq < Search (?x <= ?x).
le_n: forall n : nat, n <= n

補題の終わりにパターンを検索する

その結論がどのようなものであるべきかを知っているときに補題を検索してください：

Coq < SearchPattern (S _ <= _).
le_n_S: forall n m : nat, n <= m -> S n <= S m

部分的な結論（結論と1つ以上の最後の仮説）を検索することもできます。

Coq < Require Import Arith.
Coq < SearchPattern (?x <= ?y -> ?y <= _ -> ?x <= _).
Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p

警告：仮説の順序を混ぜると、何も見つかりません。

Coq < SearchPattern (?y <= _ -> ?x <= ?y -> ?x <= _).