## Stream: new members

### Topic: Reverse assume / Deduction Theorem

#### 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.

#### 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...

#### 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

#### 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? ;)

#### 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

#### Reid Barton (Jan 06 2021 at 11:47):

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

#### Alex J. Best (Jan 06 2021 at 11:52):

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

#### 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