Hi Nicolas,
It seems like we could refine the first parameter of carryPropagate just as the second: make an= type N1 that only admits values [1..].
How? newtype N1 = N1 Int (put that in a module and don't export N1) define the constant 2, define the increment operator, change div and mod. Now we've mainly got a proof in the type checker, but we still don't actually have a proof for our core N1 definition - but I think that is probably ok, provided it is a common core which can be reused and is minimal.
Would not that suffice to prove that base is never 0 and not have to go beyond the type-checker for a proof?
We've now encoded some properties in the type checker, changed most of the code, and still don't actually have a complete proof. Maybe the type checker isn't a proof tool ;) Thanks Neil