더 많은 관련 집합의 카디널리티 증명

Question

세 개의 연결을 포함하는 집합이 있다고 가정하면 {k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2}입니다.

이 세트의 카디널리티가 1이라고 Isabelle에서 어떻게 증명할 수 있습니까? (즉 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을 사용하는 것이 훨씬 간단합니다 (그러나 더 모호한 경우도 있음). 이것은 코드 생성기를 오라클로 사용합니다. 즉, 표현식을 ML 코드로 컴파일하고 컴파일 한 다음 실행하고 결과가 True인지 확인한 다음 일반 교정본처럼 Isabelle 커널을 거치지 않고 정리로 사용합니다. 하나는 내 의견으로는, 이것을 사용하기 전에 두 번 생각해야하지만, 장난감 예를 들어, 완벽하게 모든 권리이다 (대신 세트 이해의 Set.filter 사용)

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 

주 내가 조금 먼저 세트를 마사지했다 그 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 ∈ A ⟹ a ∈ B을 증명함으로써 A = B을 증명하기를 원한다고 말하고 임의의 다른 방법으로는 a을 반올림합니다. 이것은 아마도 safe보다 강력합니다.