how to solve basic arithmetic equation

Stream: new members

[Matei Adriel]

▶ 1 goal
x y z : RawInt
xy : x ~ y
yz : y ~ z
summed : x.1 + y.2 + (y.1 + z.2) = y.1 + x.2 + (z.1 + y.2)
⊢ y.pos + y.neg + (x.1 + z.2) = y.pos + y.neg + (z.1 + x.2)

Is there any way to solve this without manually applying a bunch of lemmas to both sides?

This is the code I have so far (I am doing this for educational reasons)

import LeanSandbox.Nat

structure RawInt where
  pos : Nat
  neg : Nat

private def eqv : (x y: RawInt) → Prop
  | ⟨a, b⟩, ⟨c, d⟩ => a + d = c + b

infix:50 " ~ " => eqv

private theorem eqv.refl (x: RawInt) : x ~ x := rfl
private theorem eqv.symm {x y: RawInt} (xy: x ~ y):  y ~ x := Eq.symm xy
/-
a - b   c - d   e - f
a + d = c + b
c + f = e + d
 => a + f = e + b -- the target

a + d + c + f = c + b + e + d
a + f + e + b -- done
-/
private theorem eqv.trans {x y z: RawInt} (xy: x ~ y) (yz: y ~ z): x ~ z := by
  have summed: _ := Nat.add_equations xy yz
  apply @Nat.subtract_to_equation_left _ _ (y.pos + y.neg)
  simp

[Eric Wieser]

I'm not familiar with lean4; but why is that pretty-printing mixing .1 and .pos?

[Arthur Paulino]

@Matei Adriel What's in LeanSandbox? Can you extract the minimal code necessary to run the code you pasted? Or point to a GitHub repo

[Arthur Paulino]

(deleted)

[Matei Adriel]

@Arthur Paulino Lean sandbox is just my "learning lean" folder. I'll make a repo the next time I'm on my laptop

[Arthur Paulino]

(deleted)

[Kyle Miller]

@Matei Adriel If you were using Lean 3 and mathlib, then I'd suggest tactic#ring_nf or tactic#linear_combination. Something you can still do is use simp to put terms into a normal form, if you give it enough lemmas:

example (x y z : RawInt)
  (summed : x.1 + y.2 + (y.1 + z.2) = y.1 + x.2 + (z.1 + y.2)) :
  y.pos + y.neg + (x.1 + z.2) = y.pos + y.neg + (z.1 + x.2) :=
by
   simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] at summed ⊢
   exact summed

[Mario Carneiro]

Eric Wieser said:

I'm not familiar with lean4; but why is that pretty-printing mixing .1 and .pos?

This is the issue I mentioned in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Working.20with.20primitive.20projections

[Mario Carneiro]

when you see .1 it's a primitive projection, while .pos is the projection function for the structure

[Mario Carneiro]

You can do this by two applications of ring: Eq.trans (by ring) summed |>.trans (by ring)

[Arthur Paulino]

This kind of arithmetic manipulation is something that I struggle with. How to use this to eliminate the sorry in

axiom sumeqs {a b c d : Nat} (hab : a = b) (hcd: c = d) : a + c = b + d

example {x y z: RawInt} (xy: x ~ y) (yz: y ~ z): x ~ z := by
  have := sumeqs xy yz
  -- this : x.pos + y.neg + (y.pos + z.neg) = y.pos + x.neg + (z.pos + y.neg)
  have h : (x.pos + z.neg) + (y.pos + y.neg) = (z.pos + x.neg) + (y.pos + y.neg) := sorry
  exact Nat.add_right_cancel h

[Arthur Paulino]

I suspect this reasoning is similar to what Matei had in mind according to his code comments

[Arthur Paulino]

Matei Adriel said:

Arthur Paulino Lean sandbox is just my "learning lean" folder. I'll make a repo the next time I'm on my laptop

Np, I only asked because I thought you wanted to know how to use Nat.add_equations and Nat.subtract_to_equation_left to prove the theorem

[Kyle Miller]

You can use the same sort of thing:

example {x y z: RawInt} (xy: x ~ y) (yz: y ~ z): x ~ z := by
  have := sumeqs xy yz
  -- this : x.pos + y.neg + (y.pos + z.neg) = y.pos + x.neg + (z.pos + y.neg)
  have h : (x.pos + z.neg) + (y.pos + y.neg) = (z.pos + x.neg) + (y.pos + y.neg) := by
    simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] at this ⊢
    exact this
  exact Nat.add_right_cancel h

[Kyle Miller]

Mario Carneiro said:

You can do this by two applications of ring: Eq.trans (by ring) summed |>.trans (by ring)

Just to show that this suggestion works even with a bad emulation of the ring tactic, if you're not using mathlib4 for some reason.

macro "ring" : tactic => `(simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm])

example (x y z : RawInt)
  (summed : x.1 + y.2 + (y.1 + z.2) = y.1 + x.2 + (z.1 + y.2)) :
  y.pos + y.neg + (x.1 + z.2) = y.pos + y.neg + (z.1 + x.2) :=
Eq.trans (by ring) summed |>.trans (by ring)

[Arthur Paulino]

Ah, then the reasoning is that we don't shape the hypothesis to be in the same form as the goal, but rather shape the hypothesis and the goal to be in the same form. And I thought that "normal form" would be ((a + b) + c) + d but it's actually a + (b + (c + d)) right?

[Matei Adriel]

@Kyle Miller I'll try your solution next time I'm on my laptop!
@Arthur Paulino yep, that's exactly what my code is doing. Is there a way to search for existing lemmas, hoogle style?

[Arthur Paulino]

I'm not familiar with Hoogle, but in Mathlib there's a tactic called library_search that tries to find the right lemma/theorem in your environment to prove a certain theorem. It works nicely in Lean 3, but for Lean 4 we'll need to wait some more

[Mauricio Collares]

Mathlib4 has a Hoogle equivalent: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Find.html

[Mauricio Collares]

But, as Arthur said, library_search is the way to go in Lean 3 and will eventually work great in Lean 4 too

[Matei Adriel]

So I have tried

private theorem eqv.trans {x y z: RawInt} (xy: x ~ y) (yz: y ~ z): x ~ z := by
  have summed: _ := Nat.add_equations xy yz
  apply @Nat.subtract_to_equation_left _ _ (y.pos + y.neg)
  simp_all [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
  exact summed

@Kyle Miller and I get this error:

Diagnostics:
1. type mismatch
     summed
   has type
     x.1 + (y.1 + (y.2 + z.2)) = y.1 + (z.1 + (x.2 + y.2)) : Prop
   but is expected to have type
     x.1 + (z.2 + (y.neg + y.pos)) = z.1 + (x.2 + (y.neg + y.pos)) : Prop

[Kyle Miller]

I had a similar sort of error before upgrading to the newest Lean 4 nightly build. What seems to be the case is that primitive projections and projection functions end up being sorted by simp in a different order, and in the newest version primitive projections stopped appearing. (Maybe @Mario Carneiro has an idea of what changed?)

[Matei Adriel]

Kyle Miller said:

I had a similar sort of error before upgrading to the newest Lean 4 nightly build. What seems to be the case is that primitive projections and projection functions end up being sorted by simp in a different order, and in the newest version primitive projections stopped appearing. (Maybe Mario Carneiro has an idea of what changed?)

How can I update using elan?

[Matei Adriel]

tried elan update but I still get the same error

[Eric Wieser]

The error is unrelated, your x and z are in different places

[Matei Adriel]

so is there any way to get rid of that without manually applying a bazillion lemmas

[Yaël Dillies]

What does simpa do here?

[Matei Adriel]

what @Kyle Miller proposed

[Kyle Miller]

Eric Wieser said:

The error is unrelated, your x and z are in different places

The primitive projections seem to cause a different sort order

[Kyle Miller]

@Matei Adriel If you post a #mwe I can try it on my own computer

[Matei Adriel]

https://github.com/Mateiadrielrafael/lean-sandbox

@Kyle Miller

[Kyle Miller]

On the Lean nightly from the last couple days, your code works. Actually, you need to delete the exact summed

private theorem eqv.trans {x y z: RawInt} (xy: x ~ y) (yz: y ~ z): x ~ z := by
  have summed: _ := Nat.add_equations xy yz
  apply @Nat.add_right_cancel _ (y.pos + y.neg) _
  simp_all [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]

[Matei Adriel]

yeah, removing the exact doesn't solve it either. How can I install the nightly build using elan?

[Kyle Miller]

Btw, I wasn't suggesting to tell you to delete exact summed -- I was just mentioning that you get "goals accomplished" on the newest Lean at the simp_all line.

[Kyle Miller]

I don't know how you're supposed to update your Lean 4 toolchain in a project, but for one of my projects I set the lean-toolchain file to contain leanprover/lean4:nightly rather than a specific version.

[Matei Adriel]

what lean-toolchain file?

[Kyle Miller]

I only know that I have one in the root folder of my project -- sorry, I can't really help beyond this.

[Matei Adriel]

thanks, figured it out eventually