我要证明自己低于目标。
n_n: ℕ
n_ih: n_n * (n_n + 1) / 2 = arith_sum n_n
⊢ (n_n + 1) * (n_n + 1 + 1) / 2 = n_n + 1 + n_n * (n_n + 1) / 2
ring, simp, linarith不能工作。我也试过微积分，但它太长了。是否有自动删除方程中的公共常数的命令?
我会说你问错了问题。你的假设和目标包含/，但这不是数学除法，这是计算机科学家使用的病理函数，它将两个自然数作为输入，并被迫返回一个自然数，所以通常不能返回正确的答案。例如5 / 2 = 2和你使用的除法。计算机科学家称之为"除余"。我称之为"破碎的，永远不应该被使用"。当我在课堂上做这种练习时，我总是在除法之前把所有的东西都强制化为，所以除法是数学除法而不是这个不满足(a / b) * b = a的病态函数。事实上，这种除法不遵守常规除法的规则，这就是为什么你不能让战术起作用。如果你在做除法之前把所有的东西都强制化为有理数，那么你就不会陷入这种混乱，ring就会很好地工作。
如果你想坚持自然除法，那么一种方法就是开始证明n(n+1)总是偶数，这样你就可以推导出n(n+1)/2)*2=n(n+1)。或者，你可以通过观察来避免这种情况，证明A/2=B/2足以证明A=B。但无论哪种方式，你都必须做几行手工操作，因为你不是在使用数学函数，你是在使用计算机科学近似，所以数学策略对它们不起作用。
我的方法是这样的:
import algebra.big_operators
open_locale big_operators
open finset
def arith_sum (n : ℕ) := ∑ i in range n, (i : ℚ) -- answer is rational
example (n : ℕ) : arith_sum n = n*(n-1)/2 :=
begin
unfold arith_sum,
induction n with d hd,
{ simp },
{ rw [finset.sum_range_succ, hd, nat.succ_eq_add_one],
push_cast,
ring, -- works now
}
end