Zulip Chat Archive

Stream: new members

Topic: Revert


view this post on Zulip bulut (Apr 19 2019 at 13:39):

What does the revert tactic exactly do?

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 13:42):

The opposite of intro.

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 13:42):

example (P Q : Prop) (hPQ : P  Q) (hP : P) : Q :=
begin
  revert hP,
  intro hP,
  revert hP,
  exact hPQ
end

view this post on Zulip bulut (Apr 19 2019 at 13:48):

So if the goal is to prove P, revert hQ (where hQ has type Q) changes the goal to Q->P?

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 13:50):

Yup.

view this post on Zulip bulut (Apr 19 2019 at 13:51):

Thank you!

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 13:51):

You can check that like this:

example (P Q : Prop) (hQ : Q) : P :=
begin
  revert hQ,
  sorry
end

The nice thing about Lean is that if you can precisely formalise a question (like yours above) then you don't even need to ask it, you can just ask Lean :D

view this post on Zulip Simon Hudon (Apr 19 2019 at 14:19):

@Kevin Buzzard I think this is leaving out a couple of things. If you know nothing about what revert does, you can try revert (1 + 2) see the complaint (actually, right now, Lean will crash) and be puzzled about why that's a wrong argument. Or worse, you call revert see nothing happened and not know where to go from there.

view this post on Zulip Simon Hudon (Apr 19 2019 at 14:19):

If you put your cursor on revert in VS code, I think it will show you its documentation though so that should be helpful.

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 14:22):

revert (1+2) ->

failed to synthesize type class instance for
P Q : Prop,
hQ : Q
⊢ has_add tactic_state

Last updated: May 14 2021 at 06:16 UTC