World: Family Combination World

Stream: new members

[Yagub Aliyev]

I successfully completed these two levels:

https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamCombo/level/1
https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamCombo/level/2

I have a recommendation if I may. I think it is much easier to work if you have not_imp, not_forall, not_exists under your hands. I can not imagine doing these two levels without them. especially after reading your hint "If you get stuck, consider using proof by contradiction."

[Jon Eugster]

@Dan Velleman

[Yagub Aliyev]

Also I am at the third level of this world:
https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamCombo/level/3
Objects:
U: Type
FGH: Set (Set U)
x: U
w: Set U
Assumptions:
h1: ∀ A ∈ F, ∃ B ∈ G, A ∩ B ∈ H
h: x ∈ ⋃₀ F ∧ x ∈ ⋂₀ G
hG: ∀ S ∈ G, x ∈ S
hw: w ∈ F ∧ x ∈ w
hwF: w ∈ F
hwx: x ∈ w

I want to use

apply h1 w

but it doesn't work. Somehow it worked earlier for universal quantifiers. Maybe the problem is that h1 is now consisted of nested quantifiers?

[Dan Velleman]

I think what you mean is that you want to apply h1 to w. That's a good next step, but the apply tactic isn't the right tactic to use for that. You can just say have h2 := h1 w.

The apply tactic is for working backwards from the goal.

[Dan Velleman]

Thanks for the recommendation. I'm going to look into introducing the push_neg tactic earlier--it automatically applies not_imp, not_forall, etc. That is a reasonable way to approach these levels, although I think proof by contradiction also works well if you remember that if you have an assumption h of the form ¬P and your goal is False, then apply h will set P as your goal.

[Notification Bot]

Yagub Aliyev has marked this topic as resolved.

[Yagub Aliyev]

https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamCombo/level/5

What is a complement of a family of sets (G^c)?

[Luigi Massacci]

Its complement as a subset of the powerset. (So all the subsets of U that do not belong to G)

[Yagub Aliyev]

Luigi Massacci said:

Its complement as a subset of the powerset. (So all the subsets of U that do not belong to G)

How do you use this concept in Lean? I mean there is no fam_comp_def it seems.

[Dan Velleman]

Families of sets are sets. The set operations union, intersection, and complement apply to them, just as they apply to all sets. So you can use the theorems inter_def, union_def, and comp_def with families of sets.

[Dan Velleman]

Perhaps when I introduce families of sets I should make this point in the text.

[Yagub Aliyev]

https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamCombo/level/5

import Mathlib.Tactic.Have
import Mathlib.Tactic.ByContra
import Mathlib.Tactic.Cases
import Mathlib.Tactic.ApplyAt

example (F G : Set (Set U)) (h1 : ⋃₀ (F ∩ Gᶜ) ⊆ (⋃₀ F) ∩ (⋃₀ G)ᶜ) : (⋃₀ F) ∩ (⋃₀ G) ⊆ ⋃₀ (F ∩ G) := by

apply comp_sub_of_sub at h1
rw[comp_inter] at h1
rw[comp_comp] at h1

This is maximum I could get in this. What do you recommend?

[Dan Velleman]

In an earlier discussion, I suggested putting off thinking as long as possible by beginning with steps that you can do without thinking. Going back to that idea, I would say that in this problem you are thinking too soon.
Since the goal is a subset statement, I would start with intro x h2, which will introduce both an arbitrary x : U and the assumption h2 : x ∈ ⋃₀ F ∩ ⋃₀ G, and the goal will become x ∈ ⋃₀ (F ∩ G). There are a few more steps you can do without thinking, but already this intro step will get you thinking in the right direction: if you know that x is an element of both ⋃₀ F and ⋃₀ G, why should it be an element of ⋃₀ (F ∩ G)?
This one is a bit tricky. Perhaps once you see why it is difficult to get from h2 to the goal, you'll be ready to think about how h1 could be useful.

[Yagub Aliyev]

@Dan Velleman
Thank you I completed all except the last level about singleton.
https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamCombo/level/7
It seems an impossible task. Any recommendation? I want to consider F={{x},{y}} but Lean does not recognize x and y which means I need to introduce them somehow. How do you do this? And how do I make sure x and y are different? How do I know if x and y even exist?

[Dan Velleman]

This is the hardest proof. Lean is right to complain that it doesn't know what x and y are. I don't know what they are either, and I suspect that you don't know either.

Your idea seems to be that you want the elements of F to be singleton sets. That's a good start. But which singleton sets? You need to figure out which singleton sets you want to put into F, and then you have to specify that in your definition of F.

Note that the hint suggests writing F in the form {S | ...}. I guess you want the ... to say something about S being a singleton set, but you'll have to be more explicit about which singleton sets should be included.

You may find it helpful to work this proof out on paper before doing it in Lean.

By the way, I updated the game, adding the push_neg tactic (it is introduced now in Complement World, Level 4) and also adding more explanation of families of sets in the introduction of Family Intersection World.

[Dan Velleman]

I'm also thinking about adding one more level to Family Combination World.

Thanks for your helpful feedback.

[Kyle Yank]

Good Job! It would be great to use "push_neg",actually I've already spent 4 days on Set Theory game,the only one I still haven't proved yet ,it is the last one.It's hard to put my thought into lean.I can do it quickly on my paper by my pen.But I'm still looking the answer, I almost do it in the last step,but still found a little problem. :smiling_face_with_tear:

[Kyle Yank]

Bro,if you have already finished this one, please send it here.I want to see how to do it.

[Kevin Buzzard]

The official answers to all the levels are in the source code which is on GitHub

[Dan Velleman]

I've added a new level to Family Combination World. The new level is level 3, and the old 3-7 are now 4-8.

[Kyle Yank]

Thank you.I'll try it now

[Kyle Yank]

Sir. I can not find it. Please give more detail.

[Notification Bot]

Kyle Yank has marked this topic as unresolved.

[Kyle Yank]

I can only find the answer to the NNG4. Where can I find the official answer to the set theory game?

[Notification Bot]

Kyle Yank has marked this topic as resolved.

[Notification Bot]

Kyle Yank has marked this topic as unresolved.

[Kyle Yank]

I just did the new one. Are there any tips for the singleton set?

[Dan Velleman]

@Kyle Yank The source files for the set theory game can be found here: https://github.com/djvelleman/STG4

I assume you've read the hints for the singleton set proof--both the one that appears right away and the one you get when you click on "Show more help!"

You say you have a proof for this one on paper? Is there some difficulty with putting your paper proof into Lean?

[Kyle Yank]

Actually, I have already finished this problem.
But I use a similar proof which is just like the official answer.

[Kyle Yank]

My paper proof is proven by making contradiction. I still don't know how to describe it in that game.

[Kyle Yank]

I assumed A is not empty and A has two elements in my paper. Then by finding the counterexamples, it's easy to find A is a singleton set.

[Kyle Yank]

Like this {{1},{2}} is not equal to {1,2}

[Kyle Yank]

But I don't know how to write this in this game, so I chose to construct a set like what the official set did.

[Kyle Yank]

the only difference between the official answer and mine is that I chose to prove it by A ⊆ B ∧ B ⊆ A.

[Dan Velleman]

Yes, there is a longer proof along the following lines:

1. Show that A has at least one element.
2. Show that A can't have more than one element.

Both parts would be proven by contradiction, and for each part you would need to choose a family F to plug into h1 to get the contradiction.

That proof can be written in Lean, but it would be much longer, and to write it you might want to use some set theory notation that is not introduced in the set theory game (such as notation for the empty set or notation for the difference of two sets).

[Kyle Yank]

That's what I did in my paper.

[Kyle Yank]

I guess I will read the introduction book firstly , I will try this later.

[Dan Velleman]

I think that proof is fine. But there may be several points where you said on paper that something was "clearly" true. One of the things that makes Lean difficult is that it doesn't understand "clearly". Even if something really is pretty clear, Lean insists that you justify it. Often that is not hard, but it's tedious.

[Kyle Yank]

That's a little monotonous, but that's what we want to improve.

[Kyle Yank]

Dan Velleman said:

I think that proof is fine. But there may be several points where you said on paper that something was "clearly" true. One of the things that makes Lean difficult is that it doesn't understand "clearly". Even if something really is pretty clear, Lean insists that you justify it. Often that is not hard, but it's tedious.

Thanks for your suggestions. :smiley:

[Yagub Aliyev]

Dan Velleman said:

This is the hardest proof. Lean is right to complain that it doesn't know what x and y are. I don't know what they are either, and I suspect that you don't know either.

Your idea seems to be that you want the elements of F to be singleton sets. That's a good start. But which singleton sets? You need to figure out which singleton sets you want to put into F, and then you have to specify that in your definition of F.

Note that the hint suggests writing F in the form {S | ...}. I guess you want the ... to say something about S being a singleton set, but you'll have to be more explicit about which singleton sets should be included.

You may find it helpful to work this proof out on paper before doing it in Lean.

By the way, I updated the game, adding the push_neg tactic (it is introduced now in Complement World, Level 4) and also adding more explanation of families of sets in the introduction of Family Intersection World.

Is it {S | ∃x, A={x}} that needs to be put there?

[Dan Velleman]

Did you mean {S | ∃x, S={x}}? The part after the | should mention S.

That is close, but not quite good enough. Of course, you can try to do the proof with that choice, and see where you get stuck.

The hint says this: "You need to apply h1 to a family of sets with two properties: the union of the family must be A, and knowing that A belongs to the family must help you prove that A is a singleton." Your proposal (as I have modified it above) has one of the required properties, but not the other.

[Yagub Aliyev]

Dan Velleman said:

I've added a new level to Family Combination World. The new level is level 3, and the old 3-7 are now 4-8.

Adding a new level in the middle or the beginning of a World seems to shift all the progress of the users and their old solutions end up in a wrong level. Adding a new bonus World or adding the new levels to the end of the World can be a short solution to this.

[Kevin Buzzard]

You're right in theory, but in practice having a level in the wrong place for all time is worse than disrupting saves for people who are currently playing (the people who finished and are never coming back don't notice, and the people who are yet to come will play the level in the right place)

[Kevin Buzzard]

I write this as someone who has on several occasions broken user saves in NNG just because it made the game better organised overall

[Jon Eugster]

Btw, it's fairly straight forward to hack and modify your own progress if some development broke it:

• In the main menu click "Dowload"
• Modify the JSON file. (There is a field "data" which contains fields of the form "[World Name]" which again contains the level numbers. Modify these numbers to the new, correct level numbers.)
• In the main Menu click on "Upload" to upload the modified user progress.

Unfortunately, I think it would be way to much overhead (or infeasible?) to have the user progress stored in a completely backwards compatible way.

[Dan Velleman]

@Yagub Aliyev Sorry for messing up your solutions to the set theory game. But, as Kevin suggested, I thought it was best to improve the game for future users, even if that was an inconvenience for people currently playing. I don't have any plans to add any other new levels. However, based on comments in a different thread, I am considering changing the names of some of the theorems in the set theory game to match the naming conventions in mathlib better.

[Yagub Aliyev]

@Dan Velleman No problem, I completed the game. I wonder where these problems are taken from? Very unusual problems for a usual set theory course. Thank you @Jon Eugster I just copied my answers from the old level to the new level.

[Dan Velleman]

I think I made up most of them. Many of them are problems I used in Proof Designer.