trinum proof with induction help

Stream: new members

[Joseph O]

i have this theorem so far

import algebra.group_with_zero.units
import tactic.qify
import data.nat.parity

def sum' : ℕ → ℕ
  | 0 := 0
  | (n+1) := n + 1 + sum' n

lemma trinum :
  ∀ n : ℕ, n*(n-1)/2 = sum' n :=
begin
  intro n,
  let h : even (n * (n-1)) :=
  begin
    apply nat.even_mul_self_pred,
  end,
  rw nat.div_eq_iff_eq_mul_left,
  induction n,
  {
    rw zero_mul,
    have h : sum' 0 = 0 := rfl,
    rw h,
    rw zero_mul,
  },
  {
    rw nat.succ_sub_one,
    rw nat.succ_mul,
    sorry,
  },
  simp,
  exact even_iff_two_dvd.mp h,
end

and in my paper proof and lean proof, I'm not sure how to proceed to work with the sum' (succ n) in the goal for the block with sorry:

state:
case nat.succ
n_n : ℕ,
n_ih : let h : even (n_n * (n_n - 1)) := _ in n_n * (n_n - 1) = sum' n_n * 2,
h : even (n_n.succ * (n_n.succ - 1)) := n_n.succ.even_mul_self_pred
⊢ n_n * n_n + n_n = sum' n_n.succ * 2

NOTE: i don't want the full solution to the proof, just whatever answers the question. or, if my proof is completely bogus and stupid, you can let me know if i have to restart (and maybe with a hint as to what to do)

[Patrick Johnson]

• Use have h instead of let h and move it after induction
• Use induction n with n ih to make variable names nicer
• At the sorry, use dunfold sum' and then rw [add_mul, ←ih]

[Patrick Johnson]

Note also that your statement is incorrect. It should be n * (n + 1) / 2.

[Kevin Buzzard]

Your statement is also morally incorrect in that it uses pathological functions like natural subtraction and division. Your sum' type should be taking values in rationals if you want to faithfully represent the mathematics.

[Joseph O]

Yeah sorry for the trouble, i just realized that
Patrick Johnson said:

• Use have h instead of let h and move it after induction
• Use induction n with n ih to make variable names nicer
• At the sorry, use dunfold sum' and then rw [add_mul, ←ih]

[Joseph O]

also what does dunfolddo?

[Kyle Miller]

tactic#dunfold and tactic#unfold are for unfolding definitions. The difference is that dunfold will only unfold definitions that can be definitionally unfolded (it will only work whenever tactic#change would work)

[Kyle Miller]

It's like tactic#dsimp vs tactic#simp.

[Kyle Miller]

I think you can just use tactic#unfold and pretend tactic#dunfold doesn't exist (at least until you deal with more complicated dependent types where occasionally unfold doesn't work but dunfold does)

[Joseph O]

I see. Thank you, I was looking for this

[Joseph O]

@Kyle Miller i am unsure how to work with this goal

n: ℕ
ih: even (n * (n + 1)) → n * (n + 1) = sum' n * 2
h: even (n.succ * (n.succ + 1))
⊢ n * (n + 1) + n + (n + 1).succ = (n + 1) * 2 + n * (n + 1)

[Joseph O]

how can i turn (n+1).succ into n+2?