repeat issues

Stream: lean4

[Kevin Buzzard]

theorem or_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := sorry

variable (P1 P2 Q1 Q2 R1 R2 : Prop)

/-
`repeat` docstring:
repeat tac applies tac to main goal. If the application succeeds, the tactic
is applied recursively to the generated subgoals until it eventually fails.
-/

example : P1 ∨ Q1 ∨ R1 ↔ P2 ∨ Q2 ∨ R2 := by
  repeat apply or_congr
  /-
  ⊢ P1 ↔ P2
  ⊢ Q1 ∨ R1 ↔ Q2 ∨ R2
  -/
  -- it didn't repeat
  repeat sorry

example : P1 ∨ Q1 ∨ R1 ↔ P2 ∨ Q2 ∨ R2 := by
  repeat apply squeamish_ossifrage -- not actually a theorem
  -- no error
  -- ⊢ P1 ∨ Q1 ∨ R1 ↔ P2 ∨ Q2 ∨ R2
  sorry

For the first one, am I misunderstanding what "generated subgoals" means? For the second, perhaps this is strictly speaking correct behaviour, although speaking from experience it can cause a lot of confusion.

[Alex J. Best]

Use repeat' there is a thread on this somewhere!

[Alex J. Best]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Semantics.20of.20repeat/near/307770628

[Kevin Buzzard]

Oh thanks! So the docstring is wrong? What should be fixed? The docstring or the tactic? Or do we just let people continue to discover this?

[Mario Carneiro]

yeah the doc is misleading at best. It's really just looping tac until it fails, which means that it actually only runs on the first generated subgoal if you use a branching tactic

[Scott Morrison]

doc-string PR at https://github.com/leanprover/lean4/pull/2184