Add recursive functions to Strata Core

[joscoh]

Issue #, if available:

Description of changes: This PR adds support for recursive functions in Strata Core, including their definition in concrete syntax, partial evaluation, and an axiom-based SMT encoding.

Main changes:

1. This PR adds an additional attribute to the DDM @[scopeSelf] that acts like @[scope] but also adds the function's name to its body's scope. This is structured and handled very similarly to @[declareDatatype], which involves a similar recursive structure. Main changes are in AST.lean, Format.lean, Core.lean.
2. Adds fields to Func indicating whether a function is recursive and giving an optional decreases clause. This information is used in Env.lean to calculate the index of the decreasing argument. Here we also rule out recursive functions that are not yet supported: polymorphic functions, functions with more sophisticated termination measures, and functions without an explicit decreasing clause.
3. RecursiveAxioms.lean contains the generation of axioms as LExpr for a recursive function. Generating the axiom is fairly simple, since we just create term e.g. forall h t, length (List.cons h t) = length (List.cons h t) and then partially evaluate the right-hand side. Since recursive functions are marked as inlineIfConstr on their decreasing parameter, this produces the simplified form.

Other changes

1. Adds support in SMT/DDMTransform/Translate for trigger patterns complex enough to handle constructors applied to arguments (e.g. List.cons h t).
2. Changes the evaluation of if-then-else to always reduce within the then and else branches and changes the small-step semantics to match.

Tests

1. RecursiveAxiomTests.lean tests the generation of recursive axioms as Lambda terms.
2. This PR adds a test to SMTEncoderDatatypeTests.lean that demonstrates the SMT encoding of the recursive function axioms.
3. RecursiveFunctionDDMTest.lean tests the DDM parsing for recursive function.
4. RecursiveFunctionErrorTest.lean demonstrates not-yet-supported recursive functions.
5. RecursiveFunctionTests.lean contain a variety of programs with recursive functions, some of which contain VCs which can be solved purely by partial evaluation and others which require SMT-based reasoning.
6. BinaryTreeSize.lean gives a more complex example that demonstrates inductive reasoning over types and functions.

What is not supported (yet): polymorphic and mutually recursive functions, termination checking.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.