在 Coq 中将证明从 Z 转移到 N

Question

在 Coq in 中有没有办法以半自动的方式证明整数语句和自然数的转移语句？

举个具体的例子，取下面的引理：

Lemma cancellation:
  forall a b c: nat, a > 0 -> a * b = a * c -> b = c.

这个命题在Z中其实是成立的。这种情况下更容易证明，因为可以用减法得到a * (b - c) = 0，然后化简a。但是自然数的减法是有上限的，因此这是行不通的。

假设我可以用整数证明这一点。是否有一些策略可以用来推导出自然数的陈述？

Answer 1

一种解决方案是一种名为 zify 的策略，它会自动将操纵自然数的目标转变为操纵整数的目标（例如，通过插入对 Z.of_nat 的适当调用）。此策略由 lia 内部调用，但似乎没有很好的记录。至少提到了here.

在您的情况下，这将给出以下结果。

Require Import ZArith.

(* The lemma stated in Z. *)
Lemma cancellation:
  (forall a b c, a > 0 -> a * b = a * c -> b = c)%Z.
Proof.
  (* your favorite proof of this result *)
Admitted.

(* The lemma stated in nat. *)
Lemma cancellation_nat:
  forall a b c: nat, a > 0 -> a * b = a * c -> b = c.
Proof.
  intros.
  zify.
  eauto using cancellation.
Qed.

在 Coq 中将证明从 Z 转移到 N

Transfering proof from Z to N in Coq

formal-verification

coq

coq-tactic