feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(examples/lean): improve dep_if example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/simplifier): assumptions/context may contain equations where the left-hand-side is a metavariable or semantic attachment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/simplifier): nontermination

The example tests/lua/simp1.lua demonstrates the issue.
The higher-order matcher matches closed terms that are definitionally equal.
So, given a definition

    definition a := 1

it will match 'a' with '1' since they are definitionally equal.

Then, if we have a theorem

    theorem a_eq_1 : a = 1

as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a"

   a --> 1 --> 1 --> 1 ...

The first simplification is expected. The other ones are not.
The problem is that "1" is definitionally equal to "a", and they match.
The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side.

To avoid this loop, we test if the new expression is not equal to the previous one.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/simplifier): nontermination