## Stream: new members

### Topic: how to solve basic arithmetic equation

#### Matei Adriel (Apr 13 2022 at 18:35):

▶ 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 (Apr 13 2022 at 20:46):

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

#### Arthur Paulino (Apr 13 2022 at 20:50):

@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

(deleted)

#### Matei Adriel (Apr 13 2022 at 22:57):

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

(deleted)

#### Kyle Miller (Apr 14 2022 at 00:21):

@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
exact summed


#### Mario Carneiro (Apr 14 2022 at 00:38):

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 (Apr 14 2022 at 00:39):

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

#### Mario Carneiro (Apr 14 2022 at 00:41):

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

#### Arthur Paulino (Apr 14 2022 at 00:41):

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


#### Arthur Paulino (Apr 14 2022 at 00:43):

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

#### Arthur Paulino (Apr 14 2022 at 00:52):

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 (Apr 14 2022 at 00:54):

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
exact this


#### Kyle Miller (Apr 14 2022 at 00:57):

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 (Apr 14 2022 at 00:58):

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 (Apr 14 2022 at 10:55):

@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 (Apr 14 2022 at 11:02):

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 (Apr 14 2022 at 11:07):

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

#### Mauricio Collares (Apr 14 2022 at 11:08):

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 (Apr 15 2022 at 15:26):

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)
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 (Apr 15 2022 at 15:33):

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 (Apr 15 2022 at 15:34):

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 (Apr 15 2022 at 15:38):

tried elan update but I still get the same error

#### Eric Wieser (Apr 15 2022 at 15:41):

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

#### Matei Adriel (Apr 15 2022 at 15:42):

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

#### Yaël Dillies (Apr 15 2022 at 15:43):

What does simpa do here?

#### Matei Adriel (Apr 15 2022 at 15:44):

what @Kyle Miller proposed

#### Kyle Miller (Apr 15 2022 at 15:46):

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 (Apr 15 2022 at 15:46):

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

@Kyle Miller

#### Kyle Miller (Apr 15 2022 at 15:51):

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) _


#### Matei Adriel (Apr 15 2022 at 15:52):

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

#### Kyle Miller (Apr 15 2022 at 15:53):

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 (Apr 15 2022 at 15:54):

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 (Apr 15 2022 at 15:55):

what lean-toolchain file?

#### Kyle Miller (Apr 15 2022 at 15:58):

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

#### Matei Adriel (Apr 15 2022 at 16:02):

thanks, figured it out eventually

Last updated: Dec 20 2023 at 11:08 UTC