コック - リライト

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ではお勧めできません。あなたの字下げは、また、数式 - コンバージョンスタイルに従わないので、by apply:の代わりにexact:を使用するとよいでしょう。

あなたの証明はまたmax_cardを使用することによって短くすることができます。

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

または

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

あなたもそれからより一般的なインデックスを指定する必要はありません使用することを好むことができ汝：

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。