Universal over concrete finite set

Stream: new members

[Logan Murphy]

Might be silly, but if one is trying to prove a predicate holds universally over a concrete, finite set, is there a way to enumerate the cases? E.g.

import data.nat.parity data.set.basic
open set nat

def s : set ℕ := {2, 4, 6, 8}

lemma silly : ∀ x ∈ s, even x :=
begin
    intros x h,
    -- case 1 : x = 2
    -- case 2 : x = 4
    -- etc.
end

[Scott Morrison]

If it is a finset then you can use fincases.

[Scott Morrison]

But there needs to be some evidence that your set is finite before this will be possible.

[Kevin Buzzard]

import data.nat.parity data.set.basic
open set nat

def s : set ℕ := {2, 4, 6, 8}

lemma silly : ∀ x ∈ s, even x :=
begin
    rintros x h,
    rcases h with rfl,
      use 1, norm_num,
    rcases h with rfl,
      use 2, norm_num,
    rcases h with rfl,
      use 3, norm_num,
    rw mem_singleton_iff at h, rw h,
      use 4, norm_num
end

[Alex J. Best]

You could also use repeat like this:

def s : set ℕ := {2, 4, 6, 8}


lemma silly : ∀ x ∈ s, even x :=
begin
    repeat {apply forall_insert_of_forall, swap, norm_num, },
    simp,
end