Zulip Chat Archive

Stream: new members

Topic: goal is ```true```


view this post on Zulip Damiano Testa (Oct 02 2020 at 12:12):

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!

view this post on Zulip Kevin Buzzard (Oct 02 2020 at 12:13):

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

view this post on Zulip Damiano Testa (Oct 02 2020 at 12:15):

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

view this post on Zulip Eric Wieser (Oct 02 2020 at 12:18):

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)

view this post on Zulip Kevin Buzzard (Oct 02 2020 at 12:48):

"I'm experimenting" is a fine answer.

view this post on Zulip Mario Carneiro (Oct 02 2020 at 15:01):

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

view this post on Zulip Anatole Dedecker (Oct 02 2020 at 15:04):

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

view this post on Zulip Mario Carneiro (Oct 02 2020 at 15:07):

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

view this post on Zulip Damiano Testa (Oct 02 2020 at 15:09):

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"?

view this post on Zulip Reid Barton (Oct 02 2020 at 15:11):

the ones that aren't simp

view this post on Zulip Mario Carneiro (Oct 02 2020 at 15:11):

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

view this post on Zulip Mario Carneiro (Oct 02 2020 at 15:12):

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

view this post on Zulip Mario Carneiro (Oct 02 2020 at 15:13):

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

view this post on Zulip Mario Carneiro (Oct 02 2020 at 15:13):

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

view this post on Zulip Damiano Testa (Oct 02 2020 at 15:21):

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!

view this post on Zulip Reid Barton (Oct 02 2020 at 15:31):

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

view this post on Zulip Mario Carneiro (Oct 02 2020 at 15:32):

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


Last updated: May 08 2021 at 03:17 UTC