undo intro

Stream: general

[Billy Price]

Easy question - what's the opposite of the intros tactic? How do I move a term in the context to a universal quantification in the goal - or a hypothesis to an antecedent?

[Bryan Gin-ge Chen]

tactic#revert should do it.

[Sina]

Bryan Gin-ge Chen said:

tactic#revert should do it.

can you give an example of the use of this tactic?

[Alex J. Best]

lemma hi : ∀ n, n + 1 + 1 = n + 2 :=
begin
  intro n,
  revert n,
  sorry,
end

[Alex J. Best]

Or do you want an example where this is actually useful?

[Alex J. Best]

In that case maybe https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Example.20of.20an.20essential.20use.20of.20revert/near/218374738 is what you want

[Sina]

This is a good simple example! thanks! But, shouldn't <revert n> come after <sorry,> ? I mean in natural deduction, you introduce n then you prove something with it and then you eliminate it to get for all. What am i missing here?
Also, how do you write inline code on Zulip? seems <xyz> is not doing that.

[Ruben Van de Velde]

` for code

[Alex J. Best]

sorry is just used because its a silly/minimal example, in actual usage yes you might intro n then do a rewrite or some other tactics, then revert n

[Kyle Miller]

Sina said:

I mean in natural deduction, you introduce n then you prove something with it and then you eliminate it to get for all. What am i missing here?

Tactics are a bit different from natural deduction judgments. One difference that the tactic context knows the statement you are trying to prove from the beginning, and every tactic can manipulate both hypotheses and goals. intro n in Alex's example ends up doing all the work of introducing n and eliminating it at the end.

revert is useful for moving hypotheses back into the goal to help get the induction hypothesis you want, for example.