Stream: Beginner Questions

Topic: How to do induction on set?

Liangrun Da (Jun 08 2024 at 15:20):

Hi! Consider the following lemma:

1. P x holds for any element x in set S.
2. For any x and y, if P x and P y holds, P (x ∪ y) holds
3. P {} holds
4. Prove that P (\Union S) holds

\Union is Complete_Lattices.Union

lemma P_Union:
  assumes "∀x ∈ S. P x"
    and "P {}"
    and "∀x y. P x ∧ P y ⟶ P(x ∪ y)"
  shows "P (⋃ S)"
proof -
  have "∀a∈S. ∀b∈S. P (a ∪ b)"
    using assms(1) assms(3) by blast
  have "∀a∈S. ∀b∈S. (a ∪ b) ∪ (⋃(S - {a, b})) = ⋃ S"
    by blast
  show ?thesis oops

I tried to prove it by decomposing (\Union S) into (a ∪ b) and (\Union (S -{a, b})) and prove P for them respectively. It seems to work but I need to an induction rule for set to finish it.

I know there is an induct rule named "length_induct" which works for list:

(⋀xs. ∀ys. length ys < length xs ⟶ ?P ys ⟹ ?P xs) ⟹ ?P ?XS

However I couldn't find a similar induction rule for set. I'm wondering if there is indeed such an induction rule for set. If not, how should I prove this lemma?

Yong Kiam (Jun 08 2024 at 16:52):

the lemma is not true, consider P to be the property of a set being closed

Yong Kiam (Jun 08 2024 at 16:53):

(in particular, if you want to induct on S, you may want to assume it's finite)

Liangrun Da (Jun 08 2024 at 17:10):

Yong Kiam said:

the lemma is not true, consider P to be the property of a set being closed

Thanks for your answer! However I'm still a bit confused by what you mean when you say "consider P to be the property of a set being closed." If "a closed set" means the set is closed under some operation, could you give me a concrete counterexample of this? I couldn't figure out a operation that satisfies "closed X op \and closed Y op --> closed (X ∪ Y)" but doesn't satisfies closed (⋃ S) op

Yong Kiam (Jun 08 2024 at 17:13):

I meant topologically closed, for example, let S be the set of singleton points in (-1,1)

Liangrun Da (Jun 08 2024 at 17:38):

Yong Kiam said:

I meant topologically closed, for example, let S be the set of singleton points in (-1,1)

I got it! Do yo think it was because S is an infinite set in your example (the set of singleton points in (-1,1)) ? If that was the reason, how can I prove the following modified lemma using induction on S? (I never did induction on set before and didn't see such an example either)

lemma P_Union:
  assumes "∀x ∈ S. P x"
    and "P {}"
    and "∀x y. P x ∧ P y ⟶ P(x ∪ y)"
    and "finite S"
  shows "P (⋃ S)"

Mathias Fleury (Jun 08 2024 at 17:58):

Just make sure that the finite assumptions comes first:

lemma P_Union:
  assumes "∀x ∈ S. P x"
    and "P {}"
    and "∀x y. P x ∧ P y ⟶ P(x ∪ y)"
    and "finite S"
  shows "P (⋃ S)"
  using assms(4,1-3)
  by (induction S)
   ...

Mathias Fleury (Jun 08 2024 at 17:59):

(yes what the "..." is very simple to find and yes the proof works)

Liangrun Da (Jun 08 2024 at 18:07):

Mathias Fleury said:

Just make sure that the finite assumptions comes first:

lemma P_Union:
  assumes "∀x ∈ S. P x"
    and "P {}"
    and "∀x y. P x ∧ P y ⟶ P(x ∪ y)"
    and "finite S"
  shows "P (⋃ S)"
  using assms(4,1-3)
  by (induction S)
   ...

Yes it worked! Thank you both.

Last updated: Dec 21 2024 at 16:20 UTC