Primitive operations in proofs

Question

For learning dependent types, I'm rewriting my old Haskell game in Idris. Currently the game „engine“ uses builtin integral types, such as Word8. I'd want to prove some lemmas involving numerical properties of those numbers (such as, that double negation is identity). However, it's not possible to say something about behaviour of primitive arithmetic operations. What would be better, to just use believe_me or other handwaving (at least for the most basic properties), or to rewrite my code using Nat, Fin and other „high-level“ numerical types?

Answer 1

I'd suggest using postulate for any of the primitive properties you need, being careful only to use things which are actually true for the numerical types in question, of course (which basically just means being careful about overflow). So you can say things like:

postulate add_commutes : (x, y : Int) -> x + y = y + x

believe_me is best avoided unless you need some computation behaviour of the proof. But, to be honest, we're still trying to work this stuff out when reasoning about primitives...

Answer 2

I believe for the moment it's generally better to use Nat when you can. The Idris devs are planning, eventually, to implement a general mechanism for replacing proof-friendly types with fast primitive ones in compilation, but for now that only happens for Nat. You could believe_me through if you really wanted, but you'd end up with functions that are not so easy to work with in proofs. Note that if you decide to play with believe_me, then you should consider also really_believe_me, which apparently makes it more believable to the type checker.