feat: meta code for the category_theory port (#755)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib.lean

@@ -145,6 +145,7 @@ import Mathlib.Lean.Expr.ReplaceRec
 import Mathlib.Lean.Expr.Traverse
 import Mathlib.Lean.LocalContext
 import Mathlib.Lean.Meta
+import Mathlib.Lean.Meta.Simp
 import Mathlib.Logic.Basic
 import Mathlib.Logic.Embedding.Basic
 import Mathlib.Logic.Equiv.Basic

Mathlib/Lean/Meta.lean

@@ -54,6 +54,27 @@ def existsi (mvar : MVarId) (es : List Expr) : MetaM MVarId := do
 
 end Lean.MVarId
 
+namespace Lean.Meta
+
+/--
+Given a monadic function `F` that takes a type and a term of that type and produces a new term,
+lifts this to the monadic function that opens a `∀` telescope, applies `F` to the body,
+and then builds the lambda telescope term for the new term.
+-/
+def mapForallTelescope' (F : Expr → Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
+  forallTelescope (← Meta.inferType forallTerm) fun xs ty => do
+    Meta.mkLambdaFVars xs (← F ty (mkAppN forallTerm xs))
+
+/--
+Given a monadic function `F` that takes a term and produces a new term,
+lifts this to the monadic function that opens a `∀` telescope, applies `F` to the body,
+and then builds the lambda telescope term for the new term.
+-/
+def mapForallTelescope (F : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
+  mapForallTelescope' (fun _ e => F e) forallTerm
+
+end Lean.Meta
+
 namespace Lean.Elab.Tactic
 
 /-- Analogue of `liftMetaTactic` for tactics that do not return any goals. -/

Mathlib/Lean/Meta/Simp.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Lean
+
+/-!
+# Helper functions for using the simplifier.
+-/
+
+open Lean Elab.Tactic
+
+namespace Lean.Meta
+
+/-- Construct a `SimpTheorems` from a list of names. (i.e. as with `simp only`). -/
+def simpTheoremsOfNames (lemmas : List Name) : MetaM SimpTheorems := do
+  lemmas.foldlM (·.addConst ·) (← simpOnlyBuiltins.foldlM (·.addConst ·) {})
+
+/-- Simplify an expression using only a list of lemmas specified by name. -/
+-- TODO We need to write a `mkSimpContext` in `MetaM`
+-- that supports all the bells and whistles in `simp`.
+-- It should generalize this, and another partial implementation in `Tactic.Simps.Basic`.
+def simpOnlyNames (lemmas : List Name) (e : Expr) : MetaM Simp.Result := do
+  (·.1) <$> simp e
+    { simpTheorems := #[← simpTheoremsOfNames lemmas], congrTheorems := ← getSimpCongrTheorems }
+
+/--
+Given a simplifier `S : Expr → MetaM Simp.Result`,
+and an expression `e : Expr`, run `S` on the type of `e`, and then
+convert `e` into that simplified type, using a combination of type hints and `Eq.mp`.
+-/
+def simpType (S : Expr → MetaM Simp.Result) (e : Expr) : MetaM Expr := do
+  match (← S (← inferType e)) with
+  | ⟨ty', none, _⟩ => mkExpectedTypeHint e ty'
+  -- We use `mkExpectedTypeHint` in this branch as well, in order to preserve the binder types.
+  | ⟨ty', some prf, _⟩ => mkExpectedTypeHint (← mkEqMP prf e) ty'
+
+end Lean.Meta