How to do this with tactic combinators?

Stream: new members

[Yan Yablonovskiy 🇺🇦]

I have been trying to make this proof for indiscrete topology work with combinators, but they never seem to access the second branch and i don't know how to redirect them. Things like assumption and done didnt work.

import Mathlib.Tactic

open TopologicalSpace

--tries to prove X is empty (to say Univ = empty set for Or.inl instead of going to Or.inr)
example (X : Type) : TopologicalSpace X where
  IsOpen (s : Set X) := s = ∅ ∨ s = Set.univ
  isOpen_univ := Or.inr rfl
  isOpen_inter := fun s t hs ht ↦ by
    apply hs.elim <;> apply ht.elim
    repeat (intro h1 h2; (first | apply Or.inl ; simp [h1,h2] | apply Or.inr ; simp [h1,h2]) )
  isOpen_sUnion := sorry

-- the non combinator version
example (X : Type) : TopologicalSpace X where
  IsOpen (s : Set X) := s = ∅ ∨ s = Set.univ
  isOpen_univ := Or.inr rfl
  isOpen_inter := fun s t hs ht ↦ by
    apply hs.elim <;> apply ht.elim
    · intro h1 h2
      apply Or.inl
      simp [h1,h2]
    · intro h1 h2
      apply Or.inl
      simp [h1,h2]
    · intro h1 h2
      apply Or.inl
      simp [h1,h2]
    · intro h1 h2
      apply Or.inr
      simp [h1,h2]
  isOpen_sUnion := sorry

[Ruben Van de Velde]

Do you want all_goals rather than repeat?

[Ruben Van de Velde]

Or is the issue with first? I don't know how that works, but maybe with a cdot or curly braces you can explain that the alternative needs to solve the goal

[Vlad Tsyrklevich]

yeah weirdly enough I got this to work though I'm not sure why it solves the fourth condition:

    apply hs.elim <;> apply ht.elim
    all_goals
    · intro h1 h2;
      try simp [Or.inl, h1, h2]

[Vlad Tsyrklevich]

ah because apply Or.inr is not required, simp [h1, h2] solves it alone

[Vlad Tsyrklevich]

I think the error is not that the second branch is not being accessed, but that the apply Or.inl from the first branch is being used and not rolled back. Indeed apply hs.elim <;> apply ht.elim <;> simp_all actually just works, but maybe you were trying to experiment with combinators and that's not the point?

[Yan Yablonovskiy 🇺🇦]

Yea i figured this would be a good use case for combinators , and TPIL chapter using combinators is full of examples using Or.inl/inr . So not sure how to get this one to work, in the refs it said
first | tac | ... runs each tac until one succeeds, or else fails.
So to me it seems like it should try and reach IsEmpty X and then try the next block and succeed :face_with_spiral_eyes:

I think the issue might be with repeat, https://lean-lang.org/doc/reference/latest/Tactic-Proofs/The-Tactic-Language/#repeat looks like it is based on making some progress on some goal.

I learned about iterate which i didn't know before:

    apply hs.elim <;> apply ht.elim
    iterate 3 (intro h1 h2; apply Or.inl ; simp [h1,h2])
    · intro h1 h2
      apply Or.inr
      simp [h1,h2]

[Vlad Tsyrklevich]

The examples in TPIL don't require "rolling back the state" like you're trying to do. Once you've run apply + simp in the first branch it carries over the second branch. Incidentally, it appears that solve doesn't have this behavior and you could do

    apply hs.elim <;> apply ht.elim <;> intro h1 h2
    all_goals solve | (left; simp [h1, h2]) | (right; simp [h1, h2])

though this is not something I knew before.

[Kenny Lau]

have you tried grind or aesop? it sounds a bit like you're trying to reinvent the wheel here