如何在LEAN定理证明者中证明数学归纳公式？

Question

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

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是鳍集，f是函数，则s.sum f是$ \ sum_ {x \ in s} f（x）$。

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

感应步骤可以用rw完成。使用VSCode，您可以在证明中的每个逗号后单击以查看每个rw的功能。这使它成为ring策略将解决的形式。