Menu
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?
531
In calculus, an antiderivative, inverse derivative, primitive function, primitive integral or indefinite integral of a function f is a differentiable function F whose derivative is equal to the original function f. This can be stated symbolically as F' = f.
Def 1.1 A function f(x1,...,xn) is primitive recursive if either: 1. f is the function that is always 0, i.e. f(x1,...,xn) = 0; This is denoted by Z when the number of arguments is understood. This rule for deriving a primitive recursive function is called the Zero rule.
Definition 1 (Primitive function). If I ⊆ R is a non-empty open interval and F, f : I → R are functions satisfying F = f on I, we call F a primitive function of f on I.
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...
189
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
