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

@@ -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

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 ()
 

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

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
 

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

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

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