Cardinality and indicator functions · Beginner Questions

lemma card_indicator:
  fixes U::"'a set"
  fixes P::"'a ⇒ bool"
  assumes "finite U"
  shows  "card { u ∈ U .   (P u)} =  (∑ u ∈ U  .  (if (P u) then 1 else 0))" by sledgehammer

I was trying to mimic a Lean proof that if I have three 2-element subsets of a 4-element set U, then at least one element of U appears in at least two of them.; that proof starts out with this:

 (U : Type _) [Fintype U]
 (U_card : Fintype.card U = 4)
 -- `f` is an indicator function, mapping each element of `U` to the set of indices
 -- of sets that contain that element.
 (f : U → Finset (Fin 3))
 -- Each of those sets contains exactly two elements.
 (h : ∀ n : Fin 3, #{x : U | n ∈ f x} = 2) :
 -- There is some element `u : U` that is an element of two distinct sets:
 -- that is, `f u` contains two distinct indices.
 ∃ (u : U) (x y : Fin 3), x ≠ y ∧ x ∈ f u ∧ y ∈ f u := by -- begin our proof

 -- the elements of `U` appear in the three sets with multiplicity 6,
 -- since each set has cardinality 2
 have h1 : ∑ n : Fin 3, #{x : U | n ∈ f x} = 6
 · simp [h]

 -- we can also express this as a sum of sums of indicator functions;
 -- importantly, we can swap the sum operators.
 have h2 : ∑ n : Fin 3, #{x : U | n ∈ f x} = ∑ u, ∑ n, if n ∈ f u then 1 else 0
 · rw [Finset.sum_comm]; simp

and it was in the line labeled h2 that I failed, and subsequently tried to simplify down to a minimal example, which is the one above.

Given how often (in probability theory, for instance), cardinalities and indicator functions are tossed around, I felt that surely this must be straightforward....but apparently it's not. I tried nitpick to see whether I'd stupidly missed some hypothesis in the statement of the lemma, but nothing obvious came up.

I also tried changing (if (P u) then 1 else 0))" to `(if (P u) then (1::nat) else 0))" in case that nudge would help, but it had no visible effect.

Yong Kiam (Jul 06 2025 at 10:10):

lemma card_indicator:
  fixes U::"'a set"
  fixes P::"'a ⇒ bool"
  assumes "finite U"
  shows  "card { u ∈ U .   (P u)} =  (∑ u ∈ U  .  (if (P u) then 1 else 0))"
  by (metis (no_types, lifting) ext assms card_eq_sum
      sum.inter_filter)

John Hughes (Jul 06 2025 at 10:24):

I've just gone in and commented out the remainder of the file I was working on, and once I've done that, this tiny lemma (right at the top) can be handled by sledgehammer. I'm not sure what's going on there, but I'm certainly happy to be able to proceed -- thank you. It's a relief to know that I didn't miss something stupid in the lemma statement. :)

Yong Kiam (Jul 06 2025 at 11:38):

probably later in your file more lemmas got fed to sledgehammer so it timed out, you could have perhaps tried to increase the time limit on your sledgehammer call

Fabian Huch (Jul 07 2025 at 06:32):

Also sledgehammer not finding a proof does not mean it's not easily provable. If you re-write the card to a sum (subst card_eq_sum) then solve_direct tells you that there already is a rule for this.

John Hughes (Jul 08 2025 at 16:30):

Thanks, Fabian. There's a challenge for a beginner, namely, how to know that I can rewrite "card" to a sum. I suppose that I could start at the very bottom of the chain of theories included in Main and read them all and try to remember everything I see, but it's hard to believe that this is a viable approach (esp. for those of us whose memory is already over-full and fast declining). Is there some other recommended way to know such things?

Should I, for instance, say to myself "I seem to be having trouble with card, so I should look at its definition, and then do a find_theorems and look for anything with card in it."? Or is there some other way that you use when you start to use some part of Isabelle that you're not already familiar with?

Fabian Huch (Jul 08 2025 at 16:37):

If I state a lemma like that I'd think: "surely there's something about card begin equal to a sum" so I'd search for the pattern

find_theorems "card _ = sum _ _"

Fabian Huch (Jul 08 2025 at 16:38):

Sledgehammer _usually_ also works well in finding lemmas, but sometimes it doesn't.

John Hughes (Jul 08 2025 at 16:58):

proof (subst card_eq_sum)

I would normally try to write something like show ?thesis by sledgehammer, but in this case the subst has changed the goal so this warns me that what I'm hoping to show isn't (a refinement of) the current goal. So I end up copying the new goal and pasting it in, to get
show " (∑x∈{u ∈ U. P u}. 1) = (∑u∈U. if P u then 1 else 0) " by sledgehammer, and then I'm on my way. But I keep wondering if there's some other way to refer to the changed goal without the copy-paste step.

proof (subst card_eq_sum)

I might instead type solve_direct (something I didn't know I could do until 5 minutes ago). It tells me that

 the current goal can be solved directly with
  Groups_Big.comm_monoid_add_class.sum.inter_filter:

but I'm not sure what to do with that information. Is there a common set of steps one takes to use this information?

lemma h1:
  shows "P 1" sorry

lemma h2:
  shows "P 1"

where "auto solve_direct" says that the goal can be solved with h1. But I've never know exactly what sequence of steps I should follow to make use of this information.

As I seem to often say in my questions, "You have no idea how little I know/understand about Isabelle, so please explain it to me as if I'm in kindergarten."

Fabian Huch (Jul 08 2025 at 17:25):

John Hughes (Jul 08 2025 at 18:13):

Ah...thank you. Perhaps solve_direct was an early automation tool, perhaps even pre-Isar.

I've tried pretty hard to stick to what I think of as "core Isar" and avoid apply-scripts, just as I avoided "asm" when writing C-code in the 1970s. :) Perhaps I should actually get familiar with apply-scripts, but avoiding them has worked for me so far.

proof (subst card_eq_sum)
  show " (∑x∈{u ∈ U. P u}. 1) = (∑u∈U. if P u then 1 else 0) "
  proof (rule sum.inter_filter)    <--------------
    show "finite U" using assms by blast

Stream: Beginner Questions

Topic: Cardinality and indicator functions

John Hughes (Jul 06 2025 at 09:57):