CODEWITHSUNDEEP
isabelle
l7ll7
l7ll7

Reputation: 1329

Proving the cardinality of a finite set

How can I prove in Isabelle the simple lemma cd : "card {m∈ℕ. m <4} = 4" statement?

auto doesn't help me and oddly sledgehammer times out (even if I use different values on the right-hand side, like 3 or 5 to make sure that I haven't overlooked some technical Isabelle details which perhaps actually make the cardinaliy evaluate to one of these numbers.)

I have the impression that I have to use some lemmas (or get inspiration) from Set_Interval.thy as there sets of these kind are extensively used, but so far I didn't manage to make progress.

Upvotes: 2

Views: 534

Answers (2)

ammbauer
ammbauer

Reputation: 426

Just wanted to add, that if you rewrite your lemma to "card {m::nat. m < n} = n", Isabelle has no problem proving it.

*Edited, thanks Manuel.

Upvotes: 4

Manuel Eberl
Manuel Eberl

Reputation: 8278

The problem with your statement is that it is not true. Look at the definition of ℕ with thm Nats_def: ℕ = range of_nat

of_nat is the canonical homomorphism from the naturals into a semiring_1, i.e. a semiring that has a 1. The definition of ℕ basically says that ℕ consists of all the elements of the ring that are of the form of_nat n for a natural number n. If you look at the type of {m∈ℕ. m <4}, you will see that it is 'a, or if you do a declare [[show_sorts]] before it, 'a :: {ord, semiring_1}, i.e. a semiring with a 1 and some kind of ordering on it. This ordering does not have to be compatible with the ring structure, nor does it have to be linear.

You may think that the set you defined is always the set {0, 1, 2, 3}, but because the ordering is not required to be compatible with the ring structure, this is not the case. The ordering could be trivially true, so you'll get all natural numbers.

Furthermore, even when the set is {0, 1, 2, 3}, its cardinality is not necessarily 4. (Think of the ring ℤ/2ℤ – then that set will be equal to {0, 1}, so the cardinality is 2)

You will probably want to restrict the type of your expression a bit. I think the right type class here is linordered_semidom, i.e. a semiring with a 1, no zero divisors, and a linear ordering that is compatible to the ring structure. Then you can do:

lemma cd : "card {m∈ℕ. m < (4 :: 'a :: linordered_semidom)} = 4"
proof -
  have "{m∈ℕ. m < (4 :: 'a)} = {m∈ℕ. m < (of_nat 4 :: 'a)}" by simp
  also have "… = of_nat ` {m. m < 4}"
    unfolding Nats_def by (auto simp del: of_nat_numeral)
  also have "card … = 4" by (auto simp: inj_on_def card_image)
  finally show ?thesis .
qed

The proof is a bit ugly considering how intuitively obvious the proposition is; the solution here is not to write down the set you want to describe in this relatively inconvenient way in the first place. It takes a bit of experience to know how to write things in a convenient way.

Upvotes: 2

Related Questions