I'm working on a register which produces receipts when customers buy articles. As an exercise, I'm thinking about making a receipt module in Coq which cannot produce erroneous receipts. In short, the articles and the payments on the receipt should always sum to 0 (where articles have price > 0 and payments have amount < 0). Is this doable, or sensible?
To do a quick sketch, a receipt would consist of receipt items and payments, like
type receipt = {
items : item list;
payments : payment list
}
And there would be functions to add articles and payments
add_article(receipt, article, quantity)
add_payment(receipt, payment)
In real life, this procedure is of course more complicated, adding different types of discounts etc.
Certainly it's easy to add a boolean function check_receipt that confirms that the receipt is correct. And since articles and payments always is added in runtime, maybe this is the only way?
Example:
receipt = {
items = [{name = "article1"; price = "10"; quantity = "2"}];
payments = [{payment_type = Cash; amount = (-20)}];
}
Is it clear what I want?
Or maybe it's more interesting to prove correct VAT calculations. There's a couple of such properties that could be proven.
