Tuply singleton v3 (with proof)

In my previous post, I had a different approach to Tuply singleton.

This is the third and last post in the Tuply singleton series. We will provide mathematical proof for correctness, and also show a generalized formula.

We will now show the mathematical proof for Tuply singleton v2. The gist of the proof is that we will consider two pairs, and we’ll be using the least nonzero difference of the second element of each pair and show that it will always be bigger than the constraint we added to the first element of each pair.

We’re trying to prove for .

• : Suppose . Then and we’re done.
• : Suppose , i.e. . If we take of both sides, we get:
  

  Note that must be in . Thus, the maximal difference allowed is 5. Also note that .

  Now, suppose that . Then , which isn’t allowed. Thus the difference is too large. And are integers, so the only smaller difference is when , which implies .

Now our Tuply singleton formula can further be generalized to just with the following constraints: , , – some upper bound n, .

Validity:

> isFormulaValid (\x1 x2 -> x1 + 5.1 * fromIntegral x2))
True
> isFormulaValid (\x1 x2 -> x1 + 5 * fromIntegral x2))
False

Haskell code:

mkFuns
  :: Integer
     -> Double
     -> (Double -> Integer -> Double, Double -> Double,
         Double -> Integer)
mkFuns n k = if k <= fromIntegral n then error "k must be > n" else (mkPair, fst', snd')
    where
    mkPair :: Double -> Integer -> Double
    mkPair a b = if a > k || a < 0 then error "Out of bounds" else a + fromIntegral (n * b)
    fst' :: Double -> Double
    fst' x = if x > fromIntegral n then fst' (x - fromIntegral n) else x
    snd' :: Double -> Integer
    snd' x = round $ (x - fst' x) / fromIntegral n

And finally, usage:

> let (mkPair, fst', snd') = mkFuns 5 5.1
> fst' $ mkPair 3 7
3.0
> snd' $ mkPair 3 7
7

Thanks to greenbagels from ##math@freenode for their help on the proof.