feat: add not_value constraint to grind_pattern (#11520)

This PR implements the constraint `not_value x` in the `grind_pattern`
command. It is the negation of the constraint `is_value`.

Author: leodemoura

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -115,6 +115,12 @@ where
       else if kind == ``isStrictValue then
         let (_, lhs) ← findLHS xs cnstr[1]
         return .isValue lhs true
+      else if kind == ``notValue then
+        let (_, lhs) ← findLHS xs cnstr[1]
+        return .notValue lhs false
+      else if kind == ``notStrictValue then
+        let (_, lhs) ← findLHS xs cnstr[1]
+        return .notValue lhs true
       else if kind == ``isGround then
         let (_, lhs) ← findLHS xs cnstr[1]
         return .isGround lhs

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -736,6 +736,7 @@ private def checkConstraints (thm : EMatchTheorem) (gen : Nat) (proof : Expr) (a
     | .depthLt lhs n => return (← getLHS args lhs).approxDepth.toNat < n
     | .isGround lhs => let lhs ← getLHS args lhs; return !lhs.hasFVar && !lhs.hasMVar
     | .isValue lhs strict => isValue (← getLHS args lhs) strict
+    | .notValue lhs strict => return !(← isValue (← getLHS args lhs) strict)
     | .sizeLt lhs n => checkSize (← getLHS args lhs) n
     | .genLt n => return gen < n
     | .maxInsts n =>

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -406,6 +406,11 @@ inductive EMatchTheoremConstraint where
     Similar to `guard`, but checks whether `e` is implied by asserting `¬e`.
     -/
     check (e : Expr)
+  | /--
+    Constraints of the form `not_value x` and `not_strict_value x`.
+    They are the negations of `is_value x` and `is_strict_value x`.
+    -/
+    notValue (bvarIdx : Nat) (strict : Bool)
   deriving Inhabited, Repr, BEq
 
 /-- A theorem for heuristic instantiation based on E-matching. -/

src/Lean/Meta/Tactic/Grind/Parser.lean

@@ -13,6 +13,8 @@ namespace GrindCnstr
 
 def isValue := leading_parser nonReservedSymbol "is_value " >> ident >> optional ";"
 def isStrictValue := leading_parser nonReservedSymbol "is_strict_value " >> ident >> optional ";"
+def notValue := leading_parser nonReservedSymbol "not_value " >> ident >> optional ";"
+def notStrictValue := leading_parser nonReservedSymbol "not_strict_value " >> ident >> optional ";"
 def isGround := leading_parser nonReservedSymbol "is_ground " >> ident >> optional ";"
 def sizeLt := leading_parser nonReservedSymbol "size " >> ident >> " < " >> numLit >> optional ";"
 def depthLt := leading_parser nonReservedSymbol "depth " >> ident >> " < " >> numLit >> optional ";"
@@ -27,7 +29,7 @@ end GrindCnstr
 
 open GrindCnstr in
 def grindPatternCnstr : Parser :=
-  isValue <|> isStrictValue <|> isGround <|> sizeLt <|> depthLt <|> genLt <|> maxInsts
+  isValue <|> isStrictValue <|> notValue <|> notStrictValue <|> isGround <|> sizeLt <|> depthLt <|> genLt <|> maxInsts
   <|> guard <|> GrindCnstr.check <|> notDefEq <|> defEq
 
 def grindPatternCnstrs : Parser := leading_parser "where " >> many1Indent (ppLine >> grindPatternCnstr)
@@ -92,6 +94,10 @@ a literal (`Nat`, `Int`, `String`, etc.), or a lambda `fun x => t`.
 
 - `is_strict_value x`: Similar to `is_value`, but without lambdas.
 
+- `not_value x`: The term bound to `x` is a **not** value (see `is_value`).
+
+- `not_strict_value x`: Similar to `not_value`, but without lambdas.
+
 - `gen < n`: The theorem instance has generation less than `n`. Recall that each term is assigned a
 generation, and terms produced by theorem instantiation have a generation that is one greater than
 the maximal generation of all the terms used to instantiate the theorem. This constraint complements

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

tests/lean/run/grind_pattern_cnstr_2.lean

@@ -293,3 +293,18 @@ example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
   grind
 
 end Ex13
+
+namespace Ex14
+
+opaque f : Nat → Nat
+axiom fax : f x ≤ x
+grind_pattern fax => f x where
+  not_value x
+
+/-- trace: [grind.ematch.instance] fax: f x ≤ x -/
+#guard_msgs in
+example : f 1 = a → f 2 = b → x ≤ y → f x ≤ y := by
+  set_option trace.grind.ematch.instance true in
+  grind
+
+end Ex14