fix(tactic/squeeze): squeeze_simp providing invalid suggestions (#1…

…1696)

`squeeze_simp` was previously permuting the lemmas passed to `simp`, which caused failures in cases where the lemma order mattered. The fix is to ensure that `squeeze_simp` does not change the order of passed lemmas.

Closes #3097

src/meta/expr.lean

@@ -541,10 +541,15 @@ meta def list_local_const_unique_names (e : expr) : name_set :=
 e.fold mk_name_set
   (λ e' _ es, if e'.is_local_constant then es.insert e'.local_uniq_name else es)
 
-/-- Returns a name_set of all constants in an expression. -/
+/-- Returns a `name_set` of all constants in an expression. -/
 meta def list_constant (e : expr) : name_set :=
 e.fold mk_name_set (λ e' _ es, if e'.is_constant then es.insert e'.const_name else es)
 
+/-- Returns a `list name` containing the constant names of an `expr` in the same order
+  that `expr.fold` traverses it. -/
+meta def list_constant' (e : expr) : list name :=
+(e.fold [] (λ e' _ es, if e'.is_constant then es.insert e'.const_name else es)).reverse
+
 /-- Returns a list of all meta-variables in an expression (without duplicates). -/
 meta def list_meta_vars (e : expr) : list expr :=
 e.fold [] (λ e' _ es, if e'.is_mvar then insert e' es else es)
@@ -571,7 +576,7 @@ meta def contains_expr_or_mvar (t : expr) (e : expr) : bool :=
 -- We can't use `t.has_meta_var` here, as that detects universe metavariables, too.
 ¬ t.list_meta_vars.empty ∨ e.occurs t
 
-/-- Returns a name_set of all constants in an expression starting with a certain prefix. -/
+/-- Returns a `name_set` of all constants in an expression starting with a certain prefix. -/
 meta def list_names_with_prefix (pre : name) (e : expr) : name_set :=
 e.fold mk_name_set $ λ e' _ l,
   match e' with

src/tactic/squeeze.lean

@@ -117,17 +117,21 @@ meta def same_result (pr : proof_state) (tac : tactic unit) : tactic bool :=
 do s ← get_proof_state_after tac,
    pure $ some pr = s
 
+/--
+Consumes the first list of `simp` arguments, accumulating required arguments
+on the second one and unnecessary arguments on the third one.
+-/
 private meta def filter_simp_set_aux
   (tac : bool → list simp_arg_type → tactic unit)
   (args : list simp_arg_type) (pr : proof_state) :
   list simp_arg_type → list simp_arg_type →
   list simp_arg_type → tactic (list simp_arg_type × list simp_arg_type)
-| [] ys ds := pure (ys.reverse, ds.reverse)
+| [] ys ds := pure (ys, ds)
 | (x :: xs) ys ds :=
   do b ← same_result pr (tac tt (args ++ xs ++ ys)),
      if b
-       then filter_simp_set_aux xs ys (x:: ds)
-       else filter_simp_set_aux xs (x :: ys) ds
+       then filter_simp_set_aux xs ys (ds.concat x)
+       else filter_simp_set_aux xs (ys.concat x) ds
 
 declare_trace squeeze.deleted
 
@@ -159,7 +163,6 @@ argument list.
  * `no_dflt`: did the user use the `only` keyword?
  * `args`:    list of `simp` arguments
  * `tac`:     how to invoke the underlying `simp` tactic
-
 -/
 meta def squeeze_simp_core
   (slow no_dflt : bool) (args : list simp_arg_type)
@@ -176,10 +179,10 @@ do v ← target >>= mk_meta_var,
    { g ← main_goal,
      tac no_dflt args,
      instantiate_mvars g },
-   let vs := g.list_constant,
+   let vs := g.list_constant',
    vs ← vs.mfilter is_simp_lemma,
    vs ← vs.mmap strip_prefix,
-   vs ← vs.to_list.mmap name.to_simp_args,
+   vs ← vs.mmap name.to_simp_args,
    with_local_goals' [v] (filter_simp_set tac args vs)
      >>= mk_suggestion,
    tac no_dflt args

test/squeeze.lean

@@ -32,3 +32,13 @@ 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] }
+
+-- 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] }
+