theorem-proving - 如何在 LEAN 定理证明器中证明数学归纳公式？

Question

谁能帮助我理解如何编写一个可以通过归纳轻松获得的简单结果的证明，例如第一个n自然数之和的公式：1+2+...+n = n(n+1)/2，使用 LEAN 定理证明器？

Answer 1

这是我的证明。你需要mathlib才能工作。

import algebra.big_operators tactic.ring

open finset

example (n : ℕ) : 2 * (range (n + 1)).sum id = n * (n + 1) :=
begin
  induction n with n ih,
  { refl },
  { rw [sum_range_succ, mul_add, ih, id.def, nat.succ_eq_add_one],
    ring }
end

range (n + 1)是小于 的自然数集n + 1，即 0 到 n。

我使用了这个finset.sum功能。如果s是一个finset并且f是一个函数，那么 s.sum f是$\sum_{x \in s} f(x)$。

该induction策略进行归纳。那么有两种情况。这个案例n = 0可以完成，refl因为这只不过是一个计算。

归纳步骤可以用 来完成rw。使用 VSCode，您可以在我的证明中的每个逗号后面单击以查看每个逗号的rw作用。这使它成为该ring策略将解决的形式。