如何在 Coq 中证明 a*b*c=a*(b*c)？答案

【问题标题】：How to prove a*b*c=a*(b*c) in Coq?如何在 Coq 中证明 a*b*c=a*(b*c)？
【发布时间】：2020-05-11 13:24:09
【问题描述】：

我试图证明上述问题。我得到了归纳的定义：

Definition nat_ind 
  (p : nat -> Prop)
  (basis : p 0)
  (step : forall n, p n -> p (S n)) :
    forall n, p n := fix f n :=
      match n return p n with
      | 0 => basis
      | S n => step n (f n)
      end.

这是我的尝试，但不知道如何完成

Goal forall a b c, a * b * c = a * (b * c).
Proof. 
 apply nat_ind.
  - intros a b c. revert a.
    apply (nat_ind (fun a => a * b * c = a * (b * c))); simpl.
    + reflexivity.
    + intros. f_equal. intros.

【问题讨论】：

标签： coq induction coqide

【解决方案1】：

在您第一次调用 nat_ind 之后，如果您查看您的目标，您会发现 Coq 根本没有做正确的事情！

______________________________________(1/3)
forall a b c : nat, a * b * c = a * (b * c)
______________________________________(2/3)
nat ->
(forall a b c : nat, a * b * c = a * (b * c)) ->
forall a b c : nat, a * b * c = a * (b * c)
______________________________________(3/3)
nat

这里发生的事情是它猜测了你的动机p，并决定将它与fun (_ : nat) => <YOUR_WHOLE_GOAL> 统一起来，一个给定任何nat 的函数都会给你的目标......是的，这很愚蠢！

推动它对a 进行归纳的一种方法是明确强制它这样做，其中：

apply nat_ind with (n := a)

（其中n 与您定义nat_ind 中使用的名称匹配）

在此之后，您将获得更合理的目标：

______________________________________(1/2)
forall b c : nat, 0 * b * c = 0 * (b * c)
______________________________________(2/2)
forall n : nat,
(forall b c : nat, n * b * c = n * (b * c)) ->
forall b c : nat, S n * b * c = S n * (b * c)

确实a 已分别被0 和S n 取代。

[编辑：我想这并不能完全回答你的问题，因为你在第二次感应电话中已经达到了同样的目的......]

为了解决您的目标，拥有一个关于乘法对加法的分布的属性将有很大帮助：

forall n m p, (n + m) * p = n * p + m * p

所有这些，以及您要证明的内容，都已经存在于 Coq 中。这是作业吗？你只是在训练吗？

【讨论】：