Zulip Chat Archive

Stream: new members

Topic: Universal over concrete finite set


view this post on Zulip Logan Murphy (Jul 16 2020 at 13:52):

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

view this post on Zulip Scott Morrison (Jul 16 2020 at 14:02):

If it is a finset then you can use fincases.

view this post on Zulip Scott Morrison (Jul 16 2020 at 14:07):

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

view this post on Zulip Kevin Buzzard (Jul 16 2020 at 21:16):

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

view this post on Zulip Alex J. Best (Jul 16 2020 at 21:21):

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

Last updated: May 14 2021 at 23:14 UTC