Alternatives to eval_expr

Stream: general

[Michael Howes]

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]

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]

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]

Does something like this work in your real application?

[Michael Howes]

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