tactics

Stream: Is there code for X?

[Paige Thomas]

Is there a tactic that does nothing but evaluate the result of a function? Is there also a tactic that does nothing but evaluate a decidable proposition?
Is there a list of all of the tactics somewhere with descriptions of each? I thought there was one, but I can't seem to find it.

[Johan Commelin]

See the discussion here for a list: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean.204.20tactics.20list/near/439268892

[Paige Thomas]

Ahh. Thank you.

[Martin Dvořák]

For your second question, decide is the tactic.
I should probably add it to my list https://github.com/madvorak/lean4-tactics because it pops up quite often.

[Paige Thomas]

Thank you. Do you know what the tactic for the first would be, if the function is one I defined and not just a fun in the proof?

[Paige Thomas]

Ie, should beta_reduce work?

[Mitchell Lee]

What about dsimp?

[Paige Thomas]

Oh. Ok, maybe, yeah. Thank you.

[Aaron Eline]

Let’s say I’m trying to prove a goal like a = g and in my context I have a bunch of types like a = b and b = f and f = g. Obviously I could rewrite each one manually, but I was wondering if there is a tactic that automates the equality chasing

[Ruben Van de Velde]

Try cc

[Aaron Eline]

Where does that tactic live?

[Ruben Van de Velde]

Mathlib.Tactic.CC

[Aaron Eline]

Ah thanks, don't have a dep on Mathlib sadly. Let me see if it can be easily extracted.

[Ruben Van de Velde]

Then probably rw or maybe subst

[Aaron Eline]

Yeah rw works but I have manually chain 4-5 equalities, and I was looking for automation. cc looks perfect and thanks

[Yakov Pechersky]

Also maybe solve_by_elim

[Kyle Miller]

If each equality involves a variable on the LHS or RHS, you can do subst_vars

[Kim Morrison]

solve_by_elim won't help here: it does backwards chaining of apply, but knows nothing about equality.

There's in progress automation work on a new tactic grind that will also solve these problems. But it's not ready yet.