Understand where singularities in disint test cases come from, and how to deal with them

[JacquesCarette]

Yuriy said:

d4, norm1a/b still have singularities. d4 contains the hardest one, I think - x/y. And also a new test case I added (DisintT/pair_x_x).

The biggest issue is all the singularities which are removed are done so in a fairly hack-y way. Instead of taking the (left and right) limit at that point, it just evaluates. I can't seem to get limit to work (even on very simple expressions).

[yuriy0]

A combination of limit, eval, and value will now (19acbd052) be able to remove most removable singularities. We will still need to deal with points in the domain where the LO form (interpreted as a 'real valued' function, which is basically what Maple understands) is genuinely discontinuous. pair_x_x is still an example of that.

limit does not yet take the left and right limits; it takes the two-directional limit, which is a stronger condition, so it cannot do the wrong thing, but there may yet be singularities it will not eliminate.

[JacquesCarette]

Could you add a specific example of what still needs to be done?

[yuriy0]

After a discussion quite a while ago, I realized I was almost certainly overthinking this issue; when we find x = k where x is a Lebesgue integration variable, we can just replace this with false. Likewise, x <= k is strengthened to x < k. This deals with all the cases where Maple (rightfully, from its point of view) produces an undefined in the result of diff. And of course it must do so - diff knows nothing of the properties of measures! It is not merely a coincidence that by applying these properties ourselves, we get the correct answer.

This was always happening in KB, but didn't occur in Partition for two reasons; at the time, certain constraints would cause an error inside KB (and so Partition just called solve, which is still the right thing to do in many cases - but now KB is occasionally used by Partition for condition simplification) and while the implementations (i.e. logic) of KB and Partition have much in common, they perform their jobs under slightly different contexts, so I though it a better idea to duplicate the commonality (instead of using KB in Partition directly) so that either one could be changed without effecting the other.

The function Partition:-Simpl:-singular_pts now implements the desired logic for Partition; the implementation could and probably will change over time, but the core logic now uses the properties we know about measures, which was the key missing issue in the previous implementation of the function.

The relevant function can be found here. The latest change to the function can be found here. The first working version is found here.