经验证的正确收据模块

我正在研究一种当顾客购买物品时产生收据的登记册。作为练习,我正在考虑在Coq中创建一个收据模块,它不会产生错误的收据。简而言之,收据上的物品和付款总额应始终为0(如果物品的价格大于0,付款金额小于0)。这是可行的还是明智的?

为了快速绘制草图,收据将包括收据项目和付款,如

type receipt = {
  items : item list;
  payments : payment list
}

还有添加物品和付款的功能

add_article(receipt, article, quantity)
add_payment(receipt, payment)

在现实生活中,这个过程当然更加复杂,增加了不同类型的折扣等。

当然,添加布尔函数很容易 check_receipt 确认收据正确。既然文章和付款总是在运行时添加,也许这是唯一的方法?

例子:

receipt = {
  items = [{name = "article1"; price = "10"; quantity = "2"}];
  payments = [{payment_type = Cash; amount = (-20)}];
}

清楚我想要什么吗?

或者证明正确的增值税计算更有趣。有几个这样的财产可以被证明。