feat: add a shorthand for while-loop invariants

[volodeyka]

This PR changes the name WhileInvariant from Std/Internal/SpecLemmas to RepeatInvariant, since in most of the cases it will be called when verifying forIn -repeat loops. Also, we add a new abbreviation to construct RepeatInvarinats. This abbreviation specifies a condition inv which should hold at the end of each loop itreation (even the breaking one), and a condition onDone which should hold in the end of the loop in addition to inv.
In the case of a normal while loop the latter one could always be taken as negation of the loop condition.

[Rob23oba]

Small style fixes

[Rob23oba]

Suggested change

	A way to construct `forIn`/`whileM` invarinat by specifying a condition `inv` which should hold
	at the end of each loop itreation (even the breaking one), and a condition `onDone` which should
	hold in the end of the loop *in addition to `inv`*.
	In the case of a normal `while` loop the latter one could always be taken as negation of the loop
	condition
	A way to construct `forIn`/`whileM` invariant by specifying a condition `inv` which should hold
	at the end of each loop iteration (even the breaking one), and a condition `onDone` which should
	hold in the end of the loop *in addition to `inv`*.
	In the case of a normal `while` loop the latter one could always be taken as negation of the loop
	condition.

[Rob23oba]

Suggested change

	(inv : α → Pred) (onDone : α → Pred) : RepeatInvariant α α Pred
	(inv : α → Pred) (onDone : α → Pred) : RepeatInvariant α α Pred

[sgraf812]

Otherwise great!

[sgraf812]

Suggested change

	/--
	A way to construct `forIn`/`whileM` invarinat by specifying a condition `inv` which should hold
	at the end of each loop itreation (even the breaking one), and a condition `onDone` which should
	hold in the end of the loop *in addition to `inv`*.
	In the case of a normal `while` loop the latter one could always be taken as negation of the loop
	condition
	-/
	@[simp]
	noncomputable abbrev RepeatInvariant.withOnDone {α : Type u} {Pred : Type u} [Assertion Pred]
	(inv : α → Pred) (onDone : α → Pred) : RepeatInvariant α α Pred
	| .inl a => inv a
	| .inr a => inv a ⊓ onDone a
	/--
	Construct an invariant for a `while` loop from a loop invariant `inv` and the
	break condition `onBreak`.
	The `break` may appear anywhere in the loop, even in positions where `inv` does
	not hold. If there is no `break` in the while loop,
	`RepeatInvariant.ofWhileNoBreak` can be more convenient to use.
	-/
	noncomputable abbrev RepeatInvariant.ofWhile {α : Type u} {Pred : Type u} [Assertion Pred]
	(inv : α → Pred) (onBreak : α → Pred) : RepeatInvariant α α Pred
	| .inl a => inv a
	| .inr a => onBreak a
	/--
	Construct an invariant for a break-less `while` loop from a loop invariant
	`inv` and the negation of the loop condition `onBreak`.
	The resulting `RepeatInvariant` asserts that `inv` holds after the loop in
	addition to `onBreak`.
	-/
	noncomputable abbrev RepeatInvariant.ofWhileNoBreak {α : Type u} {Pred : Type u} [Assertion Pred]
	(inv : α → Pred) (onBreak : α → Pred) : RepeatInvariant α α Pred :=
	.ofWhile inv (inv ⊓ onBreak)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2b6ce0d8ecd456dff131ecbd990ae5069646a90c --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-18 10:01:50)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7821657e0630f8e0dd487658de0459202fd55670 --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-18 13:23:14)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2b6ce0d8ecd456dff131ecbd990ae5069646a90c --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-18 10:01:51)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7821657e0630f8e0dd487658de0459202fd55670 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-18 13:23:16)