# Zulip Chat Archive

## Stream: general

### Topic: Tactic recursive call

#### Bolton Bailey (Nov 03 2021 at 21:38):

I ran into something I don't understand trying to write a tactic that does something roughly similar to `simp * at *`

. Below is my mwe. Why do I get the error `term new_to_simplify_with has type list name but is expected to have type tactic_state`

? Furthermore, why do I get no errors at all when I don't give arguments to `mutually_simplify_aux`

in the last line? What arguments is it being called with when I do this?

```
import data.mv_polynomial.basic
open tactic
namespace tactic
namespace interactive
open interactive interactive.types expr
setup_tactic_parser
/-- For a name nmat in the local context, simplify at it with nmwith,
and if that is successful, simplify again at nmat with integral_domain_simp.
Never fails, but returns tt if the simplification changed something -/
meta def simplify_at_with (nmat nmwith : name) : tactic bool :=
if nmat = nmwith then do return ff else do
nmwith_expr <- get_local nmwith,
used_set <- simp_core {fail_if_unchanged := ff} (failed) tt [simp_arg_type.expr (pexpr.of_expr nmwith_expr)] [] (loc.ns [some nmat]),
return (bnot (name_set.empty used_set))
meta def mutually_simplify_aux (to_simplify_with other : list name) : tactic unit :=
match to_simplify_with with
| [] := skip
| nm_with::to_simplify_withs := do
-- simplify the ones we will simplify with in the future
to_simplify_withs.mmap' (λ a, simplify_at_with a nm_with),
-- Simplify the others, and if they change, remove them from other and add to future
other_success_labels <- other.mmap (λ a, simplify_at_with a nm_with),
let others_changed := list.reduce_option (list.zip_with
(λ nm b, match b with
| tt := (some nm : option name)
| ff := none end)
other other_success_labels),
let others_unchanged := list.reduce_option (list.zip_with
(λ nm b, match b with
| tt := none
| ff := (some nm : option name) end)
other other_success_labels),
let new_to_simplify_with := list.append to_simplify_withs others_changed,
-- mutually_simplify_aux -- This throws no errors
mutually_simplify_aux new_to_simplify_with others_unchanged -- ... expected to have type tactic_state
end
end interactive
end test
```

#### Eric Wieser (Nov 03 2021 at 21:42):

I think it will work fine if you use the pattern matching syntax without `match`

#### Eric Wieser (Nov 03 2021 at 21:43):

When you recurse in lean, the equation compiler only lets you insert the arguments that appear after the colon

#### Bolton Bailey (Nov 03 2021 at 21:53):

Not sure how the normal pattern matching syntax is supposed to work. I try this and I'm told the equation compiler failed

```
import data.mv_polynomial.basic
open tactic
namespace tactic
namespace interactive
open interactive interactive.types expr
setup_tactic_parser
/-- For a name nmat in the local context, simplify at it with nmwith,
and if that is successful, simplify again at nmat with integral_domain_simp.
Never fails, but returns tt if the simplification changed something -/
meta def simplify_at_with (nmat nmwith : name) : tactic bool :=
if nmat = nmwith then do return ff else do
nmwith_expr <- get_local nmwith,
used_set <- simp_core {fail_if_unchanged := ff} (failed) tt [simp_arg_type.expr (pexpr.of_expr nmwith_expr)] [] (loc.ns [some nmat]),
return (bnot (name_set.empty used_set))
def bar : list nat → list nat → nat
| [] [] := 0
| (a :: l) [] := a
| [] (b :: l) := b
| (a :: l) (b :: m) := a + b
meta def mutually_simplify_aux : list name -> list name -> tactic unit
| [] _ := skip
| nm_with::to_simplify_withs other := do
-- simplify the ones we will simplify with in the future
to_simplify_withs.mmap' (λ a, simplify_at_with a nm_with),
-- Simplify the others, and if they change, remove them from other and add to future
other_success_labels <- other.mmap (λ a, simplify_at_with a nm_with),
let others_changed := list.reduce_option (list.zip_with
(λ nm b, match b with
| tt := (some nm : option name)
| ff := none end)
other other_success_labels),
let others_unchanged := list.reduce_option (list.zip_with
(λ nm b, match b with
| tt := none
| ff := (some nm : option name) end)
other other_success_labels),
let new_to_simplify_with := list.append to_simplify_withs others_changed,
-- mutually_simplify_aux -- This throws no errors
mutually_simplify_aux new_to_simplify_with others_unchanged -- ... expected to have type tactic_state
end interactive
end test
```

#### Bolton Bailey (Nov 03 2021 at 21:54):

I guess I was just missing parentheses

#### Eric Wieser (Nov 03 2021 at 22:23):

So it's all working now?

#### Bolton Bailey (Nov 03 2021 at 23:49):

Yep, got it working, thanks for your help!

Last updated: Aug 03 2023 at 10:10 UTC