Zulip Chat Archive

Stream: new members

Topic: equality of sets


view this post on Zulip Logan Murphy (Sep 15 2020 at 19:58):

I feel like it should be trivial to prove (something like) the following equality, but I can't seem to do it with basic tactics and I can't seem to find anything in the library that helps. Any suggestions?

def S₁ : set  := {1}
def S₂ : set  := {3}

def fin_S : fin 2  set  := ![S₁, S₂]

def S : set  := S₁  S₂

def sets_complete : ( i : fin 2, fin_S i) = S :=
by sorry

view this post on Zulip Kevin Buzzard (Sep 15 2020 at 19:59):

Can you post an #mwe please? Your code doesn't work for me.

view this post on Zulip Chris B (Sep 15 2020 at 20:14):

edit: was not expecting that to be matrix.vec_cons

@Logan Murphy sets are defined as their membership predicate, so basic equality of sets stuff comes from functional and propositional extensionality (see set.ext). You can find some of the definitions and lemmas in the documentation for data.set :
https://leanprover-community.github.io/mathlib_docs/data/set/basic.html

view this post on Zulip Logan Murphy (Sep 15 2020 at 20:18):

Thank you Chris,

Sorry Kevin, forgot my transitive imports,

import data.matrix.notation
def S₁ : set  := {1}
def S₂ : set  := {3}

def fin_S : fin 2  set  := ![S₁, S₂]

def S : set  := S₁  S₂

def sets_complete : ( i : fin 2, fin_S i) = S :=
by sorry

view this post on Zulip Adam Topaz (Sep 15 2020 at 20:54):

This boils down to proving that every term of fin 2 is either 0 or 1 (also for arbitrary S_1, S_2). Is there a one-line proof of this?

import data.matrix.notation
def S₁ : set  := {1}
def S₂ : set  := {3}

def fin_S : fin 2  set  := ![S₁, S₂]

def S : set  := S₁  S₂

lemma fin_2_eq (i : fin 2) : i = 0  i = 1 := sorry

def sets_complete : ( i : fin 2, fin_S i) = S :=
begin
  ext,
  split,
  { rintro ⟨_,i,rfl,h,
    rcases fin_2_eq i with rfl|rfl,
    left,
    assumption,
    right,
    assumption },
  { rintro (h|h),
    use S₁,
    use 0,
    refl,
    assumption,
    use S₂,
    use 1,
    refl,
    assumption }
end

view this post on Zulip Adam Topaz (Sep 15 2020 at 20:57):

Maybe there is a much shorter proof for sets_complete in your specific case where S_1 and S_2 are explicit singletons. I dont know.

view this post on Zulip Yakov Pechersky (Sep 15 2020 at 21:09):

lemma fin_2_eq (i : fin 2) : i = 0  i = 1 := by { fin_cases i; simp }

view this post on Zulip Adam Topaz (Sep 15 2020 at 21:09):

Ah, fin_cases was the tactic I was missing :)

view this post on Zulip Kevin Buzzard (Sep 15 2020 at 21:19):

We were all missing it until Scott wrote it a few months ago

view this post on Zulip Kyle Miller (Sep 15 2020 at 21:52):

Yakov Pechersky said:

lemma fin_2_eq (i : fin 2) : i = 0  i = 1 := by { fin_cases i; simp }

I thought this was something the equation compiler could solve, but I guess not. There needed to be a third case with a proof of impossibility:

lemma fin_2_eq : Π (i : fin 2), i = 0  i = 1
| 0, _⟩ := or.inl rfl
| 1, _⟩ := or.inr rfl
| n+2, h := false.elim (by { cases h, cases h_a, cases h_a_a })

view this post on Zulip Kenny Lau (Sep 15 2020 at 21:55):

if you want good inductions, use fin2

view this post on Zulip Kevin Buzzard (Sep 15 2020 at 22:01):

Does omega do the n+2 case?

view this post on Zulip Kyle Miller (Sep 15 2020 at 22:44):

Looks like omega can't do it

view this post on Zulip Alex J. Best (Sep 15 2020 at 23:20):

by simp [fin.ext_iff]; omega works, omega just needs a little help from simp.

view this post on Zulip Alex J. Best (Sep 15 2020 at 23:22):

Actually thats a bit of a red herring I guess.

by exfalso; revert h; omega

also works.


Last updated: May 14 2021 at 07:19 UTC