Reverse assume / Deduction Theorem

Stream: new members

[Henning Dieterichs]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Alex J. Best]

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

[Henning Dieterichs]

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