Stream: Beginner Questions

Topic: Is there a shorter way for this?

waynee95 (Oct 19 2022 at 18:32):

Is there a shorter way to arrive at the induction here?

lemma blubb:
  assumes "∀i ≤ card S + 1. ∀i' ≤ card S + 1.
          i ≠ i' ⟶ (f::nat⇒'a) i ≠ f i'"
  shows "∀n ≤ card S + 1. n ≤ card (⋃i≤n. {f i})"
proof (rule allI, rule impI)
  fix n
  show "n ≤ card S + 1 ⟹ n ≤ card (⋃i≤n. {f i})"
  proof (induction n)
  ...

Something like proof (rule allI, rule impI, induction) or proof (rule allI, rule impI, induction n) does not work and I can see why.
Maybe it's not really important to save two lines here but I just wanted to check.

Mathias Fleury (Oct 19 2022 at 18:38):

Theoretically, induct_tac might work

Mathias Fleury (Oct 19 2022 at 18:38):

otherwise, rephrase your theorem by removing the ∀

waynee95 (Oct 19 2022 at 18:41):

induct_tac did something but not something right.

But rephrasing the theorem by removing the quantifier works...

lemma blubb:
  assumes "∀i ≤ card S + 1. ∀i' ≤ card S + 1.
          i ≠ i' ⟶ (f::nat⇒'a) i ≠ f i'"
  shows "n ≤ card S + 1 ⟹ n ≤ card (⋃i≤n. {f i})"
proof (induction n)

well that was easier than I expected whoops

Last updated: Dec 21 2024 at 16:20 UTC