feat(tactic/interactive.lean): clear_aux_decl

docs/tactics.md

@@ -753,3 +753,28 @@ by use [1, 2, 3]
 example : ∃ p : ℤ × ℤ, p.1 = 1 :=
 by use ⟨1, 42⟩
 ```
+
+### clear_aux_decl
+
+`clear_aux_decl` clears every `aux_decl` in the local context for the current goal.
+This includes the induction hypothesis when using the equation compiler and
+`_let_match` and `_fun_match`.
+
+It is useful when using a tactic such as `finish`, `simp *` or `subst` that may use these
+auxiliary declarations, and produce an error saying the recursion is not well founded.
+
+```lean
+example (n m : ℕ) (h₁ : n = m) (h₂ : ∃ a : ℕ, a = n ∧ a = m) : 2 * m = 2 * n :=
+let ⟨a, ha⟩ := h₂ in
+begin
+  clear_aux_decl, -- subst will fail without this line
+  subst h₁
+end
+
+example (x y : ℕ) (h₁ : ∃ n : ℕ, n * 1 = 2) (h₂ : 1 + 1 = 2 → x * 1 = y) : x = y :=
+let ⟨n, hn⟩ := h₁ in
+begin
+  clear_aux_decl, -- finish produces an error without this line
+  finish
+end
+```

src/tactic/basic.lean

@@ -842,4 +842,11 @@ private meta def tactic.use_aux (h : pexpr) : tactic unit :=
 meta def tactic.use (l : list pexpr) : tactic unit :=
 focus1 $ l.mmap' $ λ h, tactic.use_aux h <|> fail format!"failed to instantiate goal with {h}"
 
+meta def clear_aux_decl_aux : list expr → tactic unit
+| []     := skip
+| (e::l) := do cond e.is_aux_decl (tactic.clear e) skip, clear_aux_decl_aux l
+
+meta def clear_aux_decl : tactic unit :=
+local_context >>= clear_aux_decl_aux
+
 end tactic

src/tactic/interactive.lean

@@ -643,5 +643,16 @@ by use [100, tt, 4, 3]
 meta def use (l : parse pexpr_list_or_texpr) : tactic unit :=
 tactic.use l >> try triv
 
+/--
+`clear_aux_decl` clears every `aux_decl` in the local context for the current goal.
+This includes the induction hypothesis when using the equation compiler and
+`_let_match` and `_fun_match`.
+
+It is useful when using a tactic such as `finish`, `simp *` or `subst` that may use these
+auxiliary declarations, and produce an error saying the recursion is not well founded.
+-/
+
+meta def clear_aux_decl : tactic unit := tactic.clear_aux_decl
+
 end interactive
 end tactic

tests/tactics.lean

@@ -706,6 +706,24 @@ end
 
 end conv
 
+section clear_aux_decl
+
+example (n m : ℕ) (h₁ : n = m) (h₂ : ∃ a : ℕ, a = n ∧ a = m) : 2 * m = 2 * n :=
+let ⟨a, ha⟩ := h₂ in
+begin
+  clear_aux_decl, -- subst will fail without this line
+  subst h₁
+end
+
+example (x y : ℕ) (h₁ : ∃ n : ℕ, n * 1 = 2) (h₂ : 1 + 1 = 2 → x * 1 = y) : x = y :=
+let ⟨n, hn⟩ := h₁ in
+begin
+  clear_aux_decl, -- finish produces an error without this line
+  finish
+end
+
+end clear_aux_decl
+
 private meta def get_exception_message (t : lean.parser unit) : lean.parser string
 | s := match t s with
        | result.success a s' := result.success "No exception" s