#17 Rewrite and inference rules add true goal and hypothesis

[Guillaume Verdier]

When a rewrite or inference rule (such as the ones in the attached project) is applied, it adds a ⊤ sub-goal and a ⊤ hypothesis to the actual goal, which needlessly clutters the proof tree.
This seems to be a relatively recent behavior: some unit tests fail because they expect a rewrite or inference rule to generate a single goal, while it generates this additional ⊤ goal.
This additional sub-goal seems to be generated to prove some well-definedness conditions: when none are needed, it is therefore true. However, it would be more user-friendly to avoid generating it in this case.

[Son Hoang]

I cannot remember the exact reason, but it must have something to do with Well-definedness.

[Son Hoang]

I now remember that it is about proof reuse. In order to reuse the proofs, the number of sub-goals has to be identical. This decision has been made since the early development of Rodin, i.e., the constraints is that every reasoner with the same input will produce the same number of sub-goal.
For example, if you change your operator so that the WD is not longer trivial, the shape of your proof tree changed, hence you potentially lose all the sub-proofs.
So this is a feature, not a bug.

[Guillaume Verdier]

Since this actually a feature, it was not modified. Unit tests that failed due to this new behavior have been fixed in commit 7f84e1c.