fix(tactic/squeeze_simp): "match failed" when simp works (#11659)

Closes #11196.

Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com>



Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com>
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/tactic/squeeze.lean

@@ -25,6 +25,17 @@ meta def pos.move_left (p : pos) (n : ℕ) : pos :=
 
 namespace tactic
 
+attribute [derive decidable_eq] simp_arg_type
+
+/-- Turn a `simp_arg_type` into a string. -/
+meta instance simp_arg_type.has_to_string : has_to_string simp_arg_type :=
+⟨λ a, match a with
+| simp_arg_type.all_hyps := "*"
+| (simp_arg_type.except n) := "-" ++ to_string n
+| (simp_arg_type.expr e) := to_string e
+| (simp_arg_type.symm_expr e) := "←" ++ to_string e
+end⟩
+
 open list
 
 /-- parse structure instance of the shape `{ field1 := value1, .. , field2 := value2 }` -/
@@ -66,10 +77,13 @@ def squeeze_loc_attr_carrier := ()
 run_cmd squeeze_loc_attr.set ``squeeze_loc_attr_carrier none tt
 
 /-- Format a list of arguments for use with `simp` and friends. This omits the
-list entirely if it is empty. -/
-meta def render_simp_arg_list : list simp_arg_type → tactic format
-| [] := pure ""
-| args := (++) " " <$> to_line_wrap_format <$> args.mmap pp
+list entirely if it is empty.
+
+Patch: `pp` was changed to `to_string` because it was getting rid of prefixes
+that would be necessary for some disambiguations. -/
+meta def render_simp_arg_list : list simp_arg_type → format
+| [] := ""
+| args := (++) " " $ to_line_wrap_format $ args.map to_string
 
 /-- Emit a suggestion to the user. If inside a `squeeze_scope` block,
 the suggestions emitted through `mk_suggestion` will be aggregated so that
@@ -81,7 +95,7 @@ meta def mk_suggestion (p : pos) (pre post : string) (args : list simp_arg_type)
 do xs ← squeeze_loc_attr.get_param ``squeeze_loc_attr_carrier,
    match xs with
    | none := do
-     args ← render_simp_arg_list args,
+     let args := render_simp_arg_list args,
      if at_pos then
        @scope_trace _ p.line p.column $
          λ _, _root_.trace sformat!"{pre}{args}{post}" (pure () : tactic unit)
@@ -91,8 +105,6 @@ do xs ← squeeze_loc_attr.get_param ``squeeze_loc_attr_carrier,
      squeeze_loc_attr.set ``squeeze_loc_attr_carrier ((p,pre,args,post) :: xs) ff
    end
 
-local postfix `?`:9001 := optional
-
 /-- translate a `pexpr` into a `simp` configuration -/
 meta def parse_config : option pexpr → tactic (simp_config_ext × format)
 | none := pure ({}, "")
@@ -152,8 +164,17 @@ do some s ← get_proof_state_after (tac ff (user_args ++ simp_args)),
    pure (user_args' ++ simp_args')
 
 /-- make a `simp_arg_type` that references the name given as an argument -/
-meta def name.to_simp_args (n : name) : tactic simp_arg_type :=
-do e ← resolve_name' n, pure $ simp_arg_type.expr e
+meta def name.to_simp_args (n : name) : simp_arg_type :=
+simp_arg_type.expr $ @expr.local_const ff n n (default) pexpr.mk_placeholder
+
+/-- If the `name` is (likely) to be overloaded, then prepend a `_root_` on it. The `expr` of an
+overloaded name is constructed using `expr.macro`; this is how we guess whether it's overloaded. -/
+meta def prepend_root_if_needed (n : name) : tactic name :=
+do x ← resolve_name' n,
+return $ match x with
+| expr.macro _ _ := `_root_ ++ n
+| _ := n
+end
 
 /-- tactic combinator to create a `simp`-like tactic that minimizes its
 argument list.
@@ -182,24 +203,13 @@ do v ← target >>= mk_meta_var,
    let vs := g.list_constant',
    vs ← vs.mfilter is_simp_lemma,
    vs ← vs.mmap strip_prefix,
-   vs ← vs.mmap name.to_simp_args,
-   with_local_goals' [v] (filter_simp_set tac args vs)
+   vs ← vs.mmap prepend_root_if_needed,
+   with_local_goals' [v] (filter_simp_set tac args $ vs.map name.to_simp_args)
      >>= mk_suggestion,
    tac no_dflt args
 
 namespace interactive
 
-attribute [derive decidable_eq] simp_arg_type
-
-/-- Turn a `simp_arg_type` into a string. -/
-meta instance simp_arg_type.has_to_string : has_to_string simp_arg_type :=
-⟨λ a, match a with
-| simp_arg_type.all_hyps := "*"
-| (simp_arg_type.except n) := "-" ++ to_string n
-| (simp_arg_type.expr e) := to_string e
-| (simp_arg_type.symm_expr e) := "←" ++ to_string e
-end⟩
-
 /-- combinator meant to aggregate the suggestions issued by multiple calls
 of `squeeze_simp` (due, for instance, to `;`).
 

test/squeeze.lean

@@ -1,6 +1,6 @@
 import data.nat.basic
+import data.pnat.basic
 import tactic.squeeze
-import data.list.perm
 
 namespace tactic
 namespace interactive
@@ -17,7 +17,7 @@ meta def squeeze_simp_test
 do (cfg',c) ← parse_config cfg,
    squeeze_simp_core slow_and_accurate.is_some no_dflt hs
      (λ l_no_dft l_args, simp use_iota_eqn none l_no_dft l_args attr_names locat cfg')
-     (λ args, guard ((args.map to_string).perm (l.map to_string)) <|> fail!"{args} expected.")
+     (λ a, guard (a.map to_string = l.map to_string) <|> fail!"{a.map to_string} expected.")
 end interactive
 end tactic
 
@@ -31,14 +31,40 @@ by { squeeze_simp_test [←h, two_mul] = [←h, two_mul, add_zero] }
 
 -- Test that the order of the given hypotheses do not matter.
 example {a b : ℕ} (h : a + a = b) : b + 0 = 2 * a :=
-by { squeeze_simp_test [←h, two_mul] = [←h, add_zero, two_mul] }
+by { squeeze_simp_test [←h, two_mul] = [←h, two_mul, add_zero] }
+
+section namespacing1
+
+@[simp] lemma asda {a : ℕ} : 0 ≤ a := nat.zero_le _
+
+@[simp] lemma pnat.asda {a : ℕ+} : 1 ≤ a := pnat.one_le _
+
+open pnat
+
+-- Test that adding two clashing decls to a namespace doesn't break `squeeze_simp`.
+example {a : ℕ} {b : ℕ+} : 0 ≤ a ∧ 1 ≤ b :=
+by { squeeze_simp_test = [_root_.asda, pnat.asda, and_self] }
+
+end namespacing1
+
+section namespacing2
+
+open nat
+
+local attribute [simp] nat.mul_succ
+
+-- Test that we strip superflous prefixes from `squeeze_simp` output, if needed.
+example (n m : ℕ) : n * m.succ = n*m + n :=
+by { squeeze_simp_test = [mul_succ] }
+
+end namespacing2
 
--- Test fix for #3097
 def a := 0
 def b := 0
 def c := 0
 def f : ℕ → ℕ := default
 @[simp] lemma k (x) : f x = b := rfl
 @[simp] lemma l : f b = c := rfl
-example : f (f a) = c := by { squeeze_simp_test = [k, l] }
 
+-- Test the fix for #3097
+example : f (f a) = c := by { squeeze_simp_test = [k, l] }