## 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