feat: simplify and improve processAssignmentFOApproxAux

src/Init/Lean/Meta/ExprDefEq.lean

@@ -540,66 +540,10 @@ else do
     v ← instantiateMVars v;
     checkAssignmentAux mvarId mvarDecl fvars hasCtxLocals v
 
-/-
-  We try to unify arguments before we try to unify the functions.
-  The motivation is the following: the universe constraints in
-  the arguments propagate to the function. -/
-private partial def isDefEqFOApprox (f₁ f₂ : Expr) (args₁ args₂ : Array Expr) : Nat → Nat → MetaM Bool
-| i₁, i₂ =>
-  if h : i₂ < args₂.size then
-    let arg₁ := args₁.get! i₁;
-    let arg₂ := args₂.get ⟨i₂, h⟩;
-    condM (isExprDefEqAux arg₁ arg₂)
-      (isDefEqFOApprox (i₁+1) (i₂+1))
-      (pure false)
-  else
-    isExprDefEqAux f₁ f₂
-
 private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
-let vArgs := v.getAppArgs;
-if vArgs.isEmpty then
-  /- ?m a_1 ... a_k =?= t,  where t is not an application -/
-  pure false
-else if args.size > vArgs.size then
-  /-
-    ?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k
-
-    reduces to
-
-    ?m a_1 ... a_i =?= f
-    a_{i+1}        =?= b_1
-    ...
-    a_{i+k}        =?= b_k
-  -/
-  let f₁ := mkAppRange mvar 0 (args.size - vArgs.size) args;
-  let i₁ := args.size - vArgs.size;
-  isDefEqFOApprox f₁ v.getAppFn args vArgs i₁ 0
-else if args.size < vArgs.size then
-  /-
-    ?m a_1 ... a_k =?= f b_1 ... b_i b_{i+1} ... b_{i+k}
-
-    reduces to
-
-    ?m  =?= f b_1 ... b_i
-    a_1 =?= b_{i+1}
-    ...
-    a_k =?= b_{i+k}
-  -/
-  let vFn := mkAppRange v.getAppFn 0 (vArgs.size - args.size) vArgs;
-  let i₂  := vArgs.size - args.size;
-  isDefEqFOApprox mvar vFn args vArgs 0 i₂
-else
-  /-
-    ?m a_1 ... a_k =?= f b_1 ... b_k
-
-    reduces to
-
-    ?m  =?= f
-    a_1 =?= b_1
-    ...
-    a_k =?= b_k
-  -/
-  isDefEqFOApprox mvar v.getAppFn args vArgs 0 0
+match v with
+| Expr.app f a _ => isExprDefEqAux args.back a <&&> isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
+| _              => pure false
 
 /-
   Auxiliary method for applying first-order unification. It is an approximation.

tests/lean/run/meta2.lean

@@ -587,7 +587,6 @@ withLocalDecl `α type BinderInfo.default $ fun α => do
 #eval tst35
 #check @Id
 
-
 def tst36 : MetaM Unit := do
 print "----- tst36 -----";
 let type := mkSort levelOne;
@@ -599,9 +598,23 @@ withLocalDecl `α type BinderInfo.default $ fun α => do
   check $ approxDefEq $ isDefEq m1 (mkConst `Id [levelZero]);
   pure ()
 
+#eval tst36
+
+def tst37 : MetaM Unit := do
+print "----- tst37 -----";
+m1 ← mkFreshExprMVar (mkArrow nat (mkArrow type type));
+m2 ← mkFreshExprMVar (mkArrow nat type);
+withLocalDecl `v nat BinderInfo.default $ fun v => do
+  let lhs := mkApp2 m1 v (mkApp m2 v);
+  rhs ← mkAppM `StateM #[nat, nat];
+  print lhs;
+  print rhs;
+  check $ approxDefEq $ isDefEq lhs rhs;
+  pure ()
+
 set_option pp.all true
 set_option trace.Meta.isDefEq.step true
 set_option trace.Meta.isDefEq.delta true
 set_option trace.Meta.isDefEq.assign true
 
-#eval tst36
+#eval tst37