Доказательство мощности более задействованного набора

Question

Предположим, у меня есть набор, включающий три конъюнкции {k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2}.

Как я могу доказать в Изабель, что мощность этого множества равна 1? (А именно, только k = 6 имеет gcd 3 6 = 2.) I. Как я могу доказать 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. Кувалда может доказать, что мощность равна нулю без проблем, хотя в результате доказательство снова немного некрасиво, как это часто бывает с Sledgehammer доказательствами:

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, а затем принимает это как теорему, не просматривая ядро ​​Изабель, как для нормальных доказательств. Следует дважды подумать, прежде чем использовать это, на мой взгляд, но игрушечные примеры, это совершенно правильно:

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.