Set Theory Game Question

Stream: new members

[Gridiron Player]

To solve Level 6 in the family intersection game, I use the following sequence of commands:

intro x
intro h2
rewrite [mem_sInter] at h2
have h3 : ⋂₀ F ∈ F → A ∪ (⋂₀F : Set U) ∈ G
exact h1 (⋂₀F : Set U)
have h4 : A ∪ (⋂₀F : Set U) ∈ G := by apply h3
have h5 : A ∪ (⋂₀F : Set U) ∈ G → x ∈ A ∪ (⋂₀F : Set U)
exact h2 (A ∪ ⋂₀ F : Set U)
have h6 : x ∈ A ∪ ⋂₀ F := by exact h5 h4
exact h6

For some reason, I am not able to apply exact h6 in the end. Might the reason be that I used casting such as (⋂₀F : Set U) ?

[Mario Carneiro]

Seems like a lean game maker bug, cc: @Jon Eugster . I was able to input the commands until the last line, which also appears to have been accepted and also produces 0 goals but does not trigger a "goals accomplished"

[Dan Velleman]

I don't understand what's happening in the step have h4 : A ∪ (⋂₀F : Set U) ∈ G := by apply h3. Applying h3 should leave you with a goal of ⋂₀ F ∈ F to complete the justification of h4. But the game just adds h4 to the list of assumptions and returns to the original goal, even though h4 has not been justified. Is there a problem with using have ... := by ... in games?

[Dan Velleman]

By the way, @Gridiron Player, this proof strategy doesn't look promising to me. I don't see any reason to believe that ⋂₀ F ∈ F is true, so I don't think h3 is going to be useful.

After intro x and intro h2, the game suggests writing out the meaning of the goal. If you do that, it gives a further hint giving a different approach to the proof.

[Gridiron Player]

@Dan Velleman For some reason, I assumed ⋂₀ F ∈ F to always be true. A simple counterexample would be F = {{1}, {2}} and ⋂₀ F = {}. {} is not an element of F.
Weird enough that the game let me do that though.

[Dan Velleman]

Yes, this looks like a bug in the game software.

[Gridiron Player]

Yes, and thinking about this deeper, the reason I thought ⋂₀ F ∈ F is always true is because I mixed it up with `⋂₀ F \subset F' Its always the basics :)

[Dan Velleman]

Perhaps what you're thinking of is the first level in Family Intersection World: If A ∈ F then ⋂₀ F ⊆ A.

[Jon Eugster]

Ah yes this makes sense, the line have h4 : A ∪ (⋂₀F : Set U) ∈ G := by apply h3 contains an "unsolved goal error" as you can see in the screenshot below (or in "editor mode"), but we've been filtering out the "unsolved goal" errors (in "typewriter mode", anyways) so that the user doesn't see it constantly while working on a proof. This will need some tweaking of this filtering logic, so you do get an error when entering the command you entered.

Screenshot_20240818_191545.png

If you replace have h4 : A ∪ (⋂₀F : Set U) ∈ G := by apply h3 by

have h4 : A ∪ (⋂₀F : Set U) ∈ G := by
  apply h3
  sorry -- goal: ⋂₀ F ∈ F

you can see better that the proof of h4 isn't done yet.

(also note that this is completely fine Lean syntax because := by <tactic> or := by <tacticSeq> are both valid, but the game generally mainly features "stream-of-conciousness" (aka unstructured) proofs, so := by isn't supported that well anyways)

[Dan Velleman]

I wonder if have h : P := by ... just shouldn't be allowed in the game. After all, if you want to give a tactic proof of P you can just do have h : P and then P becomes your immediate goal. Maybe you could allow have h : P := by <tactic> if the single tactic solves the goal P, but I'm not sure it's really useful, since the user can just as easily do have h : P on one line and then <tactic> on the next line. And have h : P := by <tacticSeq> really doesn't fit with the way the games work.

[Jon Eugster]

Indeed, if it would throw the error (which is filtered out by accident), the user would be asked to fix this line until it's error-free, so it's defacto disallowed. Probably it would be worth to even disallow by all together, you're right about that.