COQ - 재

Question

나는 수학 구성 요소 라이브러리를 사용하고 있는데이 증명하려고에 의존의 형태 오류 :

마지막 재 작성 오류 메시지와 함께 실패

Lemma card_sub_ord (k : nat) (P : nat -> bool) : 
    #|[set i : 'I_k | P i]| <= k. 
Proof. 
    set S := [set i : 'I_k | P i]. 
    have H1 : S \subset 'I_k. 
    by apply: subset_predT. 
    have H2 : #|S| <= #|'I_k|. 
    by apply: subset_leq_card. 
    have H3 : k = #|'I_k|. 
    by rewrite card_ord. 
    (* Only goal left: #|S| <= k *) 
    rewrite H3 (* <--- this fails *) 
Admitted. 

:

Error: dependent type error in rewrite of (fun _pattern_value_ : nat => is_true (#|S| <= _pattern_value_)

어떤 생각 다시 쓰기가 실패한 이유 또는이 오류 메시지에 대한 설명

Answer 1

다시 쓰기가 실패한 이유는 k이 S에 숨겨진 매개 변수로 표시되어 목표를 잘못 입력 한 모든 항목을 다시 작성한다는 것입니다. Set Printing All을 사용하여이를 확인할 수 있습니다.

by rewrite {5}H3. 

으로 끝납니다. H1...Hn 스타일의 목표 지정은 mathcomp에서 권장하지 않습니다. 여러분의 들여 쓰기도 수학 comp 스타일을 따르지 않으므로 by apply: 대신 exact:을 사용할 수 있습니다.

귀하의 증거도 max_card를 사용하여 단축 할 수

:

by rewrite -{8}(card_ord k) max_card. 

또는

by rewrite -[k in _ <= k]card_ord max_card. 

당신은 또한 인덱스를 지정 요구하지 않을 것이다 것과 더 일반적인 사용을 선호 할 수 thou를 :

suff: #|[set i : 'I_k | P i]| <= #|'I_k| by rewrite card_ord. 
exact: max_card. 

색인 땜질을 피하는 또 다른 방법은 transiti vity :

by rewrite (leq_trans (max_card _)) ?card_ord. 

YMMV.