# Zulip Chat Archive

## Stream: general

### Topic: Alternatives to eval_expr

#### Michael Howes (Apr 16 2019 at 12:04):

Hi all, does anyone know of functions that are similar to `eval_expr`

but can handle local variables? I have tried to write a tactic that is similar to ring but commutative semigroups. It uses `eval_expr`

to map expressions representing products in the semigroup into a type I can work with. The tactic is working when asked to prove an equality such as `example : 3*((2*3)*3)=(2*3)*(3*3)`

but not when asked to prove a statement such as `example (n m : ℕ) : n*((m*n)*n) = (m*n)*(n*n)`

. In the second case I get the error `invalid eval_expr, expression must be closed`

.

Here is a minimal working example that gives the same error

import tactic.interactive open tactic example (n : ℕ) : ℕ := begin (do [m] ← local_context, m' ← eval_expr ℕ m, let r := reflect (m' + 2), exact r) end

Is there any other tactic I could replace `eval_expr`

with to make the above construction work?

Thanks!

#### Rob Lewis (Apr 16 2019 at 12:11):

What do you expect the tactic to do here? `eval_expr`

will try to produce a value of type `nat`

, like 0, 1, 2, ... If you just give it a variable `n`

, it can't turn it into a value.

#### Rob Lewis (Apr 16 2019 at 12:12):

In your example, you can work entirely at the `expr`

level, no need to evaluate anything.

example (n : ℕ) : ℕ := begin (do [m] ← local_context, exact `(%%m + 2)) end

#### Rob Lewis (Apr 16 2019 at 12:14):

Does something like this work in your real application?

#### Michael Howes (Apr 16 2019 at 12:27):

I think something like this doesn't work in the application I am trying. This is the function I've defined which used `eval_expr`

:

meta def reflect_expr (α : Type) [reflected α] : expr → tactic (csge α) | `(%%e₁ * %%e₂) := do p₁ ← reflect_expr e₁, p₂ ← reflect_expr e₂, return (comp p₁ p₂) | `(%%e : α) := do a ← eval_expr α e, return (const a)

The type `csge α`

is short for `comm_semigroup_expr α`

which is an inductive type I defined to represent products in the commutative semigroup `α`

. It is defined like so:

inductive csge (α : Type) : Type | const : α → csge | comp : csge → csge → csge

If I replace the above function with:

meta def reflect_expr (α : Type) [reflected α] : expr → tactic (csge α) | `(%%e₁ * %%e₂) := do p₁ ← reflect_expr e₁, p₂ ← reflect_expr e₂, return (comp p₁ p₂) | `(%%e : α) := do return `(const %%e)

I get a type mismatch error. Also for reference I am basing the tactic I'm writing off this blog post https://xenaproject.wordpress.com/2018/06/13/ab3/ about ring

Last updated: Dec 20 2023 at 11:08 UTC