refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env

This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker.
metavar_env is now a smart point to metavar_env_cell.
ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly.

example showing that the approach for caching metavar_env is broken in the type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm'

This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle

    ctx |- Type << ?f b

as

    ctx |- Type =:= ?f b

This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/type_inferer): provide the metavar_env to instantiate and lift_free_vars in the type_inferer, it will minimize the number of local_entries needed

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed

The modifications started at commit 1852c86948dd7da8a2bac224e3c7c0ee309db224 made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as:

[x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0, inst:1 #2, inst:2 #4, inst:3 #6, inst:5 #5, inst:6 #7, inst:7 #9, inst:9 #9, inst:10 #11, inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1, inst:2 #3, inst:3 #5, inst:4 #7, inst:6 #6, inst:7 #8, inst:8 #10, inst:10 #10, inst:11 #12, inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈
?M::22 x a

After the changes, only very simple constraints are generated. The most complicated one is:

[] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/elaborator): add extra occurs-check test

The idea is to catch the inconsistency in constraints such as:

    ctx |- ?m[inst:0 v] == fun x, ?m a x

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/list): improved filter that reuses list cells

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/list): add remove_last template

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/elaborator): improve elaborator state data-structure

The "quota" hack used before this commit was inefficient, and too hackish.
This commit uses two lists of constraints: active and delayed.
The delayed constraints are only processed when there are no active constraints.
We use a simple index to quickly find which delayed constraints have assigned metavariables.

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

checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(util/pdeque): remove unused template

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/basic_thms): add ExistsIntro theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/basic_thms): add ForallIntro theorem

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean): new elaborator tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): tag meta_app constraints of the form 'ctx |- m?[inst:i v] t1 =:= t2' as expensive

This commits also adds a new unit test that demonstrates non-termination due to this kind of constraint.

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