我正在使用数学组件库,我正在尝试证明这一点:
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_)
时依赖类型错误
知道重写失败的原因或对此错误消息的解释吗?
重写失败的原因是k
在S
中显示为隐藏参数,因此通过重写所有出现,您使目标键入错误。您可以使用 Set Printing All
进行检查。
by rewrite {5}H3.
将关闭您的目标。请注意,在 mathcomp 中不鼓励以H1...Hn
风格命名目标。您的缩进也不遵循数学运算样式,您可能希望使用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.
扬子晚报.