Стереть общую константу уравнения с помощью LeanProver

Я бы сказал, что вы задали неправильный вопрос. Ваша гипотеза и цель содержат /, но это не математическое деление, это патологическая функция, которую используют компьютерщики, которая принимает на вход два натуральных числа и вынуждена возвращать натуральное число, поэтому часто не может вернуть правильный ответ. Например, 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