From bde829bb5b759a21d5fb83b8bd256a27020317d9 Mon Sep 17 00:00:00 2001
From: IndPrinciple <syxx2013050321@163.com>
Date: Thu, 2 May 2024 21:42:04 +0800
Subject: [PATCH] update monomorphic testing

---
 Auto/Lib/ExprExtra.lean                | 40 +++++++++++++++-----------
 Auto/Translation/Monomorphization.lean |  3 +-
 2 files changed, 25 insertions(+), 18 deletions(-)

diff --git a/Auto/Lib/ExprExtra.lean b/Auto/Lib/ExprExtra.lean
index 9d0f7d5..f7dfad8 100644
--- a/Auto/Lib/ExprExtra.lean
+++ b/Auto/Lib/ExprExtra.lean
@@ -214,25 +214,31 @@ def Expr.numLeadingDepArgs : Expr → Nat
     0
 | _ => 0
 
-/-- Turn all `Prop` binders into `True` -/
-private partial def Expr.isMonomorphicFactAux : Expr → MetaM Expr
-| .forallE name ty body bi => do
-  let ty := if (← Meta.isProp ty) ∧ !body.hasLooseBVars then .const ``False [] else ty
-  Meta.withLocalDecl name bi ty fun x => do
-    let body := body.instantiate1 x
-    let body ← isMonomorphicFactAux body
-    Meta.mkForallFVars #[x] body
-| _ => pure (.const ``False [])
-
 /--
-  Test whether `e` is a monomorphic fact.
-  `e` is a monomorphic fact iff for all subterms `t : α` of `e`
-     where `α` is not of type `Prop`, `α` does not depend on bound
-     variables.
+  Check whether the leading `∀` quantifiers of expression `e`
+    violates the quasi-monomorphic condition
 -/
-def Expr.isMonomorphicFact (e : Expr) : MetaM Bool := do
-  let e ← Expr.isMonomorphicFactAux e
-  return (Expr.depArgs e).size == 0
+partial def Expr.leadingForallQuasiMonomorphicAux (fvars : Array FVarId) (e : Expr) : MetaM Bool :=
+  match e with
+  | .forallE name ty body bi => Meta.withLocalDecl name bi ty fun x => do
+    let Expr.fvar xid := x
+      | throwError "Expr.leadingForallQuasiMonomorphic :: Unexpected error"
+    let bodyi := body.instantiate1 x
+    if ← Meta.isProp ty then
+      if !(← Meta.isProp bodyi) then
+        return false
+      if body.hasLooseBVar 0 then
+        return false
+      return (← Expr.leadingForallQuasiMonomorphicAux fvars ty) &&
+             (← Expr.leadingForallQuasiMonomorphicAux (fvars.push xid) bodyi)
+    else
+      let fvarSet := HashSet.empty.insertMany fvars
+      if ty.hasAnyFVar fvarSet.contains then
+        return false
+      Expr.leadingForallQuasiMonomorphicAux (fvars.push xid)  bodyi
+  | _ => return true
+
+def Expr.leadingForallQuasiMonomorphic := Expr.leadingForallQuasiMonomorphicAux #[]
 
 /--
   This should only be used when we're sure that reducing `ty`
diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
index 7d41af4..7321166 100644
--- a/Auto/Translation/Monomorphization.lean
+++ b/Auto/Translation/Monomorphization.lean
@@ -386,7 +386,8 @@ def LemmaInst.matchConstInst (ci : ConstInst) (li : LemmaInst) : MetaM (HashSet
 def LemmaInst.monomorphic? (li : LemmaInst) : MetaM (Option LemmaInst) := do
   if li.params.size != 0 then
     return .none
-  if !(← Expr.isMonomorphicFact li.type) then
+  let li := {li with type := ← prepReduceExpr li.type}
+  if !(← Expr.leadingForallQuasiMonomorphic li.type) then
     return .none
   Meta.withNewMCtxDepth do
     let (_, mvars, mi) ← MLemmaInst.ofLemmaInst li