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.

Последняя перезапись завершается с сообщением об ошибке:

Ошибка: ошибка зависимого типа при перезаписи (fun _pattern_value_ : nat => is_true (#|S| <= _pattern_value_)

Любая идея о том, почему переписать не удается или объяснение этого сообщения об ошибке?

Answer 1

Причина, по которой ваш переписать не удается, в том, что k отображается как скрытый параметр в SТаким образом, переписывая все вхождения, вы делаете цель нетипичной. Вы можете проверить это с помощью Set Printing All,

by rewrite {5}H3.

закрою вашу цель. Обратите внимание, что наименование целей в H1...Hn стиль не поощряется в mathcomp. Ваш отступ также не соответствует стилю математики, и вы можете использовать exact: на месте by apply:,

Ваше доказательство также может быть сокращено с помощью 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.

Другой способ избежать подстройки индекса - это полагаться на транзитивность:

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

YMMV.