书店

说明

为了鼓励人们更多地购买某套热门系列丛书（该系列共有 5 本）中的不同书籍，一家书店决定，对一次购买多本书的顾客提供折扣。

五本书中任意一本的单价都是 $8。

不过，如果你买两本不同的书，这两本能享受 5% 的折扣。

如果买 3 本不同的书，能享受 10% 的折扣。

如果买 4 本不同的书，能享受 20% 的折扣。

如果 5 本全买，能享受 25% 的折扣。

注意，如果你买了 4 本，其中 3 本是不同的书名，那么能组成一个套组的这 3 本可以享受 10% 的折扣，但第四本仍然是 $8。

你的任务是编写代码，计算任意一个可能出现的购物篮的价格（其中只包含同一系列的书籍），并尽可能给出最大的折扣。

例如，下面这个购物篮里的书要多少钱？

• 第一本 2 册
• 第二本 2 册
• 第三本 2 册
• 第四本 1 册
• 第五本 1 册

对这 8 本书的一种分组方式是：

• 1 组 5 本（第 1、2、3、4、5 本）
• 1 组 3 本（第 1、2、3 本）

这样总共是：

• 5 本书享受 25% 的折扣
• 3 本书享受 10% 的折扣

结果是：

• 5 × (100% - 25%) × $8 = 5 × $6.00 = $30.00，加上
• 3 × (100% - 10%) × $8 = 3 × $7.20 = $21.60

总计 $51.60。

不过，这 8 本书还有另一种分组方式：

• 1 组 4 本（第 1、2、3、4 本）
• 1 组 4 本（第 1、2、3、5 本）

这样总共是：

• 4 本书享受 20% 的折扣
• 4 本书享受 20% 的折扣

结果是：

• 4 × (100% - 20%) × $8 = 4 × $6.40 = $25.60，加上
• 4 × (100% - 20%) × $8 = 4 × $6.40 = $25.60

总计 $51.20。

而 $51.20 就是折扣最大的价格。

子类型

本练习定义了一个名为Book的子类型，对应自然数 1 到 5。 可以把子类型看作一个二元组⟨x, h⟩，其中 x 是值，h 是它有效性的证明。

子类型内部的值（这里是 x）可以通过 .val 访问，例如x.val。 它的证明可以通过 .property 访问，例如x.property。 两者也都可以照常通过模式匹配访问。

---

来源

灵感来自 Cyber-Dojo 上的 harry potter kata。