e82cd9b62c
This PR refines how the `apply` tactic (and related tactics like `rewrite`) name and tag the remaining subgoals. Assigned metavariables are now filtered out *before* computing subgoal tags. As a consequence, when only one unassigned subgoal remains, it inherits the tag of the input goal instead of being given a fresh suffixed tag. User-visible effect: proof states that previously displayed tags like `case h`, `case a`, or `case upper.h` for a single remaining goal now display the input goal's tag directly (e.g. no tag at all, or `case upper`). This removes noise from `funext`, `rfl`-style, and `induction`-alternative goals when the applied lemma introduces only one non-assigned metavariable. Multi-goal applications are unaffected — their subgoals continue to receive distinguishing suffixes. This may affect users whose proofs rely on the previous tag names (for example, `case h => ...` after `funext`). Such scripts need to be updated to use the input goal's tag instead. --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
43 lines
1.9 KiB
Text
43 lines
1.9 KiB
Text
decreasing_by.lean:34:0-39:17: error: Could not find a decreasing measure.
|
|
The basic measures relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
n m
|
|
1) 34:29-43 = ?
|
|
2) 34:46-62 ? _
|
|
Please use `termination_by` to specify a decreasing measure.
|
|
decreasing_by.lean:61:0-67:19: error: Could not find a decreasing measure.
|
|
The basic measures relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
n m
|
|
1) 61:29-43 = ?
|
|
2) 61:46-62 ? _
|
|
Please use `termination_by` to specify a decreasing measure.
|
|
decreasing_by.lean:75:0-75:13: error: unsolved goals
|
|
n m : Nat
|
|
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m)
|
|
|
|
n m : Nat
|
|
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
|
|
decreasing_by.lean:85:0-85:22: error: unsolved goals
|
|
n m : Nat
|
|
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m)
|
|
|
|
n m : Nat
|
|
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
|
|
decreasing_by.lean:93:0-94:22: error: Could not find a decreasing measure.
|
|
The basic measures relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
n m
|
|
1) 93:29-43 = ?
|
|
2) 93:46-62 ? _
|
|
Please use `termination_by` to specify a decreasing measure.
|
|
decreasing_by.lean:104:0-106:17: error: unsolved goals
|
|
n m : Nat
|
|
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
|
|
decreasing_by.lean:114:0-117:17: error: Could not find a decreasing measure.
|
|
The basic measures relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
n m
|
|
1) 114:29-43 = ?
|
|
2) 114:46-62 ? _
|
|
Please use `termination_by` to specify a decreasing measure.
|