Helper lemmas for termination proofs for UInt types

Stream: Is there code for X?

[cmlsharp]

There are several lemmas that it would be convenient to have on, say, UInt64 such as 'n \neq 0 => (n - 1) < n`. These are of course not difficult to prove, but they are the types of things I'd have hoped would be in the standard library somewhere (analogous lemmas exist for Nats).

Do these exist somewhere?

[Yaël Dillies]

Is this true? What if n - 1 underflows?

[Jakub Nowak]

Yaël Dillies said:

Is this true? What if n - 1 underflows?

It can't with n ≠ 0 assumption.

[Henrik Böving]

You're looking for docs#UInt64.sub_lt I think?

[Henrik Böving]

example (n : UInt64) (h : n ≠ 0) : n - 1 < n := by
  apply UInt64.sub_lt
  · decide
  · lia

[Jakub Nowak]

We probably should add Uint64.sub_one_lt to API, to match the analogous Nat lemma.

[Jakub Nowak]

@cmlsharp It would be helpful, if you could list other missing lemmas.

[Henrik Böving]

I'll leave that call to Markus

[Yaël Dillies]

Aah sorry, you're talking about unsigned integers. I just call these naturals :grinning_face_with_smiling_eyes:

[cmlsharp]

I'll try put together a list when I get back to my laptop. In general, just from a usability perspective it would be nice if there were analogous UInt* lemmas with identical names for all applicable Nat lemmas (resp Int*/Int lemmas).

[cmlsharp]

This is something I'd be willing to submit as a PR to the standard library if there's interest in that.

[Matt Diamond]

Could we avoid redundancy by defining these lemmas for a class of mathematical objects that includes both Nat and UInt64? It might be nicer to generalize instead of duplicate.

[Jakub Nowak]

Matt Diamond said:

Could we avoid redundancy by defining these lemmas for a class of mathematical objects that includes both Nat and UInt64? It might be nicer to generalize instead of duplicate.

It would make finding the theorems on loogle harder though.

[Matt Diamond]

would it? I figure you could just search for ?a - 1 < ?a

[Matt Diamond]

also if we follow naming conventions (e.g. sub_one_lt_self_iff_ne_bot) it might not even require searching Loogle

[Jakub Nowak]

E.g. 0 < ?_ timeouts, but Nat, 0 < ?_ doesn't. Also, if your pattern doesn't include numeral literals, than you might need to add Nat to query, to filter out irrelevant lemmas.

[Matt Diamond]

would be cool if Loogle could use instance synthesis as part of its search

[Aaron Liu]

Matt Diamond said:

would be cool if Loogle could use instance synthesis as part of its search

Can you elaborate a bit on this?

[Jakub Nowak]

I think, that if I use A in search, then loogle shoud be able to find theorems for classes, which A is instance of. E.g. if I search for Nat, ?a ≤ max ?a ?b it will find only Nat.le_max_left. But it won't find le_max_left. It only worked here, because le_max_left was duplicated for Nat.

[Matt Diamond]

yeah it might be (effectively) impossible but the idea would be that if your search includes Nat then Loogle will include lemmas that don't mention Nat explicitly but have typeclass requirements that Nat satisfies

[Aaron Liu]

like exact??

[Matt Diamond]

hmm... yeah I suppose so

[Jakub Nowak]

Matt Diamond said:

Could we avoid redundancy by defining these lemmas for a class of mathematical objects that includes both Nat and UInt64? It might be nicer to generalize instead of duplicate.

It would also make it impossible to use dot notation.

[cmlsharp]

Ah that would be rather unfortunate as well. One perhaps unsatisfying option is just to use metaprogramming for this rather than class instances. Think for example what Rust does for its various integral types. There’s no “trait” that gives i64, i32, i16, etc a “unsigned_abs” method, rather concrete implementations are created via macro.

On the one hand, sure it is unsatisfying because you can’t really abstract over these in the conventional way, but you still get the duplication-saving benefits. I think for the rather small handful of primitive types in the standard library this more ad hoc approach is fine (but I’m new to the lean ecosystem, so perhaps this is a serious faux pas)

[Jakub Nowak]

There are already macros for UInt: https://github.com/leanprover/lean4/blob/b87d2c0fb9c16d73571a208a08af1967450e7b87/src/Init/Data/UInt/Lemmas.lean#L26