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

부분 결론 (결론과 하나 또는 여러 개의 마지막 가설)을 검색 할 수도 있습니다.

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