proof automatisation

Stream: general

[Thorsten Altenkirch]

What tools are there to automatically derive proofs in predicate logic? After I say induction the rest is laborious but straightforward.

[Mario Carneiro]

This is a weak point. We have cc and finish that can do some simple FOL= reasoning, but nothing like a complete SMT solver

[Mario Carneiro]

tidy can also do a lot of obvious FOL reasoning

[Thorsten Altenkirch]

Where can I find out about the tactics you just mentioned?

[Henrik Böving]

Here is a list https://leanprover-community.github.io/mathlib_docs/tactics.html

[Mario Carneiro]

tactic#cc tactic#finish tactic#tidy