完全數

說明

根據尼各馬科斯（公元 60 年至 120 年）為正整數提出的分類法，判斷一個數字是 perfect、abundant 還是 deficient。

古希臘數學家尼各馬科斯為正整數設計了一套分類法，並依照每個數的真因數和，把它唯一歸入 perfect、abundant 或 deficient 其中一個類別。 「真因數和」的定義是：一個數字的所有因數（不包含這個數字本身）的總和。 例如，15 的真因數和是 1 + 3 + 5 = 9。

Perfect

一個數字等於它的真因數和時，就是 perfect。 例如：

• 6 是 perfect 數，因為 1 + 2 + 3 = 6
• 28 是 perfect 數，因為 1 + 2 + 4 + 7 + 14 = 28

Abundant

一個數字小於它的真因數和時，就是 abundant。 例如：

• 12 是 abundant 數，因為 1 + 2 + 3 + 4 + 6 = 16
• 24 是 abundant 數，因為 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36

Deficient

一個數字大於它的真因數和時，就是 deficient。 例如：

• 8 是 deficient 數，因為 1 + 2 + 4 = 7
• 質數都是 deficient

任務

實作出判斷給定數字是否為 perfect 的方法。 依你的語言軌道而定，你可能還需要實作出判斷給定數字是否為 abundant 或 deficient 的方法。

定義歸納型別

這個練習預期回傳值是一個你必須自行定義的歸納型別Classification。

這個型別必須有 BEq 執行個體，也就是說，它要能進行布林相等性測試；還必須有 Repr 執行個體，也就是說，這個型別的值可以格式化以供顯示。

你可以參考這個頁面，了解執行個體宣告。 Lean 可以自動為許多類別產生執行個體。

子型別

classify函式的引數是一個名為Positive的子型別：

def Positive := { x : Nat // x > 0 }

子型別代表某個特定型別中滿足述詞的元素。 Positive代表Nat中大於0的元素。

子型別的任何元素都可以想成一組配對：一個底層型別的值，加上一個數學意義上的證明，證明這個值滿足對應的述詞。

子型別在型別層級強制維持不變式，確保無法建構出格式錯誤的值。

---

出處

摘自 Neal Ford 所著《Functional Thinking》第 2 章。