Coq - dependent type error in rewrite

I am using the Mathematical Components library and I am trying to prove this:

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.

The last rewrite fails with an error message:

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

Any idea on why the rewrite fails or an explanation of this error message?

Solution

The reason your rewrite fails is that k appears as a hidden parameter in S, thus by rewriting all the occurrences you make the goal ill-typed. You can check this by using Set Printing All.

by rewrite {5}H3.

will close your goal. Note that naming goals in H1...Hn style is not encouraged in mathcomp. Your indentation also doesn't follow math-comp style, and you may want to use exact: in place of by apply:.

Your proof can also be made shorter by using max_card:

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

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

thou you could also prefer to use a more generic from that won't require specifying the indexes:

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

Another way to avoid index tinkering is to rely on transitivity:

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

YMMV.