本文介绍了将Coq引理移植到Z上，将类似的引理移植到nat上的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
我有一个证明为 Z 的引理。所有变量都必须大于或等于零。
I have a lemma that is proved for Z. All the variables are bounded to be greater that or equal to zero.
问：如何尽可能容易地并且尽可能普遍地将引理移植到 nat ，即使用通过使用 Z 的引理来证明 nat 的类似引理？
Q: How can one as easily and generally as possible "port" that lemma to nat, i.e. use that lemma to prove a similar lemma for nat by using the lemma for Z?
示例：
Require Import ZArith.
Open Scope Z.
Lemma Z_lemma:
forall n n0 n1 n2 n3 n4 n5 n6 : Z,
n >= 0 -> n0 >= 0 -> n1 >= 0 ->
n2 >= 0 -> n3 >= 0 -> n4 >= 0 ->
n5 >= 0 -> n6 >= 0 ->
n5 + n4 = n6 + n3 ->
n1 + n0 = n2 + n ->
n5 * n1 + n6 * n2 + n3 * n0 + n * n4 =
n5 * n2 + n1 * n6 + n3 * n + n0 * n4.
Admitted.
Close Scope Z.
Lemma nat_lemma:
forall n n0 n1 n2 n3 n4 n5 n6 : nat,
n5 + n4 = n6 + n3 ->
n1 + n0 = n2 + n ->
n5 * n1 + n6 * n2 + n3 * n0 + n * n4 =
n5 * n2 + n1 * n6 + n3 * n + n0 * n4.
(* prove this using `Z_lemma` *)
推荐答案
您可以通过定义 Z.of_nat 具有内射性并将其分布到（+）和（*）：
You can do it rather generically for all the lemmas which have this shape by defining a tactic exploiting the fact that Z.of_nat is injective and distributes over (+) and (*):
Ltac solve_using_Z_and lemma :=
(* Apply Z.of_nat to both sides of the equation *)
apply Nat2Z.inj;
(* Push Z.of_nat through multiplications and additions *)
repeat (rewrite Nat2Z.inj_mul || rewrite Nat2Z.inj_add);
(* Apply the lemma passed as an argument*)
apply lemma;
(* Discharge all the goals with the shape Z.of_nat m >= 0 *)
try (apply Zle_ge, Nat2Z.is_nonneg);
(* Push the multiplications and additions back through Z.of_nat *)
repeat (rewrite <- Nat2Z.inj_mul || rewrite <- Nat2Z.inj_add);
(* Peal off Z.of_nat on each side of the equation *)
f_equal;
(* Look up the assumption in the environment*)
assumption.
nat_lemma 的证明现在变成：
Lemma nat_lemma:
forall n n0 n1 n2 n3 n4 n5 n6 : nat,
n5 + n4 = n6 + n3 ->
n1 + n0 = n2 + n ->
n5 * n1 + n6 * n2 + n3 * n0 + n * n4 =
n5 * n2 + n1 * n6 + n3 * n + n0 * n4.
Proof.
intros; solve_using_Z_and Z_lemma.
Qed.
这篇关于将Coq引理移植到Z上，将类似的引理移植到nat上的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！