# Zulip Chat Archive

## 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

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

(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

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

(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
simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] at summed ⊢
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
exact Nat.add_right_cancel h
```

#### 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):

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 (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
simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] at this ⊢
exact this
exact Nat.add_right_cancel h
```

#### 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)
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 (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

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

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

@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) _
simp_all [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
```

#### 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