basic set theory

Stream: new members

[Pedro Castilho]

Hi, am student from Brazil trying to learn a bit more about lean and am having same difficulties in using some theorems from Mathlib, in particular this one:
how would I use set.union_diff_left to solve something like this in tactic mode

example : (t ∪ s) \ s ⊆ t \ s

thx for the help

[Alex Peattie]

Hey Pedro, you might find #backticks and #mwe useful when you're asking questions :smile:. I think it's more natural to prove your example with set.union_diff_right:

import data.set.basic

universe u
variables {α : Type u}

example {s t : set α} : (t ∪ s) \ s ⊆ t \ s := begin
  apply eq.subset,
  exact set.union_diff_right,
end

But if you wanted to use set.union_diff_left, you could do something like:

import data.set.basic

universe u
variables {α : Type u}

example {s t : set α} : (t ∪ s) \ s ⊆ t \ s := begin
  apply eq.subset,
  rw set.union_comm,
  exact set.union_diff_left,
end

Also, if you use the hint tactic you can see that you can prove the statement with intro, finish too

[Pedro Castilho]

But using finish wouldn't be considered cheating in such a simple proof? hahaha
by the way thx for the help, Alex

[Kevin Buzzard]

The whole point of tactics like finish is to save humans from having to write mathematically trivial proofs

[Eric Wieser]

Although writing mathematically trivial proofs is probably good practice for getting to grips with how lean works

[Esteban Estupinan]

lean has helped me in writting better proofs. Someone could give me an idea how to continue this proof or how can I use h? Thank you for your answers

[Esteban Estupinan]

open set

variable {α : Type*}
variables (A B C : set α)

theorem t1 (h: A \ B ⊆ C): A \ C ⊆ B :=
begin
  assume x,
  intro h1,
  cases h1 with ha hc,

end ```

[Marcus Rossel]

I'm guessing you don't want lemmas from Mathlib for this. So if you want to prove this "yourself", then perhaps unfolding the definition of \ might help:

theorem t1 (h: A \ B ⊆ C): A \ C ⊆ B :=
begin
  assume x,
  intro h1,
  cases h1 with ha hc,
  simp only [(\), set.diff] at h,

end

You can unfold any notation using simp [(<notation>)]. So if you also want to unfold the ⊆ you could write:

simp only [(⊆), set.subset] at h,

[Esteban Estupinan]

yes exactly, not using mathlib lemmas, prove by myself

[Eric Wieser]

It's not cheating to use set.mem_diff in that proof - if you're using mathlib's definitions, then it's totally fair game to use mathlibs lemmas that tell you what they unfold to.

[Eric Wieser]

If you use dsimp [set.mem_diff] that ensures you're not using a lemma which is "cheating" (ie, one that actually contains a proof)

[Esteban Estupinan]

thank you, unfold is a practical tool in this case, first time I use it. I see some facts that can use to proof from the unfold but sincerely I do not know how start. how can I link the unfold facts with the cases from and elimination of the first hypothesis?

[Esteban Estupinan]

import tactic

open set

variable {α : Type*}
variables (A B C : set α)

theorem t1 (h: A \ B ⊆ C): A \ C ⊆ B :=
begin
  assume x,
  intro h1,
  cases h1 with ha hc,
  simp only [(\), set.diff] at h,
  simp only [(⊆), set.subset] at h,

end

[Kyle Miller]

You might want to allow yourself dsimp only [mem_sep_eq] at h now. mem_sep_eq is a lemma that is the definitionally true -- it's a tautology.

You can also have the same effect by using change, but that requires you to know the definitions:

change ∀ a, a ∈ A ∧ a ∉ B → a ∈ C at h

[Esteban Estupinan]

thank you Kyle for supply me tactics. Now really I have the idea to complete a proof of transitive law for inclusion for sets. By change tactic I m using only x variable. My idea is more less this. like I have x is in set R, i 'have' x in set S and like i 'have' x in set S, I conclude that x is in T set and finish the proof. I tried to use apply, have-from, intro, but all these put error in the code.

[Esteban Estupinan]

import tactic

open set

variable {α : Type*}
variables (R S T : set α)

theorem t1 (h1 : R ⊆ S) (h2 : S ⊆ T) : R ⊆ T :=
begin
  assume x,
  intro h,
  simp only [(⊆), set.subset] at h1,
  change ∀ x, x ∈ R → x ∈ S at h1,
  simp only [(⊆), set.subset] at h2,
  change ∀ x, x ∈ S → x ∈ T at h2,



end

[Kyle Miller]

Hint: use the apply tactic. apply h2 is a good next step.

[Kyle Miller]

That's a proof in the "reverse direction." If you want to go in the "forward direction," a good next step is specialize h1 x h.