why `tauto` can't prove this?

Stream: new members

[Asei Inoue]

import Mathlib.Tactic

example (α : Type) (S : α → Prop) : ¬(∀ x, S x) → (∃ x, ¬ S x) := by
  -- `tauto` can't show this
  try tauto

  aesop

[Mark Fischer]

I think the issue is that tauto doesn't decompose functions and ∀ x, S x is a function. So it get's stuck there.

Here you can maybe see a bit more clearly:

example (α : Type) (S : α → Prop) : ¬((x : α) → S x) → (∃ x, ¬ S x) :=
  Classical.not_forall.mp

---

I'm not 100% sure though. If you look at the unsolved goals for tauto, it needs to synthesize a value to give S in order to derive False. Classical.not_forall creates implicit decidable instances and then calls Decidable.not_forall. I don't think tauto is designed to try anything like this.