sandialabs / Prove-It

A tool for proving and organizing general theorems using Python.
http://pyproveit.org
Other
27 stars 10 forks source link

Mult.factorization with recursion #290

Open wwitzel opened 2 years ago

wwitzel commented 2 years ago

Currently, Mult.factorization requires 'the_factor' to be a direct factor. But to be more complete and versatile, it should be able to factor from an exponentiation factor or nested Mult or maybe a sum:

Examples: a b^5 c = b^2 (a b^3 c) a (b b) c = b (a b c) a (b + bd) c = b (a (1 + d) * c)

Add.factorization uses recursion already. That can be a guide as appropriate, but the situation is a little different. In Add, the factor must appear in every term. In Mult, the factor must appear in any factor. So it is trickier with Mult because we'd want a way to peek in and decide if we can perform a factorization without actually doing the factorization to avoid extra work. We probably want number operations to have an "is_factorable(the_factors)" method to facilitate such a thing. If we are pulling to the left, find the first factorable factor going left to right. If we are pulling to the right, find the first factorable factor going right to left, perhaps.