Multiplication of Fin numbers?

Stream: Is there code for X?

[Ayhon]

I was looking for an instance of HMul (Fin n) (Fin m) (Fin ((n-1)*(m-1) + 1)) in Mathlib, but couldn't find anything sort of similar. In general it seems like the usual arithmetic operations are not supported with Fin. Am I simply looking the wrong way?

[Ayhon]

I'm using this to prove some properties on indices, the instance I'm actually interested in is HMul (Fin (2^h)) (Fin 3) (Fin (2^(h+1) - 1)) to show that if i: Fin (2^h) then 2*i: Fin (2^(h+1)) and 2*i + 1: Fin (2^(h+1)).

[Edward van de Meent]

if you want some kind of index pairing, i think using Prod should do, no?

[Ayhon]

Sorry, I'm not sure what you mean exactly. I'm quite new to Lean, this is the first project I'm developping with it

[Ayhon]

Isn't Prod used to make tuples? How does it relate?

[Edward van de Meent]

i suppose my suggestion was a bit hasty... i was in the middle of being surprised that there would be a use for multiplication of Fin...

[Edward van de Meent]

i think it would help to know what larger issue or design having this instance would help you make, because having this instance is (at first glance, to me) not desirable.

[Edward van de Meent]

because this sounds like an #xy problem

[Ayhon]

Hmm, you may be right. Let me give a bit more context into the problem I'm trying to solve.

As a small little project to learn software verification in Lean, I've decided to try to develop a verified implementation of a segment tree. Segment trees are represented by a (2^h) array in memory, which can be indexed by Fin (2^h). In particular, the segment tree stores its leaves in the positions 2^(h-1) to 2^h - 1 of the array, and internal nodes in positions 1 to 2^(h-1) - 1. For a given internal node at position i, its left child is obtained from doing 2*i and its right child from doing 2*i+1.

Basically, the indices describe the path that must be taken from the root to the node, with 0s being left and 1s being right. I would now like to prove that if I'm given an internal node (represented by Fin 2^(h-1)), I can obtain its left or right child, and still have those be valid pointers (represented by Fin 2^h). In particular, I need to show that 2*i + 1 < 2^(h+1) if i < 2^h.

If we represent bounded numbers usingFin n, I thought it to be reasonable to expect an implementation of artihmetic operations which simply adapted the bounds they were subject to as needed. So HAdd (Fin n) (Fin m) (Fin (n+m-1)) for example.

Is there an easier way of working with numbers as strings of bits? I looked at the standard library, and all I could find were definitions like Nat.binaryRec which make it easier to work with natural numbers as if they were so, but not much else.

[Ayhon]

Ideally, I would like to work with Fin (2^h) as if it were a Vector Bool h, while still being able to index the segment tree

[Eric Wieser]

are you looking for docs#BitVector ?

[Edward van de Meent]

docs#BitVec

[Ayhon]

Indeed BitVec is closer to what I was looking for, but I'd like it if addition didn't wrap around the end, but simply extend the amount of bits needed for its representation. I would like not to worry about overflows by proving that the numbers I need respect the required bounds. If this is not usually how this is achieved, is there a different way of doing so?

[Kim Morrison]

Usually it is best to work with total functions (that may have "junk" values in the parts of the domain you don't care about), and then prove theorems about the behaviour of these functions when the inputs satisfy the conditions you care about.

[Kim Morrison]

If that doesn't make sense, you may need to #xy a bit here, as I suspect you may be trying to do "the wrong thing".

[Daniel Weber]

I think you may have an easier time defining a segment tree inductively (only for the proof, not the program), proving everything there, and finally having a few lemmas showing the equivalence of that to a flat representation

[Vincent Beffara]

It sounds like you are doing something like interval arithmetic at the type level which sounds a bit frightening but there has to be a way to automatically propagate bounds through a computation and the overall motivation does feel natural.

[Ayhon]

Daniel Weber said:

I think you may have an easier time defining a segment tree inductively (only for the proof, not the program), proving everything there, and finally having a few lemmas showing the equivalence of that to a flat representation

Actually, that was a bit of my approach. I have a tree implementation of what a segment tree is, without relying on internal details. The thing is, I need these proofs to index the underlying array in the implementation. I guess I could add extra bound checks in the code and later prove that they're not needed, but since I'm already indexing with Fin (2^h) I thought I could use them instead.

[Ayhon]

Vincent Beffara said:

It sounds like you are doing something like interval arithmetic at the type level which sounds a bit frightening but there has to be a way to automatically propagate bounds through a computation and the overall motivation does feel natural.

My original inspiration was this CapNProto security advisory report. I guess what I actually want is the proof that if i < n and j < m then i*j<(n-1)*(m-1)+1, which doesn't really have to be tied to Fin. But it would believe it could be useful to have this done automatically. Although it could just be that I'm biased by my use case. 🤷🏻

[Ayhon]

I'll try to give everyone's suggestions a go once I find the time. Thank you all for your feedback! I think thinking of these implementations as foral functions will help as a general directive to keep in the implementation.