證明更多的集合的基數

Question

假設我有一個包含三個連詞{k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2}的集合。

我如何在Isabelle中證明這個集合的基數是1？ （即只有k = 6有gcd 3 6 = 2）也就是說，我該如何證明lemma a_set : "card {k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2} = 1"？

使用sledgehammer（或try）再次不會產生結果 - 我發現很難找到我需要給出的證明方法使他們能夠證明什麼。 （即使刪除，例如gcd 3 k = 2，也不適用於auto或sledgehammer。）

Answer 1

您的建議是不正確的。你描述的集合實際上是空的，如gcd 3 6 = 3。大錘可以證明基數爲零沒有問題，但所得到的證據又是醜了一點，這是常有用大錘證據的情況下：

lemma "card {k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2} = 0" 
    by (metis (mono_tags, lifting) card.empty coprime_Suc_nat 
     empty_Collect_eq eval_nat_numeral(3) gcd_nat.left_idem 
     numeral_One numeral_eq_iff semiring_norm(85)) 

讓我們手工做的，只是爲了說明如何做到這一點。這些證據往往會變得有點難看，特別是當你不瞭解系統時。

lemma "{k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2} = {}" 
proof safe 
    fix x :: nat 
    assume "x > 2" "x ≤ 7" "gcd 3 x = 2" 
    from ‹x > 2› and ‹x ≤ 7› have "x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7" by auto 
    with ‹gcd 3 x = 2› show "x ∈ {}" by (auto simp: gcd_non_0_nat) 
qed 

另一個更簡單的方法（但也可能更可疑）將使用eval。它使用代碼生成器作爲一個oracle，即它將表達式編譯爲ML代碼，編譯它，運行它，查看結果是否爲True，然後接受它作爲定理，而不像通常的證明那樣通過Isabelle內核。每個人都應該三思而後利用這一點，在我的觀點之前，但對於玩具的例子，這是完全正確：

lemma "card {k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2} = 0" 
proof - 
    have "{k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2} = Set.filter (λk. gcd 3 k = 2) {2<..7}" 
    by (simp add: Set.filter_def) 
    also have "card … = 0" by eval 
    finally show ?thesis . 
qed 

注意，我不得不有點第一按摩組（使用Set.filter而不是集理解）以便eval接受它。 （代碼生成是一個有點棘手）

UPDATE：

對於從評論其他聲明，證明必須是這樣的：

lemma "{k::nat. 0<k ∧ k ≤ 5 ∧ gcd 5 k = 1} = {1,2,3,4}" 
proof (intro equalityI subsetI) 
    fix x :: nat 
    assume x: "x ∈ {k. 0 < k ∧ k ≤ 5 ∧ coprime 5 k}" 
    from x have "x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5" by auto 
    with x show "x ∈ {1,2,3,4}" by (auto simp: gcd_non_0_nat) 
qed (auto simp: gcd_non_0_nat) 

之所以這樣看起來很不同的是因爲球門右側不再是簡單的{}，所以safe的行爲不同，併產生一個相當複雜的子目標混亂（只看proof safe後的證明狀態）。與intro equalityI subsetI，我們基本上只是說，我們要證明A = B通過證明a ∈ A ⟹ a ∈ B和其他方式任意a。這可能比safe更可靠。