feat: avoid some redundant proof terms in grind (#6615)

This PR adds two auxiliary functions `mkEqTrueCore` and `mkOfEqTrueCore`
that avoid redundant proof terms in proofs produced by `grind`.

src/Init/Grind/Lemmas.lean

@@ -12,6 +12,9 @@ import Init.Grind.Util
 
 namespace Lean.Grind
 
+theorem rfl_true : true = true :=
+  rfl
+
 theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
   fun hp => h (he.mp hp)
 

src/Lean/Meta/AppBuilder.lean

@@ -11,14 +11,14 @@ import Lean.Meta.DecLevel
 
 namespace Lean.Meta
 
-/-- Return `id e` -/
+/-- Returns `id e` -/
 def mkId (e : Expr) : MetaM Expr := do
   let type ← inferType e
   let u    ← getLevel type
   return mkApp2 (mkConst ``id [u]) type e
 
 /--
-  Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, return
+  Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, returns
   term `@id expectedType e`. -/
 def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
   let u ← getLevel expectedType
@@ -38,21 +38,21 @@ def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
   let u2 ← getLevel ety
   return mkAppN (.const ``letFun [u1, u2]) #[α, β, v, f]
 
-/-- Return `a = b`. -/
+/-- Returns `a = b`. -/
 def mkEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getLevel aType
   return mkApp3 (mkConst ``Eq [u]) aType a b
 
-/-- Return `HEq a b`. -/
+/-- Returns `HEq a b`. -/
 def mkHEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
   let bType ← inferType b
   let u ← getLevel aType
   return mkApp4 (mkConst ``HEq [u]) aType a bType b
 
 /--
-  If `a` and `b` have definitionally equal types, return `Eq a b`, otherwise return `HEq a b`.
+  If `a` and `b` have definitionally equal types, returns `Eq a b`, otherwise returns `HEq a b`.
 -/
 def mkEqHEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
@@ -63,25 +63,25 @@ def mkEqHEq (a b : Expr) : MetaM Expr := do
   else
     return mkApp4 (mkConst ``HEq [u]) aType a bType b
 
-/-- Return a proof of `a = a`. -/
+/-- Returns a proof of `a = a`. -/
 def mkEqRefl (a : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getLevel aType
   return mkApp2 (mkConst ``Eq.refl [u]) aType a
 
-/-- Return a proof of `HEq a a`. -/
+/-- Returns a proof of `HEq a a`. -/
 def mkHEqRefl (a : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getLevel aType
   return mkApp2 (mkConst ``HEq.refl [u]) aType a
 
-/-- Given `hp : P` and `nhp : Not P` returns an instance of type `e`. -/
+/-- Given `hp : P` and `nhp : Not P`, returns an instance of type `e`. -/
 def mkAbsurd (e : Expr) (hp hnp : Expr) : MetaM Expr := do
   let p ← inferType hp
   let u ← getLevel e
   return mkApp4 (mkConst ``absurd [u]) p e hp hnp
 
-/-- Given `h : False`, return an instance of type `e`. -/
+/-- Given `h : False`, returns an instance of type `e`. -/
 def mkFalseElim (e : Expr) (h : Expr) : MetaM Expr := do
   let u ← getLevel e
   return mkApp2 (mkConst ``False.elim [u]) e h
@@ -108,7 +108,7 @@ def mkEqSymm (h : Expr) : MetaM Expr := do
       return mkApp4 (mkConst ``Eq.symm [u]) α a b h
     | none => throwAppBuilderException ``Eq.symm ("equality proof expected" ++ hasTypeMsg h hType)
 
-/-- Given `h₁ : a = b` and `h₂ : b = c` returns a proof of `a = c`. -/
+/-- Given `h₁ : a = b` and `h₂ : b = c`, returns a proof of `a = c`. -/
 def mkEqTrans (h₁ h₂ : Expr) : MetaM Expr := do
   if h₁.isAppOf ``Eq.refl then
     return h₂
@@ -185,7 +185,7 @@ def mkHEqOfEq (h : Expr) : MetaM Expr := do
   return mkApp4 (mkConst ``heq_of_eq [u]) α a b h
 
 /--
-If `e` is `@Eq.refl α a`, return `a`.
+If `e` is `@Eq.refl α a`, returns `a`.
 -/
 def isRefl? (e : Expr) : Option Expr := do
   if e.isAppOfArity ``Eq.refl 2 then
@@ -194,7 +194,7 @@ def isRefl? (e : Expr) : Option Expr := do
     none
 
 /--
-If `e` is `@congrArg α β a b f h`, return `α`, `f` and `h`.
+If `e` is `@congrArg α β a b f h`, returns `α`, `f` and `h`.
 Also works if `e` can be turned into such an application (e.g. `congrFun`).
 -/
 def congrArg? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
@@ -336,13 +336,14 @@ private def withAppBuilderTrace [ToMessageData α] [ToMessageData β]
       throw ex
 
 /--
-  Return the application `constName xs`.
+  Returns the application `constName xs`.
   It tries to fill the implicit arguments before the last element in `xs`.
 
   Remark:
   ``mkAppM `arbitrary #[α]`` returns `@arbitrary.{u} α` without synthesizing
   the implicit argument occurring after `α`.
-  Given a `x : ([Decidable p] → Bool) × Nat`, ``mkAppM `Prod.fst #[x]`` returns `@Prod.fst ([Decidable p] → Bool) Nat x`.
+  Given a `x : ([Decidable p] → Bool) × Nat`, ``mkAppM `Prod.fst #[x]``,
+  returns `@Prod.fst ([Decidable p] → Bool) Nat x`.
 -/
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := do
   withAppBuilderTrace constName xs do withNewMCtxDepth do
@@ -465,8 +466,9 @@ def mkPure (monad : Expr) (e : Expr) : MetaM Expr :=
   mkAppOptM ``Pure.pure #[monad, none, none, e]
 
 /--
-  `mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
-  Remark: `fieldName` may be a subfield of `s`. -/
+`mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
+Remark: `fieldName` may be a subfield of `s`.
+-/
 partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
   let type ← inferType s
   let type ← whnf type
@@ -520,75 +522,87 @@ def mkSome (type value : Expr) : MetaM Expr := do
   let u ← getDecLevel type
   return mkApp2 (mkConst ``Option.some [u]) type value
 
-/-- Return `Decidable.decide p` -/
+/-- Returns `Decidable.decide p` -/
 def mkDecide (p : Expr) : MetaM Expr :=
   mkAppOptM ``Decidable.decide #[p, none]
 
-/-- Return a proof for `p : Prop` using `decide p` -/
+/-- Returns a proof for `p : Prop` using `decide p` -/
 def mkDecideProof (p : Expr) : MetaM Expr := do
   let decP      ← mkDecide p
   let decEqTrue ← mkEq decP (mkConst ``Bool.true)
   let h         ← mkEqRefl (mkConst ``Bool.true)
   let h         ← mkExpectedTypeHint h decEqTrue
   mkAppM ``of_decide_eq_true #[h]
 
-/-- Return `a < b` -/
+/-- Returns `a < b` -/
 def mkLt (a b : Expr) : MetaM Expr :=
   mkAppM ``LT.lt #[a, b]
 
-/-- Return `a <= b` -/
+/-- Returns `a <= b` -/
 def mkLe (a b : Expr) : MetaM Expr :=
   mkAppM ``LE.le #[a, b]
 
-/-- Return `Inhabited.default α` -/
+/-- Returns `Inhabited.default α` -/
 def mkDefault (α : Expr) : MetaM Expr :=
   mkAppOptM ``Inhabited.default #[α, none]
 
-/-- Return `@Classical.ofNonempty α _` -/
+/-- Returns `@Classical.ofNonempty α _` -/
 def mkOfNonempty (α : Expr) : MetaM Expr := do
   mkAppOptM ``Classical.ofNonempty #[α, none]
 
-/-- Return `funext h` -/
+/-- Returns `funext h` -/
 def mkFunExt (h : Expr) : MetaM Expr :=
   mkAppM ``funext #[h]
 
-/-- Return `propext h` -/
+/-- Returns `propext h` -/
 def mkPropExt (h : Expr) : MetaM Expr :=
   mkAppM ``propext #[h]
 
-/-- Return `let_congr h₁ h₂` -/
+/-- Returns `let_congr h₁ h₂` -/
 def mkLetCongr (h₁ h₂ : Expr) : MetaM Expr :=
   mkAppM ``let_congr #[h₁, h₂]
 
-/-- Return `let_val_congr b h` -/
+/-- Returns `let_val_congr b h` -/
 def mkLetValCongr (b h : Expr) : MetaM Expr :=
   mkAppM ``let_val_congr #[b, h]
 
-/-- Return `let_body_congr a h` -/
+/-- Returns `let_body_congr a h` -/
 def mkLetBodyCongr (a h : Expr) : MetaM Expr :=
   mkAppM ``let_body_congr #[a, h]
 
-/-- Return `of_eq_true h` -/
+/-- Returns `@of_eq_true p h` -/
+def mkOfEqTrueCore (p : Expr) (h : Expr) : Expr :=
+  match_expr h with
+  | eq_true _ h => h
+  | _ => mkApp2 (mkConst ``of_eq_true) p h
+
+/-- Returns `of_eq_true h` -/
 def mkOfEqTrue (h : Expr) : MetaM Expr := do
   match_expr h with
   | eq_true _ h => return h
   | _ => mkAppM ``of_eq_true #[h]
 
-/-- Return `eq_true h` -/
+/-- Returns `eq_true h` -/
+def mkEqTrueCore (p : Expr) (h : Expr) : Expr :=
+  match_expr h with
+  | of_eq_true _ h => h
+  | _ => mkApp2 (mkConst ``eq_true) p h
+
+/-- Returns `eq_true h` -/
 def mkEqTrue (h : Expr) : MetaM Expr := do
   match_expr h with
   | of_eq_true _ h => return h
   | _ => return mkApp2 (mkConst ``eq_true) (← inferType h) h
 
 /--
-  Return `eq_false h`
+  Returns `eq_false h`
   `h` must have type definitionally equal to `¬ p` in the current
   reducibility setting. -/
 def mkEqFalse (h : Expr) : MetaM Expr :=
   mkAppM ``eq_false #[h]
 
 /--
-  Return `eq_false' h`
+  Returns `eq_false' h`
   `h` must have type definitionally equal to `p → False` in the current
   reducibility setting. -/
 def mkEqFalse' (h : Expr) : MetaM Expr :=
@@ -606,7 +620,7 @@ def mkImpDepCongrCtx (h₁ h₂ : Expr) : MetaM Expr :=
 def mkForallCongr (h : Expr) : MetaM Expr :=
   mkAppM ``forall_congr #[h]
 
-/-- Return instance for `[Monad m]` if there is one -/
+/-- Returns instance for `[Monad m]` if there is one -/
 def isMonad? (m : Expr) : MetaM (Option Expr) :=
   try
     let monadType ← mkAppM `Monad #[m]
@@ -617,52 +631,52 @@ def isMonad? (m : Expr) : MetaM (Option Expr) :=
   catch _ =>
     pure none
 
-/-- Return `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n` -/
+/-- Returns `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n` -/
 def mkNumeral (type : Expr) (n : Nat) : MetaM Expr := do
   let u ← getDecLevel type
   let inst ← synthInstance (mkApp2 (mkConst ``OfNat [u]) type (mkRawNatLit n))
   return mkApp3 (mkConst ``OfNat.ofNat [u]) type (mkRawNatLit n) inst
 
 /--
-  Return `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.
-  This method assumes `a` and `b` have the same type, and typeclass `className` is heterogeneous.
-  Examples of supported classes: `HAdd`, `HSub`, `HMul`.
-  We use heterogeneous operators to ensure we have a uniform representation.
-  -/
+Returns `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.
+This method assumes `a` and `b` have the same type, and typeclass `className` is heterogeneous.
+Examples of supported classes: `HAdd`, `HSub`, `HMul`.
+We use heterogeneous operators to ensure we have a uniform representation.
+-/
 private def mkBinaryOp (className : Name) (opName : Name) (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getDecLevel aType
   let inst ← synthInstance (mkApp3 (mkConst className [u, u, u]) aType aType aType)
   return mkApp6 (mkConst opName [u, u, u]) aType aType aType inst a b
 
-/-- Return `a + b` using a heterogeneous `+`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a + b` using a heterogeneous `+`. This method assumes `a` and `b` have the same type. -/
 def mkAdd (a b : Expr) : MetaM Expr := mkBinaryOp ``HAdd ``HAdd.hAdd a b
 
-/-- Return `a - b` using a heterogeneous `-`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a - b` using a heterogeneous `-`. This method assumes `a` and `b` have the same type. -/
 def mkSub (a b : Expr) : MetaM Expr := mkBinaryOp ``HSub ``HSub.hSub a b
 
-/-- Return `a * b` using a heterogeneous `*`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a * b` using a heterogeneous `*`. This method assumes `a` and `b` have the same type. -/
 def mkMul (a b : Expr) : MetaM Expr := mkBinaryOp ``HMul ``HMul.hMul a b
 
 /--
-  Return `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
-  This method assumes `a` and `b` have the same type.
-  Examples of supported classes: `LE` and `LT`.
-  We use heterogeneous operators to ensure we have a uniform representation.
-  -/
+Returns `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
+This method assumes `a` and `b` have the same type.
+Examples of supported classes: `LE` and `LT`.
+We use heterogeneous operators to ensure we have a uniform representation.
+-/
 private def mkBinaryRel (className : Name) (rName : Name) (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
   let u ← getDecLevel aType
   let inst ← synthInstance (mkApp (mkConst className [u]) aType)
   return mkApp4 (mkConst rName [u]) aType inst a b
 
-/-- Return `a ≤ b`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a ≤ b`. This method assumes `a` and `b` have the same type. -/
 def mkLE (a b : Expr) : MetaM Expr := mkBinaryRel ``LE ``LE.le a b
 
-/-- Return `a < b`. This method assumes `a` and `b` have the same type. -/
+/-- Returns `a < b`. This method assumes `a` and `b` have the same type. -/
 def mkLT (a b : Expr) : MetaM Expr := mkBinaryRel ``LT ``LT.lt a b
 
-/-- Given `h : a = b`, return a proof for `a ↔ b`. -/
+/-- Given `h : a = b`, returns a proof for `a ↔ b`. -/
 def mkIffOfEq (h : Expr) : MetaM Expr := do
   if h.isAppOfArity ``propext 3 then
     return h.appArg!

src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Offset
+import Init.Grind.Lemmas
 import Lean.Meta.Tactic.Grind.Types
 
 namespace Lean.Meta.Grind.Arith
@@ -15,8 +16,8 @@ Helper functions for constructing proof terms in the arithmetic procedures.
 
 namespace Offset
 
-/-- `Eq.refl true` -/
-def rfl_true : Expr := mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
+/-- Returns a proof for `true = true` -/
+def rfl_true : Expr := mkConst ``Grind.rfl_true
 
 open Lean.Grind in
 /--

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

@@ -24,7 +24,7 @@ def propagateForallPropUp (e : Expr) : GoalM Unit := do
     unless (← isEqTrue p) do return
     trace_goal[grind.debug.forallPropagator] "isEqTrue, {e}"
     let h₁ ← mkEqTrueProof p
-    let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
+    let qh₁ := q.instantiate1 (mkOfEqTrueCore p h₁)
     let r ← simp qh₁
     let q := mkLambda n bi p q
     let q' := r.expr
@@ -65,7 +65,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   else
     let idx ← modifyGet fun s => (s.nextThmIdx, { s with nextThmIdx := s.nextThmIdx + 1 })
     pure <| .local ((`local).appendIndexAfter idx)
-  let proof := mkApp2 (mkConst ``of_eq_true) e proof
+  let proof := mkOfEqTrueCore e proof
   let size := (← get).newThms.size
   let gen ← getGeneration e
   -- TODO: we should have a flag for collecting all unary patterns in a local theorem