fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool

The method is_proposition was using an optimization that became incorrect after  we identified Pi and forall.
It was assuming that any Pi expression is not a proposition.
This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/simplifier): filter out propositions that cannot be used as conditional equations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lua): more to_ceqs tests

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

The elaborator was failing in the following higher-order constraint

   ctx |- (?M a) = (?M b)

This constraint has solution, but the missing condition was making the elaborator to reduce this problem to

   ctx |- a = b

That does not have a solution.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/simplifier): simplifier should only use homogeneous equalities

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/simplifier): convert disequalities (a ≠ b) into equations '(a = b) = false'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/simplifier): relax rule for conditional equalities

The idea is to support conditional equations where the left-hand-side does not contain all theorem arguments, but the missing arguments can be inferred using type inference.
For example, we will be able to have the eta theorem as rewrite rule:

theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
:= funext (λ x : A, refl (f x))

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin): minimize use of heterogenous equality in the kernel, add simpler version of congruence theorems for non-dependent types

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lean): adjust tests to reflect recent changes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(kernel/expr): remove dead code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(kernel/expr): check if the serializer works for applications with many argumets

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(kernel/expr): check if the serializer works for metavariables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lua): exercise fields method for semantic attachments

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(kernel/expr): remove dead code

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