Isabelle structure proof

Question

There is a set of some structures. I'm trying to prove that the cardinality of the set equals some number. Full theory is too long to post here. So here is a simplified one just to show the idea.

Let the objects (which I need to count) are sets containing natural numbers from 1 to n. The idea of the proof is as follows. I define a function which transforms sets to lists of 0 and 1. Here is the function and its inverse:

fun set_to_bitmap :: "nat set ⇒ nat ⇒ nat ⇒ nat list" where
  "set_to_bitmap xs x 0 = []"
| "set_to_bitmap xs x (Suc n) =
    (if x ∈ xs then Suc 0 else 0) # set_to_bitmap xs (Suc x) n"

fun bitmap_to_set :: "nat list ⇒ nat ⇒ nat set" where
  "bitmap_to_set [] n = {}"
| "bitmap_to_set (x#xs) n =
    (if x = Suc 0 then {n} else {}) ∪ bitmap_to_set xs (Suc n)"

value "set_to_bitmap {1,3,7,8} 1 8"
value "bitmap_to_set (set_to_bitmap {1,3,7,8} 1 8) 1"

Then I plan to prove that 1) a number of 0/1 lists with length n equals 2^^n, 2) the functions are bijections, 3) so the cardinality of the original set is 2^^n too.

Here are some auxiliary definitions and lemmas, which seems useful:

definition "valid_set xs n ≡ (∀a. a ∈ xs ⟶ 0 < a ∧ a ≤ n)"
definition "valid_bitmap ps n ≡ length ps = n ∧ set ps ⊆ {0, Suc 0}"

lemma length_set_to_bitmap:
  "valid_set xs n ⟹
   x = Suc 0 ⟹
   length (set_to_bitmap xs x n) = n"
  apply (induct xs x n rule: set_to_bitmap.induct)
  apply simp
  sorry

lemma bitmap_members:
  "valid_set xs n ⟹
   x = Suc 0 ⟹
   set_to_bitmap xs x n = ps ⟹
   set ps ⊆ {0, Suc 0}"
  apply (induct xs x n arbitrary: ps rule: set_to_bitmap.induct)
  apply simp
  sorry

lemma valid_set_to_valid_bitmap:
  "valid_set xs n ⟹
   x = Suc 0 ⟹
   set_to_bitmap xs x n = ps ⟹
   valid_bitmap ps n"
  unfolding valid_bitmap_def
  using bitmap_members length_set_to_bitmap by auto

lemma valid_bitmap_to_valid_set:
  "valid_bitmap ps n ⟹
   x = Suc 0 ⟹
   bitmap_to_set ps x = xs ⟹
   valid_set xs n"
  sorry

lemma set_to_bitmap_inj:
  "valid_set xs n ⟹
   valid_set xy n ⟹
   x = Suc 0 ⟹
   set_to_bitmap xs x n = ps ⟹
   set_to_bitmap ys x n = qs ⟹
   ps = qs ⟹
   xs = ys"
  sorry

lemma set_to_bitmap_surj:
  "valid_bitmap ps n ⟹
   x = Suc 0 ⟹
   ∃xs. set_to_bitmap xs x n = ps"
  sorry

lemma bitmap_to_set_to_bitmap_id:
  "valid_set xs n ⟹
   x = Suc 0 ⟹
   bitmap_to_set (set_to_bitmap xs x n) x = xs"
  sorry

lemma set_to_bitmap_to_set_id:
  "valid_bitmap ps n ⟹
   x = Suc 0 ⟹
   set_to_bitmap (bitmap_to_set ps x) x n = ps"
  sorry

Here is a final lemma:

lemma valid_set_size:
  "card {xs. valid_set xs n} = 2 ^^ n"

Does this approach seem valid? Are there any examples of such a proof? Could you suggest an idea on how to prove the lemmas? I'm stuck because the induction with set_to_bitmap.induct seems to be not applicable here.

Answer 1

In principle, that kind of approach does work: if you have a function f from a set A to a set B and an inverse function to it, you can prove bij_betw f A B (read: f is a bijection from A to B), and that then implies card A = card B.

However, there are a few comments that I have:

1. You should use bool lists instead of nat lists if you can only have 0 or 1 in them anyway.

2. It is usually better to use existing library functions than to define new ones yourself. Your two functions could be defined using library functions like this:

   set_to_bitmap :: nat ⇒ nat ⇒ nat set ⇒ bool list
   set_to_bitmap x n A = map (λi. i ∈ A) [x..<x+n]
   
   bitmap_to_set :: nat ⇒ bool list ⇒ nat set
   bitmap_to_set n xs = (λi. i + n) ` {i. i < length xs ∧ xs ! i}```
   
   

3. Side note: I would use upper-case letters for sets, not something like xs (which is usually used for lists).

4. Perhaps this is because you simplified your problem, but in its present form, valid_set A n is simply the same as A ⊆ {1..n} and the {A. valid_set A n} is simply Pow {1..n}. The cardinality of that is easy to show with results from the library:

   lemma "card (Pow {1..(n::nat)}) = 2 ^ n"
     by (simp add: card_Pow)`
   

As for your original questions: Your first few lemmas are provable, but for the induction to go through, you have to get rid of some of the unneeded assumptions first. The x = Suc 0 is the worst one – there is no way you can use induction if you have that as an assumption, because as soon as you do one induction step, you increase x by 1 and so you won't be able to apply your induction hypothesis. The following versions of your first three lemmas go through easily:

lemma length_set_to_bitmap:
  "length (set_to_bitmap xs x n) = n"
  by (induct xs x n rule: set_to_bitmap.induct) auto

lemma bitmap_members:
  "set (set_to_bitmap xs x n) ⊆ {0, Suc 0}"
  by (induct xs x n rule: set_to_bitmap.induct) auto

lemma valid_set_to_valid_bitmap: "valid_bitmap (set_to_bitmap xs x n) n"
  unfolding valid_bitmap_def
  using bitmap_members length_set_to_bitmap by auto

I also recommend not adding "abbreviations" like ps = set_to_bitmap xs x n as an assumption. It doesn't break anything, but it tends to complicate things needlessly.

The next lemma is a bit trickier. Due to your recursive definitions, you have to generalise the lemma first (valid_bitmap requires the set to be in the range from 1 to n, but once you make one induction step it has to be from 2 to n). The following works:

lemma valid_bitmap_to_valid_set_aux:
  "bitmap_to_set ps x ⊆ {x..<x + length ps}"
  by (induction ps x rule: bitmap_to_set.induct)
     (auto simp: valid_bitmap_def valid_set_def)

lemma valid_bitmap_to_valid_set:
  "valid_bitmap ps n ⟹ valid_set (bitmap_to_set ps 1) n"
  using valid_bitmap_to_valid_set_aux unfolding valid_bitmap_def valid_set_def
  by force

Injectivity and surjectivity (which is your ultimate goal) should follow from the fact that the two are inverse functions. Proving that will probably be doable with induction, but will require a few generalisations and auxiliary lemmas. It should be easier if you stick to the non-recursive definition using library functions that I sketched above.