rewrite rule

Stream: new members

[Kyle Miller]

It's in the top-level namespace, but to use it you need to import algebra.group_with_zero.units (or import something that imports this module).

[Joseph O]

Thank you.

[Kyle Miller]

The module name is the top-middle of the docs page that Andrew gave

[Joseph O]

Ok so i did try that before, and it turns out it wasn't working because i didn't have mathlib.
i made the project again with leanproject, but it fails to add mathlib for some reason, even though my elan is set to Lean 3.42.1
image.png

[Eric Wieser]

elan self update should help

[Notification Bot]

This topic was moved here from #general > rewrite rule by Eric Wieser.

[Joseph O]

@Andrew Yang i tried this:

import algebra.group_with_zero.units

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

lemma trinum :
  ∀ n : ℕ, n*(n-1)/2 = sum' n :=
begin
  rw div_eq_iff,
end

yet it gives me the error

rewrite tactic failed, did not find instance of the pattern in the target expression
  _ = ?m_5
state:
⊢ ∀ (n : ℕ), n * (n - 1) / 2 = sum' n

[Matt Diamond]

try intro n, first

[Andrew Yang]

This is because n/2 = m ↔ n = 2 * m does not hold in general for ℕ: the division is rounding down.

[Andrew Yang]

docs#tactic.interactive.qify would be useful here. You will need to supply it with a proof that 2 ∣ n * (n-1).

[Ruben Van de Velde]

docs#nat.div_eq_iff_eq_mul_left also probably works, with the same proof obligation

[Joseph O]

@Andrew Yang now i have the problem of proving h. library search doesn't suggest anything

import algebra.group_with_zero.units
import tactic.qify

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

lemma trinum :
  ∀ n : ℕ, n*(n-1)/2 = sum' n :=
begin
  intro n,
  let h : 2 ∣ n * (n-1) := by sorry,
  qify,
  rw div_eq_iff,
end

[Andrew Yang]

docs#nat.even_mul_self_pred

[Andrew Yang]

and also docs#even_iff_two_dvd

[Joseph O]

I cant import nat or data.nat for some reason

[Andrew Yang]

Is your mathlib up to date? Does elan self update not work for you?

[Matt Diamond]

if you're trying to use the first suggestion you'll need to import data.nat.parity... nat and data.nat are not valid imports

[Joseph O]

Andrew Yang said:

Is your mathlib up to date? Does elan self update not work for you?

i did that already

[Andrew Yang]

Lean modules are different from namespaces. The module name is the top-middle of the docs page.

[Mauricio Collares]

Joseph O said:

i did that already

And what is the output of elan --version? If it's not 1.4.2, how did you install elan originally?

[Matt Diamond]

@Mauricio Collares I think this person has already solved the "missing mathlib" issue, if you're trying to help with that