Stream: new members
Topic: Replacing rw with terms
Andreas Swerdlow (Sep 15 2018 at 13:37):
I have some proofs written in tactic mode that contain a lot of rewrites, including rewrites of hypotheses. Is there a way to easily convert such proofs into term mode. I know about eq.subst but can’t see a way to do this that won’t take aeons.
Apologies in advance I’m away so won’t be replying quickly.
Kevin Buzzard (Sep 15 2018 at 13:40):
The term mode version of
rw is the rather harder to use
\t, which is notation for
eq.subst, which you already know about. In special cases you can be lucky -- e.g. if your goal is
X and you want to rewrite
H : X <-> Y then you can just apply
H.2. But if it's a more complicated rewrite then you either briefly drop into tactic mode with
by rw [A,B,C] or grit your teeth and wrestle with the triangle (which is far more picky about metavariables for some reason; giving things explicit types sometimes helps).
Chris Hughes (Sep 15 2018 at 13:41):
rw's should be done in tactic mode, but often you can replace a bunch of rewrites with a
simp, with carefully chosen lemmas in the
Kevin Buzzard (Sep 15 2018 at 13:41):
Kevin Buzzard (Sep 15 2018 at 13:42):
I was working on that today. Originally all proofs were in tactic mode. I then managed to turn most stuff into term mode, but failed on that last line so left the rewrite in.
Andreas Swerdlow (Sep 15 2018 at 15:01):
Is there any advantage to term mode in a case like this?
Kevin Buzzard (Sep 15 2018 at 16:55):
I think term mode proofs are less likely to break, or perhaps they break in very predictable ways. But I honestly don't know. I just get the feeling that the mathlib people like term mode better if possible, so that's what I'm working towards. I don't have any maintainer experience.
Last updated: May 15 2021 at 00:39 UTC