goal is ```true```

Stream: new members

[Damiano Testa]

What is the "correct" way of concluding a proof whose goal is true? I have been using trivial, but I wonder whether some other tactic is more appropriate!

Thank you!

[Kevin Buzzard]

trivial is a fine tactic. Why do you end up with goals like true?

[Damiano Testa]

Using squeeze_simp, replacing simp only by rw and messing around... Ahaha

[Eric Wieser]

Possibly due to lemmas of the form x ↔ truethat maybe should just be spelt x (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60p.20x.60.20or.20.60p.20x.20.20.E2.86.94.20true.60.20in.20simp.20lemmas.3F/near/212064947)

[Kevin Buzzard]

"I'm experimenting" is a fine answer.

[Mario Carneiro]

Some interesting alternatives include constructor, split (!) and exact ⟨⟩

[Anatole Dedecker]

Or exact true.intro. But that one is boring :)

[Mario Carneiro]

or exact trivial, since trivial is both the name of the proof of true and also the name of a tactic that applies it

[Damiano Testa]

Thanks! I think that also various of the simps tactics work! Is there a reason to prefer one tactic over another one? I would like to make it as easy as possible for Lean to parse the files: which one of these tactics would be the "fastest"?

[Reid Barton]

the ones that aren't simp

[Mario Carneiro]

exact trivial is the fastest, I think, but trivial is fine. But really this is a micro optimization, there are generally much bigger fish to fry when it comes to speeding up proofs

[Mario Carneiro]

generally speaking, the less you make lean guess what you mean the faster the tactic will be

[Mario Carneiro]

so something like simp is slow because it uses a big database of true things, one of which is the one you want

[Mario Carneiro]

and the others do some minor figuring out of which inductive type to construct

[Damiano Testa]

Ok, thank you! I realize that this is not the bottleneck for speed, but this is a concrete where I can easily formulate a question about optimization and I am glad for the answer!

[Reid Barton]

while we're listing tactics that can solve true, cc is presumably the shortest one

[Mario Carneiro]

if you are in term mode you can't beat ⟨⟩