Transferring proof from Z to N in Coq

Link:: https://stackoverflow.com/q/54752598

Display all goals and responses

Question

Is there a way in Coq in to prove a statement for integer numbers and the transfer statement in a semi-automatic way to naturals?

For a concrete example, take the following lemma:

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

The statement is actually true in Z. In this case, it is easier to prove, because one can use subtraction to get a * (b - c) = 0 and then simplify a. But subtraction for naturals is capped, hence this would not work.

Assume I can prove this for integers. Is there some tactic that one could use to derive the statement for naturals as well?

Answer

One solution is a tactic called zify that automatically turns a goal manipulating naturals into a goal manipulating integers (e.g., by inserting appropriate calls to Z.of_nat). This tactic is internally called by lia, but does not seem to be well documented. It is at least mentioned here.

In your case, this would give the following.

Require Import ZArith.

(* The lemma stated in Z. *)
Lemma cancellation:
  (forall a b c, a > 0 -> a * b = a * c -> b = c)%Z.forall a b c : Z,
(a > 0)%Z -> (a * b)%Z = (a * c)%Z -> b = c
Proof.forall a b c : Z,
(a > 0)%Z -> (a * b)%Z = (a * c)%Z -> b = c
  (* 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.forall a b c : nat, a > 0 -> a * b = a * c -> b = c
Proof.forall a b c : nat, a > 0 -> a * b = a * c -> b = c
  intros.a, b, c: nat
H: a > 0
H0: a * b = a * c
b = c zify.a, b, c: nat
H0: (Z.of_nat a * Z.of_nat b)%Z =
(Z.of_nat a * Z.of_nat c)%Z
H: (Z.of_nat a > 0)%Z
cstr: (0 <= Z.of_nat a)%Z
cstr0: (0 <= Z.of_nat b)%Z
cstr1: (0 <= Z.of_nat c)%Z
__sat: (0 <= Z.of_nat a * Z.of_nat c)%Z
__sat0: (0 <= Z.of_nat a * Z.of_nat b)%Z
Z.of_nat b = Z.of_nat c eauto using cancellation.
Qed.