Revert

Stream: new members

[bulut]

What does the revert tactic exactly do?

[Kevin Buzzard]

The opposite of intro.

[Kevin Buzzard]

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

[bulut]

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

[Kevin Buzzard]

Yup.

[bulut]

Thank you!

[Kevin Buzzard]

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]

@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]

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]

revert (1+2) ->

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