working with sets defined in bracket notation

Stream: new members

[Andrew Lubrino]

I'm working on the below problem in set theory. I'm using this problem as a springboard to learn about working with sets defined inside brackets. The goal on the last line is an existential with an argument H. I think if I can build this argument from the statements I have an reintroduce the existential, I should be able to solve the goal, but, in H, Lean changed my original statement into a different statement that I'm not sure how to deal with. I've looked around in mathlib for statements that might help, but I also wanted to ask here if there is anything in mathlib that might help me here. My code is below:

import data.set
open set

variable {U : Type}
variables A : set U
variable F : set (set U)

theorem diff_notation : A ∩ (⋃₀F) = ⋃₀{(A ∩ p) | (p ∈ F)} :=
begin
  apply ext,
  intro c,
  apply iff.intro,
  intro h1,
  rw mem_sUnion,
  have h2 : c ∈ ⋃₀F, from and.right h1,
  rw mem_sUnion at h2,
  rcases h2 with ⟨p, h3, h4⟩,
  have h5 : c ∈ A ∩ p, from and.intro h1.left h4,
  sorry
end
``

[Kyle Miller]

You can use the tactic#simp tactic here -- if you want to know what lemmas it ends up using, you can do simp? or tactic#squeeze_simp.

[Andrew Lubrino]

wow, that's amazing. Thanks so much!!!

[Andrew Lubrino]

are there any good rules about when simp can or can't be used? I've tried using it before and wasn't successful but it works here.

[Patrick Massot]

https://leanprover-community.github.io/extras/simp.html

[Andrew Lubrino]

also, I have one other general question about tactics that rewrite the goal to an equivalent form. When I was in high school, I had to do some proofs in trigonometry. My teacher would always tell us that we should work from one side of the equation to the other, i.e. don't work from both sides of the equation. rewriting the goal feels a lot like working from both sides of the equation. why is this allowed?

[Andrew Lubrino]

thanks for the link, that's exactly what I'm looking for

[Andrew Lubrino]

also, I have one other general question about tactics that rewrite the goal to an equivalent form. When I was in high school, I had to do some proofs in trigonometry. My teacher would always tell us that we should work from one side of the equation to the other, i.e. don't work from both sides of the equation. rewriting the goal feels a lot like working from both sides of the equation. why is this allowed?

[Andrew Lubrino]

also, I have one other general question about tactics that rewrite the goal to an equivalent form. When I was in high school, I had to do some proofs in trigonometry. My teacher would always tell us that we should work from one side of the equation to the other, i.e. don't work from both sides of the equation. rewriting the goal feels a lot like working from both sides of the equation. why is this allowed?

[Andrew Lubrino]

thanks for the link, that's exactly what I'm looking for

[Kyle Miller]

When writing proofs, there's broadly two kinds of reasoning: forward and backward reasoning. In forward reasoning, you create new facts from already known facts (i.e., additional hypotheses), and in backward reasoning you modify the goal to something stronger (it's usually indicated by "it suffices to show that").

It's easier to get forward reasoning right, and students tend to get the backward reasoning backwards, which is likely why you're told that you "shouldn't prove things starting from the conclusion."

[Kyle Miller]

With Lean, you're just not allowed to do it wrong :-)

[Andrew Lubrino]

that makes sense. if I think about it, there should be no reason we can't work from both sides of the equation, so thanks for explaining that.

[Kevin Buzzard]

When writing proofs, there's broadly two kinds of reasoning: forward and backward reasoning.

I have heard this so often but it's not my mental model of a proof at all. When writing proofs you can do anything mathematically valid, and in particular the concept of manipulating the hypotheses until they become closer to the goal and manipulating the goal until it becomes closer to the hypotheses are concepts which I find indistinguishable -- they're both "applying the rules of mathematics in order to prove a theorem". I am still totally bewildered about why people insist on making the distinction.

[Eric Rodriguez]

I sometimes feel like this comes from school, where I remember being told that I'd be marked down if for my proof of a = b, I had to write down the steps to turn a to b or the other way round, I couldn't "meet in the middle". But, to be fair, I sometimes wish there was less applys in Lean, especially when I was still learning. It's more verbose to write the have := ..., replace := ... style, but in some ways that's what we had to do.

[Kyle Miller]

Kevin Buzzard said:

in particular the concept of manipulating the hypotheses until they become closer to the goal and manipulating the goal until it becomes closer to the hypotheses are concepts which I find indistinguishable

By mentioning manipulating hypothesis and manipulating goals... are you distinguishing these, or are those formal sequences of letters that you've learned mean something to the forward-backward thinkers?

[Kevin Buzzard]

I am able to distinguish a hypothesis from a goal, but I am unable to attach any mathematical use to concepts such as "this tactic changes only the hypotheses", "this tactic changes only the goal" and "this tactic changes both goal and hypotheses" (e.g. subst, simp * at * etc). Quite how the forwards/backwards people classify the latter tactics I don't know (and I don't care because the distinction seems to be of no help to me personally).

[Andrew Lubrino]

I'm still a little confused about what's actually happening in the theorem that simp applies here. simp applies exists_exists_and_eq_and, but the statement in the theorem looks totally different from my goal, but it still works. exists_exists_and_eq_and is (∃ (b : β), (∃ (a : α), p a ∧ f a = b) ∧ q b) ↔ ∃ (a : α), p a ∧ q (f a). My goal is ∃ (t : set U) (H : t ∈ {_x : set U | ∃ (p : set U) (H : p ∈ F), A ∩ p = _x}), c ∈ t. I'm guessing that a and b are mapped to t and p in my goal, but I think I'm confused about how the predicate inside the bracket is treated by Lean.

[Andrew Lubrino]

Maybe this is one of those things I'll have to accept until it suddenly makes sense to me three months from now hahaha

[Andrew Lubrino]

Is there any way to simplify just the stuff in brackets so that I can see what's happening there?

[Kevin Buzzard]

@Andrew Lubrino If things look different then they're not syntactically equal, however they can still be definitionally equal; maybe you want to read this to see some explanation of these ideas.

[Arthur Paulino]

You can constrain simp by writing simp only [<lemma_name>]
For example, simp only [exists_prop], turns

∃ (t : set U) (H : t ∈ {_x : set U | ∃ (p : set U) (H : p ∈ F), A ∩ p = _x}), c ∈ t

Into

∃ (t : set U), t ∈ {_x : set U | ∃ (p : set U), p ∈ F ∧ A ∩ p = _x} ∧ c ∈ t

So you can use the lemmas one by one to understand what's happening. squeeze_simp used the following lemmas:

exists_prop, mem_set_of_eq, exists_exists_and_eq_and, mem_inter_eq

[Andrew Lubrino]

Awesome, thank you both. This looks like there's a lot more for me to dig into. I really should have used squeeze_simp from the beginning. Thanks Kevin, I took a look through that page and there's actually a lot that I think is stuff I should know about. I'm going to read through that tonight.