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?
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
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)
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: Aug 03 2023 at 10:10 UTC