如何用Coq List证明自然数定理？Coq新手求助证明思路

嘿，作为Coq新手遇到这种卡壳太正常啦！我来帮你一步步拆解这个问题——本质上你想证明的是乘法对加法的分配律在列表上的推广，先从形式化问题入手，再逐步完成证明。

1. 明确核心定理 #

你的例子本质是：对于一组自然数a₁,a₂,...,aₙ和固定乘数d，(a₁*d)+(a₂*d)+...+(aₙ*d) = (a₁+a₂+...+aₙ)*d。我们先从这个通用情况证明，再扩展到你提到的配对列表场景。

2. 导入必要库 #

首先导入Coq的列表和算术库，方便使用求和、映射等工具函数：

Require Import List Arith.
Import ListNotations. (* 支持[1;2;3]这样的直观列表语法 *)

3. 证明固定乘数的列表分配律 #

先证明最基础的版本：给定自然数列表和固定乘数，列表元素逐个乘d的和等于列表总和乘d。

Theorem sum_mult_distr : forall (d : nat) (l : list nat),
  sum (map (fun n => n * d) l) = (sum l) * d.
Proof.
  intros d l.
  (* 对列表l进行归纳证明，这是列表性质证明的核心思路 *)
  induction l as [|n l IH].
  - (* 基础情况：空列表 *)
    simpl. (* 简化后两边都是0，直接相等 *)
    reflexivity.
  - (* 归纳步骤：假设子列表l满足定理，推导n::l的情况 *)
    simpl. (* 简化后左边是(n*d) + sum(map...)，右边是(n + sum l)*d *)
    rewrite IH. (* 用归纳假设替换sum(map...)为(sum l)*d *)
    rewrite <- plus_mult_distr_r. (* 调用Coq内置的算术分配律：a*d + b*d = (a+b)*d *)
    reflexivity. (* 两边完全一致，得证 *)
Qed.

关键小提示： #

• 卡壳时可以用Search "plus mult distr".快速查找Coq内置的算术定理，比如这里用到的plus_mult_distr_r；
• 列表的归纳结构是固定的：要么是空列表，要么是「单个元素+子列表」的组合，几乎所有列表性质都可以用归纳法突破。

4. 扩展到配对列表场景 #

如果你想用存储(a,d)的配对列表（且所有配对的d都相同），我们先定义一个谓词确保列表中所有配对的第二个元素一致，再证明对应的定理：

(* 定义谓词：列表中所有配对的第二个元素都等于d *)
Definition all_snd_eq (d : nat) (l : list (nat * nat)) : Prop :=
  forall p, p el l -> snd p = d.

(* 配对列表的分配律定理 *)
Theorem sum_pair_mult_distr : forall (d : nat) (l : list (nat * nat)),
  all_snd_eq d l ->
  sum (map (fun p => fst p * snd p) l) = (sum (map fst l)) * d.
Proof.
  intros d l H.
  induction l as [|p l IH].
  - (* 空列表情况 *)
    simpl. reflexivity.
  - (* 归纳步骤 *)
    simpl.
    rewrite IH. (* 应用归纳假设 *)
    (* 先证明当前配对p的第二个元素等于d（由谓词all_snd_eq保证） *)
    assert (snd p = d) as Hp.
    { apply H. left. reflexivity. }
    rewrite Hp. (* 替换snd p为d *)
    rewrite <- plus_mult_distr_r. (* 再次调用算术分配律 *)
    reflexivity.
Qed.

验证你的例子 #

把你的具体案例代入：

• 配对列表l = [(3,2);(5,2);(9,2)]
• 乘数d=2
• 显然all_snd_eq 2 l成立（所有配对的第二个元素都是2）

调用sum_pair_mult_distr定理就能得到你想要的结论：6+10+18 = (3+5+9)*2 = 34。

内容的提问来源于stack exchange，提问作者Tom And.