refactor(assumption_justification): move to the kernel

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/expr): add new mk_app template for creating applications using a collection

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/metavar): add normalize assignment justification

We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/elaborator): improve simple_ho_match

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): missing normalization step for semantic attachments

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(numerics): add missing numeric_traits<float>::zero()

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(numerics/numeric_traits): add missing test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(coding_style): add how to organize template source code

[skip ci]
fix(kernel/normalizer): do not apply substitutions in the normalizer

It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/metavar): make sure the justification and substitution are always matching each other

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
style(kernel/metavar): add missing includes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): add missing conflict justification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/elaborator): solve easy overloads at preprocessing time

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): make the first argument of if-expression implicit, add support for marking implicit arguments on builtin symbols (aka semantic attachments)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(equality): make homogeneous equality the default equality

It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.

- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
     l = nil
will not propagate the type (List Int) to nil.

- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.

Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(frontends/lean): add 'l = nil' test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/library/elaborator): replace eq with my_eq because eq is now a builtin symbol

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): heterogeneous transitivity axiom, we need this axiom to be able to generate modular proofs in the rewriting engine module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/notation): adjust the implicit arguments of TransExt, and add new test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): make the 'expression template' argument in Subst implicit because higher-order matching can infer it.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>