easy tactics needed

[kbuzzard]

Could I ask for some help? I am rewriting and reordering the material in NNG and I would like to have two new tactics. One of them is ac_rfl and all it does is simp [add_assoc, add_left_comm, add_comm], and the other one is apply hPQ to hP -- can that be done without modifying core? -- which changes hP : P to hP : Q if hPQ : P -> Q. I would imagine that both of these would be very easy to add for anyone who knew their way around basic tactic writing.

[joneugster]

Yes that can both be done, and should be fairly simple. I'll add them within the next two days

[joneugster]

apply f to h is implemented and works simply like replace h := f h. Only thing I can't overwrite is the apply docstring: you get different docstrings if you hover over apply f or over apply f to h.

ac_rfl is in core and works out of the box. One only needs to add the two instances IsCommutative and IsAssociative in the levels where this is proven. See Game.Tactic.ACRfl for demonstration.

[kbuzzard]

Thanks!