Equality of Rat values

Stream: new members

[Labyrinth]

Hi, newbie here.

I am trying to work with Rats in Lean, but I am running into the exact same problem I had in Rocq (lol).

Here is my code:

def q1g (n : Nat) : Rat :=
  match n with
  | .zero => 0
  | .succ n' => (q1g n') + (-1)^(n+1)*n^2

def q1d (n : Nat) : Rat :=
  (-1)^(n+1)*n*(n+1)/2

theorem q1 (n : Nat) :
  q1g n = q1d n := by
  induction n with
  | zero =>
    unfold q1g q1d
    simp

The goal state at the end of this is 0 = 0/2, however I don't know how to prove this and can't find it looking online or through the docs.

Is this like in Rocq, where you need a different kind of equality for 0 = 0 # 2 to be true?

PS: Not 100% sure I'm on the best channel for this; sorry if not.

[Kevin Buzzard]

simp solves the goal for me with import Mathlib at the top -- so either you're on an old version of mathlib or you're not importing enough simp lemmas. But in general norm_num is the tactic you want for proving equalities in Rat, and for the induction step you'll also want ring.

Oh -- do you explicitly want to do this stuff mathlib-free? Then I don't have a clue. All the powerful tools for doing arithmetic/algebra are in the maths library.

[Labyrinth]

I feel a bit stupid now, because I added the import too and it just worked. I was on the live web version, and had "Latest Mathlib" selected, and... I thought that would import it without me specifying :sweat_smile:

[Kevin Buzzard]

Actually you can probably do this in core Lean only using grind or omega (powerful tools in the core library).

[Labyrinth]

Seems to work, yeah. I have no reason not to use Mathlib though (as long as I actually import it next time)

[Labyrinth]

Thanks Kevin!

[Notification Bot]

This topic was moved here from #lean4 > Equality of Rat values by Yury G. Kudryashov.

[Kenny Lau]

are we resolving topics now?

[Kevin Buzzard]

Not as far as I know -- indeed I think we were rather hoping that the community literally forgot that such a thing existed.

[Ruben Van de Velde]

We turned off the feature, I think, except for maintainers

[Kevin Buzzard]

Oh cool, I can even delete any evidence that this ever happened. (this topic was resolved and then unresolved again)