Tactic recursive call

Stream: general

[Bolton Bailey]

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]

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

[Eric Wieser]

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

[Bolton Bailey]

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]

I guess I was just missing parentheses

[Eric Wieser]

So it's all working now?

[Bolton Bailey]

Yep, got it working, thanks for your help!