Zulip Chat Archive

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

Kevin Buzzard (Sep 15 2020 at 19:59):

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

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

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

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

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.

Yakov Pechersky (Sep 15 2020 at 21:09):

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

Adam Topaz (Sep 15 2020 at 21:09):

Ah, fin_cases was the tactic I was missing :)

Kevin Buzzard (Sep 15 2020 at 21:19):

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

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 })