Coq中如何证明0 ≤ a < b → rem a b = a？lia策略报错怎么办？

问题原因 #

• lia 策略本身仅支持纯线性整数算术命题的自动证明，对于 Z.rem 这类特殊算术运算，默认不会加载对应的运算性质公理，就算命题本身成立也无法自动推导，就会抛出 Cannot find witness 的报错。
• 你设置的 Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations 只适配了欧几里得除法的等式转换规则，没有覆盖 rem 的边界取值性质，所以对这个目标没有效果。

解决方法 #

方法1：直接调用标准库现成引理 #

Coq的ZArith标准库已经提供了完全符合你需求的现成引理 Z.rem_small，你可以直接调用完成证明：

Lemma rem_pos : forall {a b : Z},
  0 <= a < b ->
  rem a b = a.
Proof.
  intros. apply Z.rem_small. lia.
Qed.

这里内部的lia仅用来推导前提0 < b，完全在lia的能力范围内。

方法2：手动引入rem性质供lia调用 #

如果你希望全程用lia完成证明，可以手动把Z.rem的相关性质断言出来传给lia：

Lemma rem_pos : forall {a b : Z},
  0 <= a < b ->
  rem a b = a.
Proof.
  intros.
  pose proof Z.rem_eq a b.
  pose proof Z.rem_bound_abs a b.
  lia.
Qed.

内容的提问来源于stack exchange，提问作者geckos