fix: zetaDelta at Sym/Pattern.lean

This PR fixes missing zetaDelta support at the pattern
matching/unification procedure in the new Sym framework.

src/Lean/Meta/Sym/Apply.lean

@@ -113,6 +113,6 @@ public def BackwardRule.apply (goal : Goal) (rule : BackwardRule) : SymM (List G
       let mvarId := result.args[i]!.mvarId!
       { goal with mvarId }
   else
-    throwError "rule is not applicable to goal{goal.mvarId}\nrule:{indentExpr rule.expr}"
+    throwError "rule is not applicable to goal{goal.mvarId}rule:{indentExpr rule.expr}"
 
 end Lean.Meta.Sym

src/Lean/Meta/Sym/Pattern.lean

@@ -197,9 +197,9 @@ partial def process (p : Expr) (e : Expr) : UnifyM Bool := do
   | .bvar bidx => assignExpr bidx e
   | .mdata _ p => process p e
   | .const declName us =>
-    processConst declName us e <||> checkMVar p e
+    processConst declName us e <||> checkLetVar p e <||> checkMVar p e
   | .sort u =>
-    processSort u e <||> checkMVar p e
+    processSort u e <||> checkLetVar p e <||> checkMVar p e
   | .app .. =>
     processApp p e <||> checkMVar p e
   | .forallE .. | .lam .. =>
@@ -219,6 +219,12 @@ partial def process (p : Expr) (e : Expr) : UnifyM Bool := do
     pure (p == e) <||> checkMVar p e
   | .letE .. => unreachable!
 where
+  checkLetVar (p : Expr) (e : Expr) : UnifyM Bool := do
+    unless (← read).zetaDelta do return false
+    let .fvar fvarId := e | return false
+    let some value ← fvarId.getValue? | return false
+    process p value
+
   processApp (p : Expr) (e : Expr) : UnifyM Bool := do
     let f := p.getAppFn
     let .const declName _ := f | processAppDefault p e
@@ -228,7 +234,7 @@ where
 
   processAppWithInfo (p : Expr) (e : Expr) (i : Nat) (info : ProofInstInfo) : UnifyM Bool := do
     let .app fp ap := p | if e.isApp then return false else process p e
-    let .app fe ae := e | return false
+    let .app fe ae := e | checkLetVar p e
     unless (← processAppWithInfo fp fe (i - 1) info) do return false
     if h : i < info.argsInfo.size then
       let argInfo := info.argsInfo[i]
@@ -249,7 +255,7 @@ where
 
   processAppDefault (p : Expr) (e : Expr) : UnifyM Bool := do
     let .app fp ap := p | if e.isApp then return false else process p e
-    let .app fe ae := e | return false
+    let .app fe ae := e | checkLetVar p e
     unless (← processAppDefault fp fe) do return false
     process ap ae
 
@@ -257,6 +263,7 @@ where
     let .const declName' us' := e | return false
     unless declName == declName' do return false
     processLevels us us'
+
   processSort (u : Level) (e : Expr) : UnifyM Bool := do
     let .sort v := e | return false
     processLevel u v

tests/lean/run/sym_pattern.lean

@@ -49,3 +49,20 @@ info: @Exists.intro Nat (fun x => And (p x) (@Eq Nat x Nat.zero)) Nat.zero
 #guard_msgs in
 set_option pp.explicit true in
 #eval SymM.run' test2
+
+opaque a : Nat
+opaque bla : Nat → Nat → Nat
+opaque foo : Type → Nat → Nat
+axiom pFoo (x : Nat) : p (foo Prop (bla x 1))
+
+def test3 : SymM Unit := do
+  withLetDecl `x (.sort 1) (.sort 0) fun x =>
+  withLetDecl `y (mkConst ``Nat) (mkNatLit 1) fun y => do
+  let target := mkApp (mkConst ``p) (mkApp2 (mkConst ``foo) x (mkApp2 (mkConst ``bla) (mkNatAdd (mkNatLit 3) y) y))
+  let mvar ← mkFreshExprMVar target
+  let goal ← Sym.mkGoal mvar.mvarId!
+  let rule ← mkBackwardRuleFromDecl ``pFoo
+  let [] ← rule.apply goal | throwError "failed"
+  logInfo mvar
+
+#eval SymM.run' test3