Не могу использовать PeanoNat.Nat.add_assoc в качестве доказательства

Question

Require Import PeanoNat.

Check PeanoNat.Nat.add_assoc.

Вывод:

Nat.add_assoc
     : forall n m p : nat, n + (m + p) = n + m + p

Итак, теорема определена.

Но когда я создаю теорему и пытаюсь ее использовать, она выдает ошибку:

Theorem a : forall a b c d e f,
    a + b + c + d + e = f.
Proof.
  intros.
  PeanoNat.Nat.add_assoc a (b + c) d.

Ошибка: ссылка PeanoNat.Nat.add_assoc не найдена в текущей среде.

Почему не удается найти теорему?

Answer 1

То, что приходит после Proof., не само доказательство. Это серия инструкций, называемых тактикой, которые рассказывают Coq, как создать доказательство. add_assoc - это доказательство, а не тактика, которая создает доказательство. Вы бы использовали тактику rewrite (Nat.add_assoc a (b + c) d) для перезаписи (любой части) цели в соответствии с равенством

Nat.add_assoc a (b + c) d
  : a + (b + c + d) = a + (b + c) + d

Однако ваша цель a + b + c + d + e = f не содержит ни одного из этих терминов - + остается ассоциативным, а ваша цель на самом деле (((a + b) + c) + d) + e = f - поэтому эта тактика потерпит неудачу. На самом деле ваша цель недоказуема, но я предполагаю, что это только для примера. Вас также может заинтересовать тактика apply [prf]. Он принимает заключение (вещь справа от всех -> s и forall s) prf, сопоставляет его с целью и дает вам подцели для всех его гипотез. Смотрите также: Справочник по тактике Coq .