将 Z 上的 Coq 引理移植到 nat 上的类似引理

Question

我有一个引理被证明 Z。所有变量都必须大于或等于零。

问：如何尽可能简单和普遍地 "port" 到 nat 的引理，即使用该引理证明 nat 的类似引理，方法是使用引理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` *)

Answer 1

你可以通过定义一个策略来对所有具有这种形状的引理进行相当通用的操作，即利用 Z.of_nat 是单射的并分布在 (+) 和 (*) 上的事实：

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.

将 Z 上的 Coq 引理移植到 nat 上的类似引理

Port a Coq lemma over Z to a similar lemma over nat

coq