Coq - abhängiger Typ Fehler in Rewrite

Question

ich die mathematischen Komponenten Bibliothek verwenden und ich versuche, dies zu beweisen:

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. 

Die letzte Rewrite mit einer Fehlermeldung fehlschlägt:

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

Jede Idee Warum schlägt das Umschreiben fehl oder eine Erklärung dieser Fehlermeldung?

Answer 1

Der Grund für das Umschreiben ist, dass k als ausgeblendeter Parameter in S angezeigt wird, und zwar durch Umschreiben aller Vorkommnisse, die das Ziel unkorrekt machen. Sie können dies überprüfen, indem Sie Set Printing All verwenden.

by rewrite {5}H3. 

wird Ihr Ziel schließen. Beachten Sie, dass das Benennen von Zielen in H1...Hn Stil in Mathcomp nicht unterstützt wird. Ihre Einrückung folgt auch nicht dem Math-Comp-Stil, und Sie möchten vielleicht exact: anstelle von by apply: verwenden.

Ihr Nachweis kann auch kürzer gemacht werden, indem max_card mit:

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

oder

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

du Sie könnten auch aus, dass eine allgemeinere verwenden möchten benötigen nicht die Indizes festgelegt wird:

Eine weitere Möglichkeit, Indexbasteln zu vermeiden, ist die Verwendung von Transiti vity:

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

YMMV.