fix: instantiateTheorem in grind (#8369)

This PR fixes a type error at `instantiateTheorem` function used in
`grind`. It was failing to instantiate theorems such as
```lean
theorem getElem_reverse {xs : Array α} {i : Nat} (hi : i < xs.reverse.size)
    : (xs.reverse)[i] = xs[xs.size - 1 - i]'(by simp at hi; omega)
```
in examples such as
```lean
example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2)
    : xs[j] = xs[xs.size - 1 - j]
```
generating the issue
```lean
  [issue] type error constructing proof for Array.getElem_reverse
      when assigning metavariable ?hi with
        ‹j < xs.toList.length›
      has type
        j < xs.toList.length : Prop
      but is expected to have type
        j < xs.reverse.size : Prop
```

Author: leodemoura

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

@@ -89,6 +89,9 @@ private def assign? (c : Choice) (bidx : Nat) (e : Expr) : OptionT GoalM Choice
     -- `Choice` was not properly initialized
     unreachable!
 
+private def unassign (c : Choice) (bidx : Nat) : Choice :=
+  { c with assignment := c.assignment.set! bidx unassigned }
+
 /--
 Returns `true` if the function `pFn` of a pattern is equivalent to the function `eFn`.
 Recall that we ignore universe levels in patterns.
@@ -290,6 +293,63 @@ private def addNewInstance (thm : EMatchTheorem) (proof : Expr) (generation : Na
   trace_goal[grind.ematch.instance] "{← thm.origin.pp}: {prop}"
   addTheoremInstance thm proof prop (generation+1)
 
+private def synthesizeInsts (mvars : Array Expr) (bis : Array BinderInfo) : OptionT M Unit := do
+  let thm := (← read).thm
+  for mvar in mvars, bi in bis do
+    if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
+      let type ← inferType mvar
+      unless (← synthesizeInstanceAndAssign mvar type) do
+        reportIssue! "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
+        failure
+
+private def applyAssignment (mvars : Array Expr) : OptionT (StateT Choice M) Unit := do
+  let thm := (← read).thm
+  let numParams := thm.numParams
+  for h : i in [:mvars.size] do
+    let bidx := numParams - i - 1
+    let mut v := (← get).assignment[bidx]!
+    unless isSameExpr v unassigned do
+      let mvarId := mvars[i].mvarId!
+      let mvarIdType ← mvarId.getType
+      let vType ← inferType v
+      let unassignOrFail : OptionT (StateT Choice M) Unit := do
+        /-
+        If there is type error and `vType` is a proposition, we can still instantiate the
+        theorem by unassigning `v` and using it as an extra hypothesis.
+        Here is an example to motivate the unassignment.
+        ```
+        example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2)
+            : xs[j] = xs[xs.size - 1 - j] := by
+          grind
+        ```
+        Without the unassignment we get a type error while trying to instantiate the theorem
+        ```
+        theorem getElem_reverse {xs : Array α} {i : Nat} (hi : i < xs.reverse.size) :
+          (xs.reverse)[i] = xs[xs.size - 1 - i]'(by simp at hi; omega)
+        ```
+        The pattern for this theorem is `xs.reverese[i]`. Note that `hi` occurs there as an implicit argument.
+        The term `xs[j]` in our goal e-matches the pattern because we have the equality `xs.reverse = xs`.
+        However, the implicit proof at `xs[j]` has type `j < xs.size` instead of `j < xs.reverse.size`.
+        -/
+        if (← isProp vType) then
+          modify (unassign · bidx)
+        else
+          reportIssue! "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
+          failure
+      unless (← withDefault <| isDefEq mvarIdType vType) do
+        if let some heq ← withoutReportingMVarIssues <| proveEq? vType mvarIdType (abstract := true) then
+          /-
+          Some of the `cast`s will appear inside the `Grind.MatchCond` binders, and
+          we want their proofs to be properly wrapped.
+          -/
+          let heq := mkApp2 (mkConst ``Grind.nestedProof) (← mkEq vType mvarIdType) heq
+          v ← mkAppM ``cast #[heq, v]
+        else
+          unassignOrFail
+          continue
+      unless (← mvarId.checkedAssign v) do
+        unassignOrFail
+
 /--
 After processing a (multi-)pattern, use the choice assignment to instantiate the proof.
 Missing parameters are synthesized using type inference and type class synthesis."
@@ -306,35 +366,8 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   if mvars.size != thm.numParams then
     reportIssue! "unexpected number of parameters at {← thm.origin.pp}"
     return ()
-  -- Apply assignment
-  for h : i in [:mvars.size] do
-    let mut v := c.assignment[numParams - i - 1]!
-    unless isSameExpr v unassigned do
-      let mvarId := mvars[i].mvarId!
-      let mvarIdType ← mvarId.getType
-      let vType ← inferType v
-      let report : M Unit := do
-        reportIssue! "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
-      unless (← withDefault <| isDefEq mvarIdType vType) do
-        let some heq ← withoutReportingMVarIssues <| proveEq? vType mvarIdType (abstract := true)
-          | report
-            return ()
-        /-
-        Some of the `cast`s will appear inside the `Grind.MatchCond` binders, and
-        we want their proofs to be properly wrapped.
-        -/
-        let heq := mkApp2 (mkConst ``Grind.nestedProof) (← mkEq vType mvarIdType) heq
-        v ← mkAppM ``cast #[heq, v]
-      unless (← mvarId.checkedAssign v) do
-        report
-        return ()
-  -- Synthesize instances
-  for mvar in mvars, bi in bis do
-    if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
-      let type ← inferType mvar
-      unless (← synthesizeInstanceAndAssign mvar type) do
-        reportIssue! "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
-        return ()
+  let (some _, c) ← applyAssignment mvars |>.run c | return ()
+  let some _ ← synthesizeInsts mvars bis | return ()
   let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
     addNewInstance thm proof c.gen

tests/lean/grind/palindrome.lean

@@ -0,0 +1,5 @@
+set_option grind.warning false
+
+example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2) :
+    xs[j] = xs[xs.size - 1 - j] := by
+  grind

tests/lean/run/grind_ematch_type_error.lean

@@ -0,0 +1,44 @@
+set_option grind.warning false
+
+def IsPalindrome (xs : Array Nat) : Prop := xs.reverse = xs
+
+def checkPalin1 (xs : Array Nat) : Bool :=
+  go 0
+where
+  go  (i : Nat) :=
+    if h : i < xs.size / 2 then
+      if xs[i] = xs[xs.size - 1 - i] then
+        go (i + 1)
+      else
+        false
+    else
+      true
+
+example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2) :
+    xs[j] = xs[xs.size - 1 - j] := by
+  grind
+
+theorem checkPalin1_correct' : checkPalin1 xs = true ↔ IsPalindrome xs := by
+  unfold checkPalin1
+  suffices ∀ i, checkPalin1.go xs i = true ↔ ∀ j, i ≤ j → (_ : j < xs.size / 2) → xs[j] = xs[xs.size - 1 - j] by
+    rw [this, IsPalindrome]
+    constructor
+    · intro w
+      ext i hi₁ hi₂
+      · grind
+      · by_cases h : i < xs.size / 2 <;> grind
+    · intro w
+      intro j hj hj'
+      grind
+  intro i
+  fun_induction checkPalin1.go
+  case case1 j h₁ h₂ ih =>
+    constructor
+    · intro w j'
+      by_cases j' = j <;> grind
+    · grind
+  case case2 j h₁ h₂ =>
+    simp only [Bool.false_eq_true, false_iff, Classical.not_forall]
+    refine ⟨j, by grind⟩
+  case case3 x h =>
+    grind