working with long arithmetic equations

Stream: new members

[Matei Adriel]

Say I have a goal which looks like a * x1 + a * x2 + a * x3 + ... a * x100 = b

What is the best way to group two specific terms? (eg: say I want to group x8 and x11 into a * (x8 + x11))

[Yaël Dillies]

You can state the equality you want and let abel do it for you.

[Matei Adriel]

what is abel?

[Yaël Dillies]

tactic#abel

[Arthur Paulino]

I think Matei is using Lean 4 though. Is abel available in Mathlib4?

[Henrik Böving]

Not to my or doc-gen4's knowledge

[Arthur Paulino]

You can use Kyle's trick with simp [Nat.add_comm, Nat.add_assoc, Nat.add_left_comm] to get an equation to its normal form

[Matei Adriel]

@Arthur Paulino that trick doesn't seem to help here

[Arthur Paulino]

#mwe

[Matei Adriel]

Don't think this is going to help, but here you go @Arthur Paulino

[Arthur Paulino]

Ah, I had misread your first post, sorry

[Arthur Paulino]

@Matei Adriel here's a smaller problem:

  private theorem multiplyRawInts.respects
    {x y z w: RawInt}
    (xz: x ~ z)
    (yw: y ~ w): multiplyRawInts x y = multiplyRawInts z w := by
    apply eqv.sound
    simp_all [eqv]
    apply @Nat.subtract_to_equation_left _ _
      (y.pos * z.neg + y.pos * z.pos + x.neg * w.pos + x.pos * w.pos)
    simp only [Nat.add_assoc]
    have : x.1 * y.1 + (x.2 * y.2 + (z.2 * w.1 + z.1 * w.2)) =
        z.1 * w.1 + (z.2 * w.2 + (x.2 * y.1 + x.1 * y.2)) := by
      sorry
    rw [this]

[Arthur Paulino]

Can you clear that sorry out?

[Matei Adriel]

ok, smaller problem - how do I "exit" conv mode? (and get back to the bigger goal)

[Henrik Böving]

By moving to the next higher indentation level

[Matei Adriel]

@Henrik Böving I can't seem to get that to work. Can you provide me an example?

[Henrik Böving]

theorem foo (a b c d : Nat) : a + b + c + d = a + c + b + d := by
  conv =>
    right
    left
    rw [Nat.add_assoc]
    right
    rw [Nat.add_comm]
  sorry

if you hover your cursor on the sorry you will see you are out of conv mode

[Matei Adriel]

oh, I was confused because I was hovering on the indentation before the sorry...

[Matei Adriel]

Ok, I was able to finish the proof:

  private theorem multiplyRawInts.respects: ∀
    {x y z w: RawInt}
    (xz: x ~ z)
    (yw: y ~ w), (multiplyRawInts x y = multiplyRawInts z w)
  | ⟨a, b⟩, ⟨c, d⟩, ⟨e, f⟩, ⟨g, h⟩ => by
    intro xz yw
    apply eqv.sound
    simp_all [eqv]

    have first: (c + h) * (b + e) + g * (a + f) + c * (a + f)
      = (c + h) * (f + a) + g * (b + e) + c * (b + e) := by
      simp [Nat.add_comm, xz, yw]

    have second: b * (d + g) + e * (c + h) + c * (a + f) + f * g + a * g
      = f * (c + h) + a * (d + g) + c * (b + e) + b * g + e * g := by
      simp [yw, xz] at first ⊢
      conv at first in g * (e + b) => rw [<-xz]
      conv at first => tactic => nat_ring
      nat_ring
      exact first

    conv at second => tactic => nat_ring
    apply @Nat.subtract_to_equation_left _ _
      (a * g + b * g + c * f + c * e)

    nat_ring_all

quite painful if I may say so myself :)

[Henrik Böving]

Have you tried to make some usage of simp_arith? It's usually quite helpful in situations like these

[Henrik Böving]

Assuming you are still using Lean 4, at least I havent heard of these nat_ring tactics yet

[Matei Adriel]

Henrik Böving said:

Assuming you are still using Lean 4, at least I havent heard of these nat_ring tactics yet

the nat_ring tactic is just a little macro @Kyle Miller showed me

macro "nat_ring"  : tactic => `(simp [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm, Nat.left_distrib, Nat.right_distrib])

(ended up adding a few things to the list myself)

[Matei Adriel]

I'm not sure what simp_arith does - my editor just hangs when I try to use it

[Matei Adriel]

I eventually get this error:

tactic 'simp' failed, nested error:
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

[Matei Adriel]

well, that's caused by simp_all_arith. simp_arith does work, but it does not solve the goal