## Stream: new members

### Topic: Revert

#### bulut (Apr 19 2019 at 13:39):

What does the revert tactic exactly do?

#### Kevin Buzzard (Apr 19 2019 at 13:42):

The opposite of intro.

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


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

Yup.

Thank you!

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

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

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

#### Kevin Buzzard (Apr 19 2019 at 14:22):

revert (1+2) ->

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