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>
111 lines
3.2 KiB
Text
111 lines
3.2 KiB
Text
import Lean
|
|
|
|
open Lean
|
|
open Meta
|
|
|
|
def execShow (x : MetaM Expr) : MetaM Unit := do
|
|
let e ← x
|
|
IO.println (← ppExpr e)
|
|
|
|
/-
|
|
The `MetaM` has an ambient local context.
|
|
The local context contains the types of the free variables.
|
|
-/
|
|
|
|
def mkLam1 : MetaM Expr :=
|
|
/- The following `withLocalDecl` extends the local context with `(x : Nat)`, and executes the lambda
|
|
with an expression `x`. -/
|
|
withLocalDecl `x BinderInfo.default (mkConst `Nat) fun x =>
|
|
/- Similar to the method above, but sets `BinderInfo.default`. -/
|
|
withLocalDeclD `y (mkConst `Nat) fun y => do
|
|
-- Double backticks instruct Lean to resolve the names at compilation time
|
|
let b ← mkAppM ``HAdd.hAdd #[x, y] -- `x + y`
|
|
let b ← mkAppM ``HAdd.hAdd #[b, x] -- `x + y + x`
|
|
/- `mkLambdaFVars` converts the free variables into de-Bruijn bound variables, and construct the lambda for us. -/
|
|
mkLambdaFVars #[x, y] b
|
|
|
|
/-- info: fun x y => x + y + x -/
|
|
#guard_msgs in
|
|
#eval execShow mkLam1
|
|
|
|
/-- info: Nat → Nat → Nat -/
|
|
#guard_msgs in
|
|
#eval execShow do let e ← mkLam1; inferType e
|
|
|
|
def mkForall1 : MetaM Expr :=
|
|
withLocalDeclD `x (mkConst `Nat) fun x =>
|
|
withLocalDeclD `y (mkConst `Nat) fun y => do
|
|
let b ← mkEq x y
|
|
mkForallFVars #[x, y] b
|
|
|
|
/-- info: ∀ (x y : Nat), x = y -/
|
|
#guard_msgs in
|
|
#eval execShow mkForall1
|
|
|
|
def mkForall2Lambda : MetaM Expr := do
|
|
let e ← mkForall1
|
|
/- The following method `opens` a `forall` term, and expands the local context with
|
|
new free variables corresponding to the forall binders.
|
|
We also have a telescope function for `lambda` terms. -/
|
|
forallTelescopeReducing e fun xs b => do
|
|
IO.println s!">> {← xs.mapM Meta.ppExpr}"
|
|
IO.println s!">> {← ppExpr b}"
|
|
-- xs is an array of `Expr`
|
|
let b ← mkAppM ``HMul.hMul xs
|
|
mkLambdaFVars xs b
|
|
|
|
/--
|
|
info: >> #[x, y]
|
|
>> x = y
|
|
fun x y => x * y
|
|
-/
|
|
#guard_msgs in
|
|
#eval execShow mkForall2Lambda
|
|
|
|
def mkGoal : MetaM Expr :=
|
|
withLocalDeclD `x (mkConst `Nat) fun x =>
|
|
withLocalDeclD `y (mkConst `Nat) fun y => do
|
|
withLocalDeclD `h (← mkEq x y) fun h => do
|
|
let b ← mkEq y x
|
|
mkForallFVars #[x, y, h] b
|
|
|
|
/-- info: ∀ (x y : Nat), x = y → y = x -/
|
|
#guard_msgs in
|
|
#eval execShow mkGoal
|
|
|
|
def proveGoal : MetaM Unit := do
|
|
let g ← mkGoal
|
|
-- `main` is a metavariable representing the term we want to construct
|
|
let main ← mkFreshExprSyntheticOpaqueMVar g
|
|
let m := main.mvarId!
|
|
IO.println (← ppGoal m)
|
|
IO.println "-----"
|
|
let (xs, m) ← m.introNP 3 -- `intro` 3 variables using the binder names to name the new locals
|
|
IO.println (← ppGoal m)
|
|
IO.println "-----"
|
|
-- The `apply` tactic generates 0 or more subgoals
|
|
let [m] ← m.apply (mkConst ``Eq.symm [Level.one]) | throwError "unexpected number of subgoals"
|
|
IO.println (← ppGoal m)
|
|
IO.println "-----"
|
|
m.assumption
|
|
-- `main` contains the whole proof now
|
|
IO.println (← ppExpr main)
|
|
check main -- type check the proof. This is not the kernel type checker.
|
|
IO.println (← ppExpr (← inferType main))
|
|
|
|
/--
|
|
info: ⊢ ∀ (x y : Nat), x = y → y = x
|
|
-----
|
|
x y : Nat
|
|
h : x = y
|
|
⊢ y = x
|
|
-----
|
|
x y : Nat
|
|
h : x = y
|
|
⊢ x = y
|
|
-----
|
|
fun x y h => Eq.symm h
|
|
∀ (x y : Nat), x = y → y = x
|
|
-/
|
|
#guard_msgs in
|
|
#eval proveGoal
|