Coq - erreur de type dépendant dans rewrite

Question

J'utilise la bibliothèque des composants mathématiques et je suis en train de le prouver:

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. 

La dernière réécriture échoue avec un message d'erreur:

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

Toute idée pourquoi la réécriture échoue ou une explication de ce message d'erreur?

Answer 1

La raison pour laquelle votre réécriture échoue est que k apparaît comme un paramètre caché dans S, donc en réécrivant toutes les occurrences que vous avez mal typées. Vous pouvez vérifier cela en utilisant Set Printing All.

by rewrite {5}H3. 

fermer votre objectif. Notez que l'attribution de noms au style H1...Hn n'est pas encouragée dans mathcomp. Votre indentation ne suit pas non plus le style math-comp, et vous pouvez utiliser exact: à la place de by apply:.

Votre preuve peut aussi être plus court en utilisant max_card:

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

ou

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

tu vous pourriez aussi préférer utiliser un plus générique de qui ne nécessitera pas préciser les indices:

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

Une autre façon d'éviter le bricolage d'index est de se fier aux vité:

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

YMMV.