what is (17 : fin 2)?

Stream: general

[Alex Kontorovich]

Why doesn't Lean just tell me this is nonsense? It won't accept (banana : fin 2) but it's accepting 17, and I don't know what that's supposed to mean. (Will Lean 4 be any different in this respect?) Just curious, thanks!

[Mario Carneiro]

Does #eval work?

[Mario Carneiro]

Anyway it's defined with wrapping arithmetic, so it is 1

[Mario Carneiro]

There is a PR in the pipes to change it to saturating arithmetic but it will still be 1 in that case

[Mario Carneiro]

#eval (17 : fin 2) -- 1

[Mario Carneiro]

As for why lean doesn't say it's nonsense, it's because numerals in lean desugar to applications of the bit0 and bit1 functions that are defined on anything with a 1 and a +

[Mario Carneiro]

this approach doesn't leave any room for saying that some numerals are okay and others are not, you either get all numerals or none

[Mario Carneiro]

as for whether lean 4 will change things, it's not clear. The approach is different - there is a class OfNat A n that inhabits each particular numeral, so in principle we could have instances OfNat (fin 17) 0 , ...OfNat (fin 17) 16 with no more, and then you will only be able to use these numerals, but it's not yet clear how to get families of instances parameterized by decidable arithmetic predicates like this (we would want instance (h : m < n) : OfNat (fin n) m here but that needs typeclass inference to prove m < n somehow).

[Simon Hudon]

Lean 4 has less room to "somehow prove something" in type class search as it is no longer supposed to invoke the tactic framework. The only option that I know of is to use an instance of Fact (n < m)

[Mario Carneiro]

Well it doesn't need to invoke "tactics" per se, there are a bunch of monads now, we just need the relevant one to have extensible rules, possibly with a caveat that any extensions need to be pure-functional and possibly some other properties, and the user is responsible for any slowdown that results. Lean 3 can't call tactics either, and especially when it comes to dealing with kernel literals the alternative to "computed instances" is a sort of prolog-programming in instance search which is almost guaranteed to have worse performance and probably a worse result too (a needlessly complicated instance term coming out, that affects downstream elaboration).