feat: improve acyclic tactic

closes #1182

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`.

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