RFC: Positive integer type with views

Stream: std4

[François G. Dorais]

I have developed a positive integer type that can function simultaneously as:

• A subtype of Nat, so that basic operations can benefit from special handling of Nat.
• An inductive type with one base and one recursive constructor: one = 1 and succ x = x+1.
• An inductive type with one base and two recursive constructors:one = 1, bit0 x = 2*x, bit1 x = 2*x+1.

This is an extension of @Leonardo de Moura's example of type views here (following an old zulip discussion).

Automation for type views doesn't exist yet but it can be done once we have some use cases, such as this!

The RFC is currently available from the pos branch my personal Std4 fork: https://github.com/fgdorais/std4/blob/pos/Std/Data/Pos/Basic.lean

If there is support for this, I will turn it into a PR for Std4.

[François G. Dorais]

For what it's worth, the code generated for Pos.log2 and Pos.log2TR is just as good as what I would generate manually (without knowing about GMP/BigNum support).

[Yury G. Kudryashov]

Note that Mathlib uses name docs#PNat for a similar type.

[François G. Dorais]

Recorded! But doesn't PNat that suggest just the basic subtype structure without the additional views?

[François G. Dorais]

Also Pos does sometimes suggest "position", as in String.Pos, which is another naming issue.

[François G. Dorais]

PS: This is partly from old personal Lean4 stuff prior to Mathlib4 and Std4; my naming convention doesn't fit but I will fix that before submitting a PR.

[François G. Dorais]

What about PInt or PosInt? Added with an easier coercion to Int?

[Yury G. Kudryashov]

What do the views (as custom data structures) add compared to custom recursion/induction principles?

[François G. Dorais]

I'm not sure what you mean? They _are_ the custom recursion/induction principles! However, they are data oriented by design. The idea is to write code like this:

def lg2 (x : Pos) : Nat :=
  match x.toBinView with
  | .one => 0
  | .bit0 x => lg2 x + 1
  | .bit1 x => lg2 x + 1

Right now this works provided the helper lemmas are supplied but that could be automated quite easily.