From 4e7a2b2371b61b446c9be52f86fe2ddc8142749b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Oct 2025 19:51:21 -0700 Subject: [PATCH] feat: anchors for referencing terms in the `grind` state (#10709) This PR implements *anchors* (also known as stable hash codes) for referencing terms occurring in a `grind` goal. It also introduces the commands `show_splits` and `show_state`. The former displays the anchors for candidate case splits in the current `grind` goal. --- src/Init/Grind/Interactive.lean | 14 ++ src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 5 + src/Lean/Elab/Tactic/Grind/Show.lean | 153 +++++++++++++----- src/Lean/Meta/Tactic/Grind.lean | 1 + src/Lean/Meta/Tactic/Grind/Anchor.lean | 71 ++++++++ src/Lean/Meta/Tactic/Grind/Types.lean | 4 + tests/lean/run/grind_interactive.lean | 81 +++++++++- 7 files changed, 289 insertions(+), 40 deletions(-) create mode 100644 src/Lean/Meta/Tactic/Grind/Anchor.lean diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean index 92f8fcfc73..38e575f400 100644 --- a/src/Init/Grind/Interactive.lean +++ b/src/Init/Grind/Interactive.lean @@ -27,6 +27,9 @@ syntax (name := skip) "skip" : grind syntax (name := lia) "lia" : grind /-- `ring` (commutative) rings and fields. -/ syntax (name := ring) "ring" : grind +/-- The `sorry` tactic is a temporary placeholder for an incomplete tactic proof. -/ +syntax (name := «sorry») "sorry" : grind + /-- Instantiates theorems using E-matching. -/ syntax (name := instantiate) "instantiate" : grind @@ -56,6 +59,17 @@ syntax (name := showTrue) "show_true " showFilter : grind syntax (name := showFalse) "show_false " showFilter : grind /-- Shows equivalence classes of terms. -/ syntax (name := showEqcs) "show_eqcs " showFilter : grind +/-- Show case-split candidates. -/ +syntax (name := showSplits) "show_splits " showFilter : grind +/-- Show `grind` state. -/ +syntax (name := «showState») "show_state " showFilter : grind + +declare_syntax_cat grind_ref (behavior := both) + +syntax:max "#" noWs num : grind_ref +syntax term : grind_ref + +syntax (name := cases) "cases " grind_ref (" with " (colGt ident)+)? : grind /-- `done` succeeds iff there are no remaining goals. -/ syntax (name := done) "done" : grind diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean index 6415e42f2d..83e8c31eb2 100644 --- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean @@ -40,6 +40,11 @@ def evalGrindSeq : GrindTactic := fun stx => @[builtin_grind_tactic Parser.Tactic.Grind.«done»] def evalDone : GrindTactic := fun _ => done +@[builtin_grind_tactic Parser.Tactic.Grind.«sorry»] def evalSorry : GrindTactic := fun _ => do + let goal ← getMainGoal + goal.mvarId.admit + replaceMainGoal [] + @[builtin_grind_tactic skip] def evalSkip : GrindTactic := fun _ => return () diff --git a/src/Lean/Elab/Tactic/Grind/Show.lean b/src/Lean/Elab/Tactic/Grind/Show.lean index a34196c3ba..b36be1d0f8 100644 --- a/src/Lean/Elab/Tactic/Grind/Show.lean +++ b/src/Lean/Elab/Tactic/Grind/Show.lean @@ -8,6 +8,7 @@ prelude public import Lean.Elab.Tactic.Grind.Basic import Init.Grind.Interactive import Lean.Meta.Tactic.Grind.PP +import Lean.Meta.Tactic.Grind.Anchor namespace Lean.Elab.Tactic.Grind open Meta @@ -68,24 +69,33 @@ where | .fvar fvarId => return Option.isSome <| e.find? fun e => e.isFVar && e.fvarId! == fvarId | .gen pred => let gen ← getGen e; return pred gen +def ppAsserted? (filter : Filter) (collapsed := false) : GrindTacticM (Option MessageData) := do + let facts ← liftGoalM do (← get).facts.toArray.filterM fun e => filter.eval e + if facts.isEmpty then + return none + return some <| Grind.ppExprArray `facts "Asserted facts" facts (collapsed := collapsed) + @[builtin_grind_tactic showAsserted] def evalShowAsserted : GrindTactic := fun stx => withMainContext do match stx with | `(grind| show_asserted $[$filter?]?) => let filter ← elabFilter filter? - let facts ← liftGoalM do (← get).facts.toArray.filterM fun e => filter.eval e - if facts.isEmpty then - throwError "no facts" - logInfo <| Grind.ppExprArray `facts "Asserted facts" facts (collapsed := false) + let some msg ← ppAsserted? filter | throwError "no facts" + logInfo msg | _ => throwUnsupportedSyntax -def showProps (filter? : Option (TSyntax `show_filter)) (isTrue : Bool) : GrindTacticM Unit := withMainContext do - let filter ← elabFilter filter? +def ppProps? (filter : Filter) (isTrue : Bool) (collapsed := false) : GrindTacticM (Option MessageData) := do let props ← liftGoalM do let eqc ← getEqc (← if isTrue then getTrueExpr else getFalseExpr) eqc.toArray.filterM fun e => return (← filter.eval e) && !e.isTrue && !e.isFalse if props.isEmpty then - throwError s!"no {if isTrue then "true" else "false"} propositions" - logInfo <| Grind.ppExprArray `props s!"{if isTrue then "True" else "False"} propositions" props (collapsed := false) + return none + return some <| Grind.ppExprArray `props s!"{if isTrue then "True" else "False"} propositions" props (collapsed := collapsed) + +def showProps (filter? : Option (TSyntax `show_filter)) (isTrue : Bool) : GrindTacticM Unit := withMainContext do + let filter ← elabFilter filter? + let some msg ← ppProps? filter isTrue + | throwError s!"no {if isTrue then "true" else "false"} propositions" + logInfo msg @[builtin_grind_tactic showTrue] def evalShowTrue : GrindTactic := fun stx => do match stx with @@ -97,38 +107,109 @@ def showProps (filter? : Option (TSyntax `show_filter)) (isTrue : Bool) : GrindT | `(grind| show_false $[$filter?]?) => showProps filter? false | _ => throwUnsupportedSyntax +def ppEqcs? (filter : Filter) (collapsed := false) : GrindTacticM (Option MessageData) := liftGoalM do + let mut regularEqcs : Array MessageData := #[] + let mut otherEqcs : Array MessageData := #[] + let goal ← get + for eqc in goal.getEqcs (sort := true) do + if Option.isSome <| eqc.find? (·.isTrue) then + pure () + else if Option.isSome <| eqc.find? (·.isFalse) then + pure () + else if let e :: _ :: _ := eqc then + -- We may want to add a flag to pretty print equivalence classes of nested proofs + unless (← isProof e) do + /- + **Note**: If one element of the equivalence class satisfies the filter, we consider + the whole equivalence class to be relevant. Reason: you can view an equivalence + class `{a, b, c}` as a bunch of equations. Thus, if only `b` satisfies the filter, + then "morally" the equations `b = a` and `b = c` would also satisfy it. + -/ + if (← eqc.anyM fun e => filter.eval e) then + let mainEqc ← eqc.filterM fun e => return !(← isSupportApp e) + if mainEqc.length <= 1 then + otherEqcs := otherEqcs.push <| ppEqc eqc + else + let supportEqc ← eqc.filterM fun e => isSupportApp e + if supportEqc.isEmpty then + regularEqcs := regularEqcs.push <| ppEqc mainEqc + else + regularEqcs := regularEqcs.push <| ppEqc mainEqc #[ppEqc supportEqc] + unless otherEqcs.isEmpty do + regularEqcs := regularEqcs.push <| .trace { cls := `eqc } "others" otherEqcs + if regularEqcs.isEmpty then + return none + else + return MessageData.trace { cls := `eqc, collapsed } "Equivalence classes" regularEqcs + @[builtin_grind_tactic showEqcs] def evalShowEqcs : GrindTactic := fun stx => withMainContext do match stx with | `(grind| show_eqcs $[$filter?]?) => let filter ← elabFilter filter? - let info ← liftGoalM do - let mut regularEqcs : Array MessageData := #[] - let mut otherEqcs : Array MessageData := #[] - let goal ← get - for eqc in goal.getEqcs (sort := true) do - if Option.isSome <| eqc.find? (·.isTrue) then - pure () - else if Option.isSome <| eqc.find? (·.isFalse) then - pure () - else if let e :: _ :: _ := eqc then - -- We may want to add a flag to pretty print equivalence classes of nested proofs - unless (← isProof e) do - let eqc ← eqc.filterM fun e => filter.eval e - let mainEqc ← eqc.filterM fun e => return !(← isSupportApp e) - if mainEqc.length <= 1 then - otherEqcs := otherEqcs.push <| ppEqc eqc - else - let supportEqc ← eqc.filterM fun e => isSupportApp e - if supportEqc.isEmpty then - regularEqcs := regularEqcs.push <| ppEqc mainEqc - else - regularEqcs := regularEqcs.push <| ppEqc mainEqc #[ppEqc supportEqc] - unless otherEqcs.isEmpty do - regularEqcs := regularEqcs.push <| .trace { cls := `eqc } "others" otherEqcs - if regularEqcs.isEmpty then - throwError "no equivalence classes" - return MessageData.trace { cls := `eqc, collapsed := false } "Equivalence classes" regularEqcs - logInfo info + let some msg ← ppEqcs? filter | throwError "no equivalence classes" + logInfo msg + | _ => throwUnsupportedSyntax + +def pushIfSome (msgs : Array MessageData) (msg? : Option MessageData) : Array MessageData := + if let some msg := msg? then msgs.push msg else msgs + +@[builtin_grind_tactic showState] def evalShowState : GrindTactic := fun stx => withMainContext do + match stx with + | `(grind| show_state $[$filter?]?) => + let filter ← elabFilter filter? + let msgs := #[] + let msgs := pushIfSome msgs (← ppAsserted? filter (collapsed := true)) + let msgs := pushIfSome msgs (← ppProps? filter true (collapsed := true)) + let msgs := pushIfSome msgs (← ppProps? filter false (collapsed := true)) + let msgs := pushIfSome msgs (← ppEqcs? filter (collapsed := true)) + logInfo <| MessageData.trace { cls := `grind, collapsed := false } "Grind state" msgs + | _ => throwUnsupportedSyntax + +def truncateAnchors (es : Array (Expr × UInt64)) : Array (Expr × UInt64) × Nat := + go 4 +where + go (numDigits : Nat) : Array (Expr × UInt64) × Nat := Id.run do + if 4*numDigits < 64 then + let shift := 64 - 4*numDigits + let mut found : Std.HashSet UInt64 := {} + let mut result := #[] + for (e, a) in es do + let a' := a >>> shift.toUInt64 + if found.contains a' then + return (← go (numDigits+1)) + else + found := found.insert a' + result := result.push (e, a') + return (result, numDigits) + else + return (es, numDigits) + termination_by 64 - 4*numDigits + +def anchorToString (numDigits : Nat) (anchor : UInt64) : String := + let cs := Nat.toDigits 16 anchor.toNat + let n := cs.length + let zs := List.replicate (numDigits - n) '0' + let cs := zs ++ cs + cs.asString + +@[builtin_grind_tactic showSplits] def evalShowSplits : GrindTactic := fun stx => withMainContext do + match stx with + | `(grind| show_splits $[$filter?]?) => + let filter ← elabFilter filter? + let goal ← getMainGoal + let candidates := goal.split.candidates + let candidates ← liftGrindM <| candidates.toArray.mapM fun c => do + let e := c.getExpr + let anchor ← getAnchor e + return (e, anchor) + let (candidates, numDigits) := truncateAnchors candidates + let candidates ← liftGoalM <| candidates.filterM fun (e, _) => filter.eval e + if candidates.isEmpty then + throwError "no case splits" + let msgs := candidates.map fun (e, a) => + .trace { cls := `split } m!"#{anchorToString numDigits a} := {e}" #[] + let msg := MessageData.trace { cls := `splits, collapsed := false } "Case split candidates" msgs + logInfo msg | _ => throwUnsupportedSyntax end Lean.Elab.Tactic.Grind diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index 40147e56d6..db532e7ad6 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -41,6 +41,7 @@ public import Lean.Meta.Tactic.Grind.VarRename public import Lean.Meta.Tactic.Grind.ProofUtil public import Lean.Meta.Tactic.Grind.PropagateInj public import Lean.Meta.Tactic.Grind.Order +public import Lean.Meta.Tactic.Grind.Anchor public section diff --git a/src/Lean/Meta/Tactic/Grind/Anchor.lean b/src/Lean/Meta/Tactic/Grind/Anchor.lean new file mode 100644 index 0000000000..6ddb9c3e9e --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Anchor.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module +prelude +public import Lean.Meta.Tactic.Grind.Types +import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons +namespace Lean.Meta.Grind + +/-! +Anchor (aka stable hash) support for `grind`. We use +anchors to reference terms in the `grind` state. +-/ + +/-- +Hashes names for computing anchors (aka stable hash codes) +-/ +def hashName (n : Name) : UInt64 := + if n.hasMacroScopes || n.isInaccessibleUserName || n.isImplementationDetail then + 0 + else + hash n + +-- `mixHash` variant where `0` is treated as don't care +def mix (a b : UInt64) : UInt64 := + if a == 0 then b + else if b == 0 then a + else mixHash a b + +public partial def getAnchor (e : Expr) : GrindM UInt64 := do + if let some a := (← get).anchors.find? { expr := e } then + return a + let a ← match e with + | .const declName _ => pure <| hash declName + | .fvar fvarId => pure <| hashName (← fvarId.getDecl).userName + | .mdata _ b => getAnchor b + | .letE n v t b _ => + pure <| mix (hashName n) <| mix (← getAnchor t) <| mix (← getAnchor v) (← getAnchor b) + | .lam n d b _ | .forallE n d b _ => + pure <| mix (hashName n) <| mix (← getAnchor d) (← getAnchor b) + | .proj _ i s => pure <| mix (hash i) (← getAnchor s) + | .bvar idx => pure <| hash idx + | .lit v => pure <| hash v + | .app .. => e.withApp fun f args => do + if isMarkedSubsingletonConst f && args.size == 2 then + -- **Note**: we only visit the type of marked subsingleton terms. + getAnchor args[0]! + else + let pinfos ← if f.hasLooseBVars then + pure #[] + else + pure <| (← getFunInfo f).paramInfo + let mut r ← getAnchor f + for h : i in *...args.size do + let arg := args[i] + if h : i < pinfos.size then + let info := pinfos[i] + -- **Note**: we ignore implicit instances we computing stable hash codes + -- TODO: evaluate whether we should ignore regular implicit arguments too. + unless info.isInstImplicit do + r := mix r (← getAnchor arg) + else + r := mix r (← getAnchor arg) + pure r + | .sort _ | .mvar _ => pure 0 + modify fun s => { s with anchors := s.anchors.insert { expr := e } a } + return a + +end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 1aabb91f20..7071c08fc3 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -217,6 +217,10 @@ structure State where if it implements the `ReflCmp` type class. -/ reflCmpMap : PHashMap ExprPtr (Option Expr) := {} + /-- + Cached anchors (aka stable hash codes) for terms in the `grind` state. + -/ + anchors : PHashMap ExprPtr UInt64 := {} private opaque MethodsRefPointed : NonemptyType.{0} def MethodsRef : Type := MethodsRefPointed.type diff --git a/tests/lean/run/grind_interactive.lean b/tests/lean/run/grind_interactive.lean index facd8ee5dd..ee27ae8960 100644 --- a/tests/lean/run/grind_interactive.lean +++ b/tests/lean/run/grind_interactive.lean @@ -1,3 +1,5 @@ +set_option warn.sorry false + /-- error: `grind` failed case grind @@ -59,12 +61,12 @@ trace: [props] True propositions --- trace: [eqc] Equivalence classes [eqc] {bs, as.set i₁ v₁ ⋯} - [eqc] {as.size, bs.size, (as.set i₁ v₁ ⋯).size, (bs.set i₂ v₂ ⋯).size} - [eqc] {bs[j], (bs.set i₂ v₂ ⋯)[j]} + [eqc] {cs, bs.set i₂ v₂ ⋯} + [eqc] {as.size, bs.size, cs.size, (as.set i₁ v₁ ⋯).size, (bs.set i₂ v₂ ⋯).size} + [eqc] {cs[j], bs[j], (bs.set i₂ v₂ ⋯)[j]} [eqc] {if i₂ = j then v₂ else bs[j]} [eqc] others - [eqc] {bs.set i₂ v₂ ⋯} - [eqc] {↑as.size, ↑bs.size, ↑(bs.set i₂ v₂ ⋯).size} + [eqc] {↑as.size, ↑bs.size, ↑cs.size, ↑(bs.set i₂ v₂ ⋯).size} -/ #guard_msgs in example (as bs cs : Array α) (v₁ v₂ : α) @@ -131,3 +133,74 @@ h_2 : a * b ≤ 0 #guard_msgs in example {a b : Int} : a > 0 → b > 0 → a*b > 0 := by grind => finish + + +/-- +trace: [grind] Grind state + [facts] Asserted facts + [_] (bs.set i₂ v₂ ⋯).size = bs.size + [_] (as.set i₁ v₁ ⋯).size = as.size + [_] (bs.set i₂ v₂ ⋯)[j] = if i₂ = j then v₂ else bs[j] + [props] True propositions + [_] j < (bs.set i₂ v₂ ⋯).size + [_] j < bs.size + [eqc] Equivalence classes + [eqc] {as.size, bs.size, cs.size, (as.set i₁ v₁ ⋯).size, (bs.set i₂ v₂ ⋯).size} + [eqc] {cs[j], bs[j], (bs.set i₂ v₂ ⋯)[j]} + [eqc] {if i₂ = j then v₂ else bs[j]} + [eqc] others + [eqc] {↑as.size, ↑bs.size, ↑cs.size, ↑(bs.set i₂ v₂ ⋯).size} +-/ +#guard_msgs in +example (as bs cs : Array α) (v₁ v₂ : α) + (i₁ i₂ j : Nat) + (h₁ : i₁ < as.size) + (h₂ : bs = as.set i₁ v₁) + (h₃ : i₂ < bs.size) + (h₃ : cs = bs.set i₂ v₂) + (h₄ : i₁ ≠ j ∧ i₂ ≠ j) + (h₅ : j < cs.size) + (h₆ : j < as.size) + : cs[j] = as[j] := by + grind => + instantiate + show_state gen > 0 + instantiate + +/-- +trace: [splits] Case split candidates + [split] #7a08 := ¬p ∨ ¬q + [split] #8212 := ¬p ∨ q + [split] #fc16 := p ∨ ¬q + [split] #4283 := p ∨ q + [split] #0457 := p ∨ r +-/ +#guard_msgs (trace) in +example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by + grind => + show_splits + sorry + +def h (as : List Nat) := + match as with + | [] => 1 + | [_] => 2 + | _::_::_ => 3 + +/-- +trace: [splits] Case split candidates + [split] #7577 := match bs with + | [] => 1 + | [head] => 2 + | head :: head_1 :: tail => 3 + [split] #448c := match as with + | [] => 1 + | [head] => 2 + | head :: head_1 :: tail => 3 +-/ +#guard_msgs (trace) in +example : h bs = 1 → h as ≠ 0 := by + grind [h.eq_def] => + instantiate + show_splits + sorry