Передача доказательства от Z до N в Coq

Question

Есть ли в Coq способ доказать оператор для целых чисел и оператор перевода полуавтоматическим способом в натуральные числа?

В качестве конкретного примера возьмите следующую лемму:

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, но, похоже, не очень хорошо документирована.По крайней мере, здесь упоминается .

В вашем случае это даст следующее.

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.