feat(library/tactic): expose COND and WHEN tacticals in Lua, add HOL-like tactical names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): modify assumption_tactic, it should fail if not applicable, and TRY tactical

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/elaborator): simplify synthesizer interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): add basic tactic support in the frontend

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parse): allow script-code blocks to be used in the apply command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
style(frontends/lean/parse): missing include

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lua): incorrect assertion

The assertion got violated after a bug was fixed in the to_goal procedure.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add show_tactic, and optional '.' in the end of tactic command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition.

Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P.

For example, consider the constraint
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b))

Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet.
So, the elaborator would continue to process the constraint, and convert it into:

[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

Now, ?M::1 is assigned to the term
     if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

This is bad, since the original structure was lost.

This commit also contains an example that only works after the commit is applied.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add to_tactic_ext, it allows functions that return tactics to be used where a tactic is expected

For example, after this commit, we can write

simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic

instead of

simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic()

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/rewriter): add skeleton for depth rewriter
refactor(library/rewriter): have separate functions to build RW results from components
feat(library/rewriter): add apply_rewriter_fn skeleton
checkpoint for rewriter
checkpoint
checkpoint
checkpoint