feat: change extended syntax for mvcgen invariants ... with ... (#9989)

This PR changes the new extended syntax for `mvcgen` to `mvcgen invariants ... with ...`.
2025-08-19 16:51:19 +02:00 · 2025-08-19 16:51:19 +02:00 · 90ef90b462
commit 90ef90b462
parent cab46ea3d1
4 changed files with 74 additions and 58 deletions
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@ -365,25 +365,23 @@ end VCGen
 def elabInvariants (stx : Syntax) (invariants : Array MVarId) : TacticM Unit := do
  let some stx := stx.getOptional? | return ()
  let stx : TSyntax ``invariantAlts := ⟨stx⟩
+  withRef stx do
  match stx with
-  | `(invariantAlts| using invariants $alts*) =>
-    for alt in alts do
+  | `(invariantAlts| invariants $alts*) =>
+    let invariants ← invariants.filterM (not <$> ·.isAssigned)
+    for h : n in [0:alts.size] do
+      let alt := alts[n]
      match alt with
-      | `(invariantAlt| | $ns,* => $rhs) =>
-        for ref in ns.getElems do
-          let n := ref.getNat
-          if n = 0 then
-            logErrorAt ref "Invariant index 0 is invalid. Invariant indices start at 1 just as the case labels `inv<n>`."
-            continue
-          let some mv := invariants[n-1]? | do
-            logErrorAt ref m!"Invariant index {n} is out of bounds. Invariant indices start at 1 just as the case labels `inv<n>`. There were {invariants.size} invariants."
-            continue
-          if ← mv.isAssigned then
-            logErrorAt ref m!"Invariant {n} is already assigned"
-            continue
-          discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
-      | _ => logErrorAt alt "Expected invariantAlt, got {alt}"
-  | _ => logErrorAt stx "Expected invariantAlts, got {stx}"
+      | `(invariantAlt| · $rhs) =>
+        let some mv := invariants[n]? | do
+          logErrorAt rhs m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv<n>` ({invariants.size})."
+          continue
+        discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
+      | _ => logErrorAt alt m!"Expected invariantAlt, got {alt}"
+    if alts.size < invariants.size then
+      let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType)
+      throwErrorAt stx m!"Lacking definitions for the following invariants.\n{toMessageList missingTypes}"
+  | _ => logErrorAt stx m!"Expected invariantAlts, got {stx}"

 private def patchVCAltIntoCaseTactic (alt : TSyntax ``vcAlt) : TSyntax ``case :=
  -- syntax vcAlt := sepBy1(caseArg, " | ") " => " tacticSeq
@ -397,7 +395,7 @@ partial def elabVCs (stx : Syntax) (vcs : Array MVarId) : TacticM (List MVarId)
    let vcs ← applyPreTac vcs tactic
    evalAlts vcs alts
  | _ =>
-    logErrorAt stx "Expected inductionAlts, got {stx}"
+    logErrorAt stx m!"Expected inductionAlts, got {stx}"
    return vcs.toList
 where
  applyPreTac (vcs : Array MVarId) (tactic : Option Syntax) : TacticM (Array MVarId) := do
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@ -325,16 +325,15 @@ macro "mvcgen_trivial" : tactic =>
  )

 /--
-An invariant alternative of the form `| <n₁>, ..., <nₖ> => term`, where `nᵢ` are natural numbers
-referring to numbered invariant goals.
+An invariant alternative of the form `· term`, one per invariant goal.
 -/
-syntax invariantAlt  := ppDedent(ppLine) withPosition("| " num,+) " => " term
+syntax invariantAlt  := ppDedent(ppLine) cdotTk (colGe term)

 /--
-After `using`, there can be an optional ` invariants ` followed by a list of alternatives
-`| 1 => term | ... | <n> => term`.
+After `mvcgen [...]`, there can be an optional `invariants` followed by a bulleted list of
+invariants `· term; · term`.
 -/
-syntax invariantAlts := " using" (&" invariants " withPosition((colGe invariantAlt)*))?
+syntax invariantAlts := &" invariants" withPosition((colGe invariantAlt)*)

 /--
 In induction alternative, which can have 1 or more cases on the left
--- a/tests/lean/run/9581.lean
+++ b/tests/lean/run/9581.lean
@ -34,5 +34,5 @@ theorem F_spec_using_with :
   F
   ⦃⇓ _ => ⌜1 < 2⌝⦄ := by
  mvcgen [F]
-  using invariants | 1 => ⇓ _ => ⌜1 < 2⌝
+  invariants · ⇓ _ => ⌜1 < 2⌝
  with omega
--- a/tests/lean/run/mvcgenInvariantsWith.lean
+++ b/tests/lean/run/mvcgenInvariantsWith.lean
@ -25,32 +25,32 @@ theorem nodup_correct_vanilla (l : List Int) : nodup l ↔ l.Nodup := by
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
  all_goals mleave; grind

-theorem nodup_correct_using (l : List Int) : nodup l ↔ l.Nodup := by
+theorem nodup_correct_invariants (l : List Int) : nodup l ↔ l.Nodup := by
  generalize h : nodup l = r
  apply Id.of_wp_run_eq h
-  mvcgen using invariants
-  | 1 => Invariant.withEarlyReturn
-      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
-      (onContinue := fun traversalState seen =>
-        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
+  mvcgen invariants
+  · Invariant.withEarlyReturn
+   (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝) -- minimal indentation here is part of the test
+   (onContinue := fun traversalState seen =>
+   ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
  all_goals grind

-theorem nodup_correct_using_with_pretac (l : List Int) : nodup l ↔ l.Nodup := by
+theorem nodup_correct_invariants_with_pretac (l : List Int) : nodup l ↔ l.Nodup := by
  generalize h : nodup l = r
  apply Id.of_wp_run_eq h
-  mvcgen using invariants
-  | 1 => Invariant.withEarlyReturn
+  mvcgen invariants
+  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
  with grind

-theorem nodup_correct_using_with_cases (l : List Int) : nodup l ↔ l.Nodup := by
+theorem nodup_correct_invariants_with_cases (l : List Int) : nodup l ↔ l.Nodup := by
  generalize h : nodup l = r
  apply Id.of_wp_run_eq h
  mvcgen
-  using invariants
-  | 1 => Invariant.withEarlyReturn
+  invariants
+  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
@ -61,12 +61,12 @@ theorem nodup_correct_using_with_cases (l : List Int) : nodup l ↔ l.Nodup := b
  | vc4 => grind
  | vc5 => grind

-theorem nodup_correct_using_with_pretac_cases (l : List Int) : nodup l ↔ l.Nodup := by
+theorem nodup_correct_invariants_with_pretac_cases (l : List Int) : nodup l ↔ l.Nodup := by
  generalize h : nodup l = r
  apply Id.of_wp_run_eq h
  mvcgen
-  using invariants
-  | 1 => Invariant.withEarlyReturn
+  invariants
+  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
@ -75,12 +75,12 @@ theorem nodup_correct_using_with_pretac_cases (l : List Int) : nodup l ↔ l.Nod
  | vc2 | vc3 | vc4 => grind
  | vc5 => grind

-theorem nodup_correct_using_with_cases_error (l : List Int) : nodup l ↔ l.Nodup := by
+theorem nodup_correct_invariants_with_cases_error (l : List Int) : nodup l ↔ l.Nodup := by
  generalize h : nodup l = r
  apply Id.of_wp_run_eq h
  mvcgen
-  using invariants
-  | 1 => Invariant.withEarlyReturn
+  invariants
+  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
@ -132,45 +132,64 @@ def nodup_twice (l : List Int) : Bool := Id.run do
    seen2 := seen2.insert x
  return true

-theorem nodup_twice_correct_using_with (l : List Int) : nodup_twice l ↔ l.Nodup := by
+theorem nodup_twice_correct_invariants_with (l : List Int) : nodup_twice l ↔ l.Nodup := by
  generalize h : nodup_twice l = r
  apply Id.of_wp_run_eq h
  mvcgen
-  using invariants
-  | 1 => Invariant.withEarlyReturn
+  invariants
+  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
-  | 2 => Invariant.withEarlyReturn
+  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
  with grind

-theorem nodup_twice_correct_using_multiple_with (l : List Int) : nodup_twice l ↔ l.Nodup := by
+theorem nodup_twice_correct_invariants_multiple_with (l : List Int) : nodup_twice l ↔ l.Nodup := by
  generalize h : nodup_twice l = r
  apply Id.of_wp_run_eq h
  mvcgen
-  using invariants
-  | 1, 2 => Invariant.withEarlyReturn
+  invariants
+  · Invariant.withEarlyReturn
+      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
+      (onContinue := fun traversalState seen =>
+        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
+  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
  with grind

-/-- error: Invariant 2 is already assigned -/
+/--
+error: Lacking definitions for the following invariants.
+
+  Invariant l (MProd (Option Bool) (HashSet Int)) PostShape.pure
+-/
 #guard_msgs in
-theorem nodup_twice_correct_using_multiple_error (l : List Int) : nodup_twice l ↔ l.Nodup := by
+theorem nodup_twice_missing_one_invariant (l : List Int) : nodup_twice l ↔ l.Nodup := by
  generalize h : nodup_twice l = r
  apply Id.of_wp_run_eq h
  mvcgen
-  using invariants
-  | 1, 2 => Invariant.withEarlyReturn
-      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
-      (onContinue := fun traversalState seen =>
-        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
-  | 2 => Invariant.withEarlyReturn
+  invariants
+  · Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
  with grind
+
+/--
+error: Lacking definitions for the following invariants.
+
+  Invariant l (MProd (Option Bool) (HashSet Int)) PostShape.pure
+  ⏎
+  Invariant l (MProd (Option Bool) (HashSet Int)) PostShape.pure
+-/
+#guard_msgs in
+theorem nodup_twice_missing_two_invariants (l : List Int) : nodup_twice l ↔ l.Nodup := by
+  generalize h : nodup_twice l = r
+  apply Id.of_wp_run_eq h
+  mvcgen
+  invariants
+  with grind