From 878ef3a281ba3d62d398f8350fca0901695dc1cd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Jun 2022 15:24:36 -0700
Subject: [PATCH] feat: improve `acyclic` tactic

closes #1182
---
 src/Lean/Meta/Tactic/Acyclic.lean |  2 +-
 tests/lean/run/1182.lean          | 34 +++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/1182.lean

diff --git a/src/Lean/Meta/Tactic/Acyclic.lean b/src/Lean/Meta/Tactic/Acyclic.lean
index 7acaa06ecb..57145ea564 100644
--- a/src/Lean/Meta/Tactic/Acyclic.lean
+++ b/src/Lean/Meta/Tactic/Acyclic.lean
@@ -12,7 +12,7 @@ private def isTarget (lhs rhs : Expr) : MetaM Bool := do
   if !lhs.isFVar || !lhs.occurs rhs then
     return false
   else
-    return rhs.isConstructorApp (← getEnv)
+    return (← whnf rhs).isConstructorApp (← getEnv)
 
 /--
   Close the given goal if `h` is a proof for an equality such as `as = a :: as`.
diff --git a/tests/lean/run/1182.lean b/tests/lean/run/1182.lean
new file mode 100644
index 0000000000..bf91d9167b
--- /dev/null
+++ b/tests/lean/run/1182.lean
@@ -0,0 +1,34 @@
+example: ¬ n + 1 = n := λ h => nomatch h
+
+
+inductive Term (L: Nat → Type) (n : Nat) : Nat → Type _
+| var  (k: Fin n)                           : Term L n 0
+| func (f: L l)                             : Term L n l
+| app  (t: Term L n (l + 1)) (s: Term L n 0): Term L n l
+
+namespace Term
+
+inductive SubTermOf: Term L n l₁ → Term L n l₂ → Prop
+| refl: SubTermOf t t
+| appL: SubTermOf t s₁ → SubTermOf t (app s₁ s₂)
+| appR: SubTermOf t s₂ → SubTermOf t (app s₁ s₂)
+
+theorem app_SubTermOf {t₁: Term L n (l+1)}
+  (h: (app t₁ t₂).SubTermOf t₃):
+  t₁.SubTermOf t₃ ∧ t₂.SubTermOf t₃ := by
+  match h with
+  | .appR h => have := app_SubTermOf h; exact ⟨.appR this.1, .appR this.2⟩
+  | .appL h => have := app_SubTermOf h; exact ⟨.appL this.1, .appL this.2⟩
+  | .refl => exact ⟨.appL .refl, .appR .refl⟩
+
+mutual
+  theorem not_app_SubTermOf_left (t: Term L n (l+1)) : ¬ (app t s).SubTermOf t :=
+    fun
+    | .appR h => have := app_SubTermOf h; not_app_SubTermOf_right _ this.1
+    | .appL h => have := app_SubTermOf h; not_app_SubTermOf_left  _ this.1
+
+  theorem not_app_SubTermOf_right (s: Term L n 0) : ¬ (app t s).SubTermOf s :=
+    fun
+    | .appR h => have := app_SubTermOf h; not_app_SubTermOf_right _ this.2
+    | .appL h => have := app_SubTermOf h; not_app_SubTermOf_left  _ this.2
+end