當函數返回1時，函數返回0，消除不合格

Question

考慮以下Isabelle的最小工作示例，其中我定義了兩個不同的函數func1和func2，它們應該模擬Eulers Totient函數。
奇怪的是，明顯的定義是錯誤的，並通過引入∈ℕ導致正確的，但尚未確定的定義，只是略微改變了定義。
（我穿插代碼的確切問題，因爲這使得它可能更清楚我所指的）。

theory T 
    imports 
    Complex_Main 
    "~~/src/HOL/Number_Theory/Number_Theory" 
    begin 

(* Part I*) 

definition func1 :: "nat ⇒ nat" 
    where "func1 n = card {m. m≤n ∧ coprime n m}" 

lemma func1_equals : "func1 1 = 2" (* This equation is obviously false...*) 
    by (auto simp: func1_def) 

    (* Question 1: Why is this proof correct according to Isabelle? *) 

(* Part II*)  

definition func2 :: "nat ⇒ nat" 
    where "func2 n = card {m. m∈ℕ ∧ m≤n ∧(coprime n m)}" 
(* Slightly changed definition by incorporating ∈ℕ*) 

lemma func2_equals : "func2 1 = 1" 
    apply (auto simp: func2_def) 
(* Unproved subgoal <<card {m ∈ ℕ. m ≤ Suc 0} = Suc >> looks more promising *) 
    oops 

    (* Question 2: Which proof method should I use to prove the last lemma? 
Interestingly, sledgehammer runs out of time...*) 
    Question 3: Analogous to Q2 but for func2 4 = 2 ? The difference now is that 
the preliminary <<apply (auto simp: func2_def)>> rewrites to a slightly 
different subgoal. *) 

end 

有沒有更好的方法來定義歐拉總功能？

Answer 1

你的兩個定義是等價的：

lemma "func1 n = func2 n" 
    by (simp add: func1_def func2_def Nats_def) 

你之所以得到2，而不是1是一個微妙的和那種你運行，當你正式的數學定義成問題的一個很好的例子：自然Isabelle中的數字包含0，因此如果您評估func1 1，請查看不大於1 - 0和1的數字 - 並檢查它們中的哪一個互質爲1.由於gcd 0 n = n對於所有n，您會發現0和1都是coprime爲1，因此結果爲2.

歐拉函數只計算積極整數小於n是互質到n，所以你的定義應該看起來更像是這樣的：

definition totient :: "nat ⇒ nat" where 
    "totient n = card {k ∈ {0<..n}. coprime k n}" 

如果你想生成代碼的工作，你可以使用下面的碼公式：

lemma totient_code [code]: "totient n = card (Set.filter (λk. coprime k n) {0<..n})" 
    by (simp add: totient_def Set.filter_def) 

然後，你可以這樣做：

value "map (int ∘ totient) [1..<10]" 
(* Output: "[1, 1, 2, 2, 4, 2, 6, 4, 6]" :: "int list" *) 

請注意，雖然我認爲總體功能在Isabelle中是非常好的，但我不確定這是對初學者來說最好的考慮，因爲涉及套基和這些東西的證明可能會涉及一些問題。瞭解該系統的一個好方法是Nipkow和Klein的免費博客。這本書中的例子和練習是更多的計算機科學/面向程序設計的，但是材料更適合於初學者，並且更適合於交互式定理證明，因爲證明傾向於減少混亂並且需要較少的系統經驗。

而且，順便說一句，sledgehammer未能證明func2 1 = 1的原因是因爲結果是2而不是1。你可以通過展開unfolding Nats_def或者將Nats_def添加到簡寫集simp add:來證明通過展開ℕ的定義（其對於自然數基本上就是UNIV），如上所述。