From 78b09d5dccaed35c42d3c59b562134add8a67507 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 26 Sep 2025 14:57:49 +0200 Subject: [PATCH] feat: support case label like syntax in `mvcgen invariants` (#10570) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds support for case label like syntax in `mvcgen invariants` in order to refer to inaccessible names. Example: ```lean def copy (l : List Nat) : Id (Array Nat) := do let mut acc := #[] for x in l do acc := acc.push x return acc theorem copy_labelled_invariants (l : List Nat) : ⦃⌜True⌝⦄ copy l ⦃⇓ r => ⌜r = l.toArray⌝⦄ := by mvcgen [copy] invariants | inv1 acc => ⇓ ⟨xs, letMuts⟩ => ⌜acc = l.toArray⌝ with admit ``` --- src/Init/Tactics.lean | 9 +++++ src/Lean/Elab/Tactic/Do/VCGen.lean | 43 +++++++++++++++++++----- src/Std/Tactic/Do/Syntax.lean | 18 +++++++--- tests/lean/run/mvcgenInvariantsWith.lean | 32 ++++++++++++++++-- 4 files changed, 85 insertions(+), 17 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index fd0f152876..b6ef112683 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -2217,6 +2217,15 @@ mvcgen [...] invariants · I2 with grind ``` +When `I1` and `I2` need to refer to inaccessibles (`mvcgen` will introduce a lot of them for program +variables), you can use case label syntax: +``` +mvcgen [...] invariants +| inv1 _ acc _ => I1 acc +| _ => I2 +with grind +``` +This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`. ### Invariant suggestions diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 535a6c372a..8b952bb58f 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen.lean @@ -370,15 +370,40 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant match stx with | `(invariantAlts| $invariantsKW $alts*) => let invariants ← invariants.filterM (not <$> ·.isAssigned) + + let mut dotOrCase := LBool.undef -- .true => dot for h : n in 0...alts.size do - let alt := alts[n] - match alt with - | `(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}" + let alt := alts[n] + match alt with + | `(invariantDotAlt| · $rhs) => + if dotOrCase matches .false then + logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported." + break + dotOrCase := .true + let some mv := invariants[n]? | do + logErrorAt alt m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv` ({invariants.size})." + continue + withRef rhs do + discard <| evalTacticAt (← `(tactic| exact $rhs)) mv + | `(invariantCaseAlt| | $tag $args* => $rhs) => + if dotOrCase matches .true then + logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported." + break + dotOrCase := .false + let n? : Option Nat := do + let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal + let .str .anonymous s := tag.getId | none + s.dropPrefix? "inv" >>= Substring.toNat? + let some mv := do invariants[(← n?) - 1]? | do + logErrorAt alt m!"No invariant with label {tag} {repr tag}." + continue + if ← mv.isAssigned then + logErrorAt alt m!"Invariant {n?.get!} is already assigned." + continue + withRef rhs do + discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv + | _ => logErrorAt alt m!"Expected `invariantDotAlt`, got {alt}" + if let `(invariantsKW| invariants) := invariantsKW then if alts.size < invariants.size then let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType) @@ -391,7 +416,7 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant if ← mv.isAssigned then continue let invariant ← suggestInvariant mv - suggestions := suggestions.push (← `(invariantAlt| · $invariant)) + suggestions := suggestions.push (← `(invariantDotAlt| · $invariant)) let alts' := alts ++ suggestions let stx' ← `(invariantAlts|invariants $alts'*) if suggestions.size > 0 then diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index 3c7a398d34..268c72cbac 100644 --- a/src/Std/Tactic/Do/Syntax.lean +++ b/src/Std/Tactic/Do/Syntax.lean @@ -328,7 +328,12 @@ macro "mvcgen_trivial" : tactic => /-- An invariant alternative of the form `· term`, one per invariant goal. -/ -syntax invariantAlt := ppDedent(ppLine) cdotTk (colGe term) +syntax invariantDotAlt := ppDedent(ppLine) cdotTk (colGe term) + +/-- +An invariant alternative of the form `| inv a b c => term`, one per invariant goal. +-/ +syntax invariantCaseAlt := ppDedent(ppLine) "| " caseArg " => " (colGe term) /-- Either the contextual keyword ` invariants ` or its tracing form ` invariants? ` which suggests @@ -337,11 +342,14 @@ skeletons for missing invariants as a hint. syntax invariantsKW := &"invariants " <|> &"invariants? " /-- -After `mvcgen [...]`, there can be an optional `invariants` followed by a bulleted list of -invariants `· term; · term`. -The tracing variant ` invariants? ` will suggest a skeleton for missing invariants. +After `mvcgen [...]`, there can be an optional `invariants` followed by either +* a bulleted list of invariants `· term; · term`. +* a labelled list of invariants `| inv1 => term; inv2 a b c => term`, which is useful for naming + inaccessibles. +The tracing variant ` invariants? ` will suggest a skeleton for missing invariants; see the +docstring for `mvcgen`. -/ -syntax invariantAlts := invariantsKW withPosition((colGe invariantAlt)*) +syntax invariantAlts := invariantsKW withPosition((colGe (invariantDotAlt <|> invariantCaseAlt))*) /-- In induction alternative, which can have 1 or more cases on the left diff --git a/tests/lean/run/mvcgenInvariantsWith.lean b/tests/lean/run/mvcgenInvariantsWith.lean index 67a4b9b492..417c30834e 100644 --- a/tests/lean/run/mvcgenInvariantsWith.lean +++ b/tests/lean/run/mvcgenInvariantsWith.lean @@ -94,7 +94,7 @@ theorem test_with_pretac {m : Option Nat} (h : m = some 4) : (match m with | some n => (set n : StateM Nat PUnit) | none => set 0) - ⦃⇓ r s => ⌜s = 4⌝⦄ := by + ⦃⇓ _ s => ⌜s = 4⌝⦄ := by mvcgen with simp_all theorem test_with_cases {m : Option Nat} (h : m = some 4) : @@ -102,7 +102,7 @@ theorem test_with_cases {m : Option Nat} (h : m = some 4) : (match m with | some n => (set n : StateM Nat PUnit) | none => set 0) - ⦃⇓ r s => ⌜s = 4⌝⦄ := by + ⦃⇓ _ s => ⌜s = 4⌝⦄ := by mvcgen with | vc1 => grind @@ -113,7 +113,7 @@ theorem test_with_pretac_cases {m : Option Nat} (h : m = some 4) : (match m with | some n => (set n : StateM Nat PUnit) | none => set 0) - ⦃⇓ r s => ⌜s = 4⌝⦄ := by + ⦃⇓ _ s => ⌜s = 4⌝⦄ := by mvcgen with simp -- `simp` is a no-op on some goals, but it should not fail | vc1 => grind @@ -193,3 +193,29 @@ theorem nodup_twice_missing_two_invariants (l : List Int) : nodup_twice l ↔ l. mvcgen invariants with grind + +def copy (l : List Nat) : Id (Array Nat) := do + let mut acc := #[] + for x in l do + acc := acc.push x + return acc + +set_option warn.sorry false in +theorem copy_labelled_invariants (l : List Nat) : ⦃⌜True⌝⦄ copy l ⦃⇓ r => ⌜r = l.toArray⌝⦄ := by + mvcgen [copy] invariants + | inv1 acc => ⇓ ⟨xs, letMuts⟩ => ⌜acc = l.toArray⌝ + with admit + +set_option warn.sorry false in +theorem copy_labelled_invariants_noname (l : List Nat) : ⦃⌜True⌝⦄ copy l ⦃⇓ r => ⌜r = l.toArray⌝⦄ := by + mvcgen [copy] invariants + | _ acc => ⇓ ⟨xs, letMuts⟩ => ⌜acc = l.toArray⌝ + with admit + +/-- error: Alternation between labelled and bulleted invariants is not supported. -/ +#guard_msgs in +theorem copy_labelled_invariants_dontmix (l : List Nat) : ⦃⌜True⌝⦄ copy l ⦃⇓ r => ⌜r = l.toArray⌝⦄ := by + mvcgen [copy] invariants + · ⇓ ⟨xs, letMuts⟩ => ⌜True⌝ + | _ acc => ⇓ ⟨xs, letMuts⟩ => ⌜acc = l.toArray⌝ + with admit