factorisation tactic

Stream: new members

[Nicholas Wilson]

is there a factorisation tactic? or is that (one of the things) what ring/ring_nf do?

[Nicholas Wilson]

I have a bunch of sums and each term in that sum has a bunch of common factors, e.g one term is

cos (a * x¹) * cos (a * x¹) * (cos (a * x) * cos (a * x)) * cosh (x¹ * b) * (cosh (x * b) * cosh (x * b)) *
                        sinh (x¹ * b) *
                      2

and the common factors shared are 2* cosh (x¹ * b) * sinh (x¹ * b), I would like to factor these common terms out or failing that bring them to the front (or at least together) so that I can apply sinh_two_mul.

[Johan Commelin]

If you manually write it in the form that you want, then ring can prove that your new expression is equal to the old one.

[Nicholas Wilson]

Ideally not because that is a _very_ long expression. (Also I realised some of them have 2* cosh (x¹ * b) * sinh (x¹ * b) and some of them have 2* cosh (x * b) * sinh (x * b) (x vs x¹))

[Nicholas Wilson]

also the factors are in different places in the sequence of products

[Kalle Kytölä]

I think what you are asking for is more symbolic computation than basic theorem proving. I don't think there is any reason that this could not be done by some tactics, but as Johan Commelin implicitly suggests above, currently you probably have to state the desired factorization manually. In fact I hope and believe that there will be more tactics that do some (simple) symbolic computation in Lean itself in the future.

(Incidentally, I am going to meet a CS professor today to discuss hiring summer interns to develop small bits of simple symbolic computation within Lean. :fingers_crossed:)

[Nicholas Wilson]

Indeed. Noted, I'd just love to be able to do factorise [2, cosh (x * b), sinh (x * b)] instead of spelling it all out for ring

[Nicholas Wilson]

any idea how hard it would be to write a tactic to do that? I've never written tactics before.

[Johan Commelin]

ring_nf chooses an ordering of the atoms that occur in the formula. Maybe such an optional list argument could influence the ordering. I don't know enough about the implementation of ring_nf to know whether this is easy to pull off. But that might lead to a first approximation of your hypothetical factorise

[Johan Commelin]

cc @Anne Baanen

[Nicholas Wilson]

Yeah i would expect to defer to ring/ring_nf for most of the heavy lifting.

[Damiano Testa]

For permuting factors, you can try move_mul.

[Damiano Testa]

If you can give a #mwe, I can try to see how it would work.

[Anne Baanen]

Johan Commelin said:

ring_nf chooses an ordering of the atoms that occur in the formula. Maybe such an optional list argument could influence the ordering. I don't know enough about the implementation of ring_nf to know whether this is easy to pull off. But that might lead to a first approximation of your hypothetical factorise

It should not be hard to modify docs#Mathlib.Tactic.AtomM.run or call docs#Mathlib.Tactic.AtomM.addAtom to pass these arguments. However, I have no real idea how well this would work in practice. Certainly we wouldn't be able to extract the factor 2 since numeric constants like that are handled specially.

[Anne Baanen]

I also tried tricks with metavariables like:

import Mathlib

example (a b c d : ℤ) : True := by
  have : a * b + a * c + d * a = a * _
  · ring -- goal: a * b + a * c + a * d = a ^ 2
  trivial

So it looks like _ gets unified with the first atom in the AtomM context.

[Damiano Testa]

I had something like this in mind:

import Mathlib

example (a b c d x : ℤ) : a * b + a * c + d * a = x := by
  move_mul [a]
  simp only [← add_mul]
  --  ⊢ (b + c + d) * a = x
  sorry

[Damiano Testa]

Note that this works also with the 2:

example (a b c d x : ℤ) : 2 * a * b + a * 2 * c + d * 2 * a = x := by
  move_mul [2, a]
  simp only [← add_mul]
  -- ⊢ (b + c + d) * 2 * a = x
  sorry

[Nicholas Wilson]

Silly question when I do move_mul [2, , cosh (x * b)] I get unexpected identifier; expected command, am I missing an Import or something?

[Damiano Testa]

It was a continuation of the previous example: import Mathlib.

[Nicholas Wilson]

Thanks, that's going to take a while...

[Damiano Testa]

import Mathlib.Tactic.MoveAdd
import Mathlib.Data.Int.Basic

open Lean Parser Tactic in
macro "factorise " ts:rwRuleSeq : tactic =>
  `(tactic| (move_mul $ts; simp only [← add_mul]))

open Lean Parser Tactic in
/-- `factorise`, but with the US-friendly spelling. -/
macro "factorize " ts:rwRuleSeq : tactic =>
  `(tactic| factorise $ts)

example (a b c d x : ℤ) : 2 * a * b + a * 2 * c + d * 2 * a = x := by
  factorise [2, a]
  -- ⊢ (b + c + d) * 2 * a = x
  sorry

this is somewhat more minimal.

[Damiano Testa]

You should try lake exe cache get.

[Damiano Testa]

By the way, it is not the first time that a "factorisation tactic" comes up. If there is support for this, I can PR the simple macro above as an initial implementation and then start dealing with further requests as needed.

[Damiano Testa]

Just to be clear, I am not planning for this to be a tactic that takes a ^2 - b ^ 2 and replaces it with (a - b) * (a + b). I am thinking of this simply as a tactic that collects together explicit factors that are already present in the expression and get called out by the user!

[Alex J. Best]

I would say we should wait and implement an actual factorization tactic that does what we want, otherwise it could be a headache or confusing to people to replace uses of the old one when we get one that does something stronger. One important feature that makes such a tactic even more useful is that it should produce proofs that the factors are prime / irreducible. That said we could implement the tactic you suggest, just with a different name, collect_factors or something?

[Damiano Testa]

Alex, the collect_factors name sounds like a good choice! I'll wait to see if there is are any further comments.