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.

最后一次重写失败并显示错误消息：

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.

将关闭您的目标。请注意，在 mathcomp 中不鼓励使用 H1...Hn 风格命名目标。您的缩进也不遵循 math-comp 样式，您可能想使用 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.

Coq - 重写中的依赖类型错误

Coq - dependent type error in rewrite

ssreflect