Lean: add support for range types

[ineol]

No description provided.

[github-actions]

Test Results

   12 files  ±0     24 suites  ±0   0s ⏱️ ±0s
  749 tests ±0    749 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 493 runs  +1  2 493 ✅ +1  0 💤 ±0  0 ❌ ±0 

Results for commit d89514c. ± Comparison against base commit f87c292.

♻️ This comment has been updated with latest results.

[javra]

The idea was to keep two kinds, @Alasdair implemented the Nat kind specifically to avoid having heuricstics. Not sure how to solve that for ranges, though.

I think your heuristic doensn't have a one-sided error? Nexp_neg can be a double negation, for example

[ineol]

So I grepped all the uses of range in the models and my understanding is that for the overwhelming majority of them they are clearly non-negative, and a few clearly include negative elements, so this is an optimistic assumption.

[Alasdair]

The way to do this would be to take an env representing the context when converting the type, then you can call Type_check.prove env (nc_gteq low (nint 0)). That avoids any syntactic-restrictions, but Lean might need more explicit conversions to be inserted.

[javra]

The rule for conversions is generally that Int to Nat would have to be made explicit while Nat to Int would be implicit

[ineol]

@javra what do you think is the best thing to do here?

[javra]

Have you tried using @Alasdair 's suggestion for implementing clearly_negative? Otherwise we could just leave it as it is and add a comment to improve the heuristics later on.

But I'd call it provably_positive and only return Nat if the lower bound can be proven to be positive, otherwise we'd have to use Int in order not to run into problems.

[ineol]

I implemented Alasdair's strategy and it seems to be working. I put the env in the context we already had.

Now, the ranges in parameters are transformed into atom in the enviroment somehow, and so are translated to Int. I guess for consistency we should translate them in the same way. Do you know what is going on @Alasdair ?

[javra]

This doesn't go through because it would need an explicit conversion here. I don't immediatly get why the return type is translated as Nat but the argument type as Int 🤔

[ineol]

See my reply below

[Alasdair]

I implemented Alasdair's strategy and it seems to be working. I put the env in the context we already had.

Now, the ranges in parameters are transformed into atom in the enviroment somehow, and so are translated to Int. I guess for consistency we should translate them in the same way. Do you know what is going on @Alasdair ?

In general the type range(X, Y) will be converted into int('n) with the constraint X <= 'n <= Y. For historical reasons the int type with a single parameter is refered to as atom internally, but that isn't really visible to users. We do this canonicalisation step mostly just to ensure that different ways of writing a function type (with a range, explicit constraint, etc) all get mapped to the same thing and therefore get handled consistently.

[ineol]

I updated the PR to also try to prove that parameters/atoms are non-negative. What do you think?