Zulip Chat Archive

Stream: new members

Topic: Reverse assume / Deduction Theorem


view this post on Zulip Henning Dieterichs (Jan 06 2021 at 10:48):

I have (h: P) |- X. Is there a tactic that rewrites this to |- P -> X? This would be helpful for the simplifier, as simp would then (probably) solve the goal - after simplification it should have Y -> Y and then true.

view this post on Zulip Henning Dieterichs (Jan 06 2021 at 10:49):

It is revert, sorry for the spam. I searched for deduction etc. There are just too many tactics...

view this post on Zulip Reid Barton (Jan 06 2021 at 11:36):

revert is a funny basic-but-rare tactic: according to Jason's slides from yesterday, it is not among the top 20 most commonly used tactics in mathlib

view this post on Zulip Henning Dieterichs (Jan 06 2021 at 11:41):

Is there a list of the most used tactics? Maybe even depending on the types that occur in the current goal? ;)

view this post on Zulip Reid Barton (Jan 06 2021 at 11:47):

according to the slides the order is rw, simp, exact, apply, have, cases, refine, refl, intros, simpa, ext, rcases, intro, rwa, dsimp, by_cases, split, induction, rintros, convert

view this post on Zulip Reid Barton (Jan 06 2021 at 11:47):

https://docs.google.com/presentation/d/1poOu2gP9mSGAdAFvOupHvf4tpgD33jACQLJAVcphA1g/edit#slide=id.gb359d37294_4_0 slide 14

view this post on Zulip Reid Barton (Jan 06 2021 at 11:47):

I'm sure their model contains information of the latter kind :upside_down:

view this post on Zulip Alex J. Best (Jan 06 2021 at 11:52):

Poor gpt, doesn't know the satisfaction of a good ac_refl call

view this post on Zulip Henning Dieterichs (Jan 06 2021 at 11:52):

wow this is awesome. I cannot wait to see open AI tackle automated theorem proofing :D


Last updated: May 12 2021 at 22:15 UTC