Succinct way to discharge subgoals

Stream: new members

[Josh Cohen]

Suppose I have a tactic tac that generates 3 subgoals, and I know the tactics that solve the 2nd and/or 3rd ones, is there an easy way to solve these goals without a verbose cases or needing lots of indentation? In Rocq, I can say tac; [ | tac1 | tac2]; this applies tac1 to the second subgoal generated by tac and tac2 to the third one. For a 2-subgoal example, see the following

inductive foo where
  | f (s: String) (n: Nat)
deriving DecidableEq

def mkFooDefault (s: String) : foo := .f s 0

theorem bar: (if (.f "0" 0) = mkFooDefault "0" then b1 else b2) = b3 := by
  rw[if_pos]

I would like to be able to give the rfl that closes the generated subgoal from if_pos without needing cases, nesting, etc. Is there a way to do this in general (not just for this specific example)? Thanks

[Josh Cohen]

I would also like something more exact than just e.g. tac <;> try tac1 <;> try tac2, since these tactics might be slow to run over every subgoal.

[František Silváši 🦉]

tac_that_yields_3_subgoals <;> [tac1; tac2; tac3] is the 'tacticy' way to do it
so in your case, rw [if_pos] <;> [skip; rfl].

Of course, there's a preference for using arguments here, so for example rw [if_pos (show _ by rfl)].

[Josh Cohen]

Thanks, I was not aware of that syntax. To make sure I understand correctly, in <;> [tac1; tac2; tac3] tac1 is run on the first subgoal, tac2 on the second, and tac3 on the third? Or only if each tactic solves the corresponding goal?

[František Silváši 🦉]

tac<k> is applied to the kth subgoal, there is no obligation to close the goal.

I'll emphasize that this is not particularly common to see in Lean, you'll normally see people structure their proofs with using arguments, \centerdots, cases, refine ?p -> case ps, etc.

Relying on order of subgoals normally makes things less readable.

[Josh Cohen]

Thank you. Is there an idiomatic Lean way to close a single auxiliary subgoal generated by a rewrite, apply, etc? Repeated use of cases or \centerdots could end up with a proof with many layers of indentation and cases even though the "interesting part" might only be in one of those cases.

[František Silváši 🦉]

I agree you normally want 'linear' proofs that focus on the interesting parts of the argument.

The idiomatic way is to use arguments as alluded to above - rw [if_pos h] where h is a proof that your condition holds. Maybe you already have h, maybe you have h : condition := ..., maybe it's short and you rw [if_pos (show condition from ...)]; many ways to start skinning the :cat: . Maybe you rw [if_pos (by tac)] where tac is some automation that can do the trick, like grind.

[Ruben Van de Velde]

Also, you can write

tactic
· side goal
· side goal
rest of main argument

or like

tactic ?h1 ?h2
case h1 => side goal
case h2 => side goal
rest of main argument

[Philippe Duchon]

Is there a way to select a subgoal other than the first? (If there is one, it doesn't seem to be very idiomatic, as I don't remember reading about it in the various online Lean books I've read)

In Rocq, you can do something like 2 : <tac> (hope I'm right about the syntax) to apply a tactic to, say, the second subgoal; something that can be used to close a simple subgoal here and there instead of waiting for the end of what could be a long first goal - as an alternative to using some form of indentation.

[František Silváši 🦉]

You can rotate_right (and left) to move them around, swap them (that's really just rotate by one), or you can choose them with case <name>. There's also case' <name> => tac that lets you apply tac to the chosen goal without enforcing its closure. I am not sure there's a way to refer to them by their index in the order displayed in the infoview, but it's a trivial bit of metaprogramming. Admittedly I'd discourage this style.

[Wang Jingting]

Philippe Duchon said:

Is there a way to select a subgoal other than the first? (If there is one, it doesn't seem to be very idiomatic, as I don't remember reading about it in the various online Lean books I've read)

In Rocq, you can do something like 2 : <tac> (hope I'm right about the syntax) to apply a tactic to, say, the second subgoal; something that can be used to close a simple subgoal here and there instead of waiting for the end of what could be a long first goal - as an alternative to using some form of indentation.

I think you can do pick_goal 2 in lean which has a similar effect.

[Josh Cohen]

František Silváši 🦉 said:

tac_that_yields_3_subgoals <;> [tac1; tac2; tac3] is the 'tacticy' way to do it
so in your case, rw [if_pos] <;> [skip; rfl].

This syntax didn't work for me for some reason, I get error "unexpected token '['; expected tactic" after the <;>. And I am trying to use this in a tactic macro, so I cannot use explicitcases.

Alternatively, is there a better way to write a tactic macro of the form:

tac1
case case1 => tac2
case case2 => tac3