0
Coq에서
negb true을false으로 어떻게 바꿀 수 있습니까?Coq에서 negb true를 false로 다시 쓰려면 어떻게해야합니까?
나는 도서관에서 negb true을 false으로 다시 쓰는 간단한 방법을 찾고있었습니다.
그러나 유용한 것은 없습니다.
나는 simpl.을 알고 있지만 기본 구문을 선호합니다.
A
답변
1
당신은 이미 simpl이 negb true에서 false으로 줄 것이라는 것을 알고 있습니다. 이것은 두 정의가 동일하기 때문입니다. 먼저 당신이 필요로하는 문을 증명할 수 지식으로
, 다음에 다시 :
assert (H: negb true = false) by reflexivity.
rewrite H.
그러나 더 나은, 당신은 단지 한 줄이 모든 것을 할 replace를 사용할 수 있습니다
replace (negb true) with false by reflexivity.
두 경우 모두 반사율은 서브 호 (negb true = false)를 해결합니다 (앞에서 언급했듯이).
4
검색 엔진이 보조 정리를 검색하면 검색 엔진은 가져온 모듈 만 찾습니다. 먼저
Require Import Bool.
에 필요한 이유
그런 다음
Search (negb _ = false).
negb_false_iff: forall b : bool, negb b = false <-> b = true
당신은 재 작성을위한 보조 정리를 사용할 수 있습니다 보여 당신 Require Import Setoid 경우.
Goal negb true = false.
rewrite negb_false_iff. reflexivity. Qed.
당신은 아마 너무 많이 전개 및 대형 읽을 수없는 조건을 만들기 때문에 당신이 어떤 상황과 simpl 놨 최대 목표/가설에 negb true을 가지고 있기 때문에 simpl를 사용하지 않습니다.
simpl (negb true). (* rewrites `negb true` to `false` in the goal *)
또는
simpl (negb true) in *. (* rewrites `negb true` in the goal and hypotheses *)
simpl이이 방법을 사용하여 적용되는 컨텍스트를 좁힐 수 있습니다