search

advancedresearch / poi

a pragmatic point-free theorem prover assistant
Apache License 2.0
136 stars 7 forks source link

Not able to solve simple goal #1085

Closed bvssvni closed 9 months ago

bvssvni commented 9 months ago 
> goal (x^2 - x) / 2
> (4 * x ^ 2 - 4 * x) / 8

I suggest adding the following rules to the standard library:

(a * b + a * c) / d <=> (a / d) * (b + c);
(a * b - a * c) / d <=> (a / d) * (b - c);
0.5 * a <=> a / 2;