feat: add option in LnSymSimpContext to add arbitrary expressions t…

…o the simpset (#177)

### Description:

This allows us to `simp` with expressions that aren't just fvars or
constants.

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine? yes

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

Co-authored-by: Shilpi Goel <[email protected]>

Tactics/Simp.lean

@@ -48,6 +48,8 @@ def LNSymSimpContext
   (thms : Array Name := #[])
   -- Local hypotheses to use during simp.
   (decls : Array LocalDecl := #[])
+  -- Other expressions to use during simp
+  (exprs : Array Expr := #[])
   -- Simprocs to add to the default set.
   (simprocs : Array Name := #[])
   -- argument to `DiscrTree.mkPath`
@@ -70,13 +72,19 @@ def LNSymSimpContext
     const_simpTheorems ← const_simpTheorems.addDeclToUnfold d
   for t in thms do
     const_simpTheorems ← const_simpTheorems.addConst t
-  for l in decls do
-    let proof := l.toExpr
-    let fvar := l.fvarId
-    let mut newThms ← mkSimpTheorems (.fvar fvar) #[] proof
+
+  let exprs := exprs ++ (decls.map fun d => Expr.fvar d.fvarId)
+  for e in exprs do
+    let origin :=
+      if let Expr.fvar id := e then
+        .fvar id
+      else
+        .other (← mkFreshUserName `sym_n)
+    let mut newThms ← mkSimpTheorems origin #[] e
     if noIndexAtArgs = false then
       newThms ← newThms.mapM fixSimpTheoremKey
     const_simpTheorems := newThms.foldl addSimpTheoremEntry const_simpTheorems
+
   let all_simpTheorems := (#[const_simpTheorems] ++ ext_simpTheorems)
   let (ctx : Simp.Context) := { config := config,
                                 simpTheorems := all_simpTheorems,