Simplify right-hand side of claims

[ttuegel]

Should we simplify the right-hand side of claims at startup? Does it matter, if we implement #1270?

[yzhang90]

Suppose we have a claim

 rule <k> #start => #end </k> <a> X  => #fun2(X)</a>

and semantics rule

rule <k> #start => #step1 </k> <a> X </a> requires X > 0

In the removeDestination step after applying the semantics rule, even if we do unification first, and the unification in the cell fails, we still need to evaluate #fun2(X), is it correct?

But in most cases, #fun2 would be either unsimplifiable or its argument is concrete. If it is the latter case, function memoization should be helpful.

I would postpone the implementation of this until we met some concrete examples where simplifying RHS first will greatly improve the performance because short startup time during proof debugging is also something that I want.

[ttuegel]

Related: #1278, #1304

[ttuegel]

We discussed this today. We might consider evaluating functions on the right-hand side, but avoiding other simplification which could cause branching.

[ttuegel]

Does it matter, if we implement #1270?

The answer to this question, now that #1270 is finished, is "yes, it matters".