tauto failure

Stream: new members

[Eric Paul]

Should tauto be able to solve this goal?

import Mathlib

example (x y : ℕ) (P Q : ℕ → Prop) :
    (∃n, P n ∧ Q n) ∨ x = y → (∃n, P n ∧ Q n) ∨ x = y := by
  tauto --fails

I ran into this issue when I had a slightly less trivial goal like the following that could not be solved by tauto

import Mathlib

example (x y : ℕ) (P Q J : ℕ → Prop) :
    (∃n, P n ∧ Q n ∧ J n) ∨ x = y → (∃n, P n ∧ J n ∧ Q n) ∨ y = x := by
  -- `tauto` fails
  simp [And.comm, eq_comm]

Thankfully, for these examples there are many other simple ways to solve the goals so it's not really an issue but I'm still curious as to whether tauto should be able to solve them and if not, why.

(grind solves them both!)

[Robin Arnez]

Oh wow, I would've thought it could solve these, I mean the solution is literally exact id amd turns out itauto can solve the first one. grind is definitely a cool tactic that I'm very excited about and it is getting better as we speak! If you wanna know what kind of stuff grind is for, there is a "guide" in the test files.

[Luigi Massacci]

I think the problem with tauto (and why itauto works instead) is that it destructs the existential in the hypothesis at some point

[Luigi Massacci]

this might be a situation where tauto not sticking to just purely propositional logic and trying to close first order goals comes back to bite it in the ass