CODEWITHSUNDEEP
isabelle
l7ll7
l7ll7

Reputation: 1329

Proving the cardinality of a more involved set

Supposing I have a set involving three conjunctions {k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2}.

How can I prove in Isabelle that the cardinality of this set is 1 ? (Namely only k=6 has gcd 3 6 = 2.) I.e., how can I prove lemma a_set : "card {k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2} = 1" ?

Using sledgehammer (or try) again doesn't yield results - I find it very difficult to find what exactly I need to give the proof methods to make them able to to the proof. (Even removing, e.g. gcd 3 k = 2, doesn't make it amenable to auto or sledgehammer.)

Upvotes: 0

Views: 240

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

Your proposition is incorrect. The set you described is actually empty, as gcd 3 6 = 3. Sledgehammer can prove that the cardinality is zero without problems, although the resulting proof is again a bit ugly, as is often the case with Sledgehammer proofs:

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))

Let's do it by hand, just to illustrate how to do it. These sorts of proofs do tend to get a little ugly, especially when you don't know the system well. 

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

Another, much simpler way (but also perhaps more dubious one) would be to use eval. This uses the code generator as an oracle, i.e. it compiles the expression to ML code, compiles it, runs it, looks if the result is True, and then accepts this as a theorem without going through the Isabelle kernel like for normal proofs. One should think twice before using this, in my opinion, but for toy examples, it is perfectly all right:

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

Note that I had to massage the set a bit first (use Set.filter instead of the set comprehension) in order for eval to accept it. (Code generation can be a bit tricky)

UPDATE:

For the other statement from the comments, the proof has to look like this:

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)

The reason why this looks so different is because the right-hand side of the goal is no longer simply {}, so safe behaves differently and generates a pretty complicated mess of subgoals (just look at the proof state after the proof safe). With intro equalityI subsetI, we essentially just say that we want to prove that A = B by proving a ∈ A ⟹ a ∈ B and the other way round for arbitrary a. This is probably more robust than safe.

Upvotes: 2

Related Questions