Meta program that traverses product expressions fails

kendroe commented 6 years ago

Prerequisites

[ ] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
  - Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.

Description

A simple meta program to simplify a product expression fails. The program generates no errors.

Steps to Reproduce

Try the following program:

meta def simplifyProd : expr → expr | (expr.app (expr.app (expr.app (prod.fst) tt1a) tt1b) (expr.app (expr.app (expr.app (expr.app(prod.mk) tt1) tt2) a) b)) := a | (expr.app a b) := expr.app (simplifyProd a) (simplifyProd b) | (expr.lam v b t e) := expr.lam v b (simplifyProd t) (simplifyProd e) | (expr.pi v b t e) := expr.pi v b (simplifyProd t) (simplifyProd e) | x := x

theorem testit (f:ℕ) (s:ℕ) : (f,s).fst=f := begin do { t ← target, trace "Start", trace t.to_raw_fmt, tq ← some (simplifyProd t), trace tq.to_raw_fmt, change tq }, refl end

Expected behavior: [What you expect to happen]

tq should have the expression "f=f"

Actual behavior: [What actually happens]

tq gets the expression (f,s).fs=f

Reproduces how often: [What percentage of the time does it reproduce?]

always

Versions

Lean 3.4.1

Additional Information

cipher1024 commented 6 years ago

Using dsimp should get rid of those projections for you.

avigad commented 6 years ago

@kendroe The right place for questions like is Zulip, https://leanprover.zulipchat.com/.

There are various bugs in your code:

you need to quote the constants prod.fst and prod.mk
you don't want to use some (it dropped you into the option monad)
the parentheses in your first case were associated the wrong way.

The modification below works.

open tactic

meta def simplifyProd : expr → expr
| `(prod.fst (prod.mk %%a %%b)) := a
| (expr.app a b) := expr.app (simplifyProd a) (simplifyProd b)
| (expr.lam v b t e) := expr.lam v b (simplifyProd t) (simplifyProd e)
| (expr.pi v b t e) := expr.pi v b (simplifyProd t) (simplifyProd e)
| x := x

theorem testit (f:ℕ) (s:ℕ) :
(f,s).fst=f :=
begin
do {
t ← target,
trace "Start",
trace t,
let tq := (simplifyProd t),
trace tq,
change tq
},
refl
end

leodemoura commented 6 years ago

@avigad @cipher1024 Thanks.

Since this is not a bug, I am closing this issue.

leanprover / lean3