From 90ef90b462f8a94d0189956680853fa17d4a9a72 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Tue, 19 Aug 2025 16:51:19 +0200 Subject: [PATCH] feat: change extended syntax for `mvcgen invariants ... with ...` (#9989) This PR changes the new extended syntax for `mvcgen` to `mvcgen invariants ... with ...`. --- src/Lean/Elab/Tactic/Do/VCGen.lean | 34 ++++---- src/Std/Tactic/Do/Syntax.lean | 11 ++- tests/lean/run/9581.lean | 2 +- ...ingWith.lean => mvcgenInvariantsWith.lean} | 85 ++++++++++++------- 4 files changed, 74 insertions(+), 58 deletions(-) rename tests/lean/run/{mvcgenUsingWith.lean => mvcgenInvariantsWith.lean} (71%) diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 2af6c26022..44b0161edf 100644 --- 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`." - 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`. 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` ({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 diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index 9559cfbe36..39738f27b9 100644 --- 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 `| , ..., => 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 | ... | => 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 diff --git a/tests/lean/run/9581.lean b/tests/lean/run/9581.lean index 087acfa8d0..04d496358f 100644 --- 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 diff --git a/tests/lean/run/mvcgenUsingWith.lean b/tests/lean/run/mvcgenInvariantsWith.lean similarity index 71% rename from tests/lean/run/mvcgenUsingWith.lean rename to tests/lean/run/mvcgenInvariantsWith.lean index 7aaaafa66d..67a4b9b492 100644 --- a/tests/lean/run/mvcgenUsingWith.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