Example of an essential use of revert

Stream: new members

[Lars Ericson]

I am reading chapter 5.2 of TPIL. Every example of revert is redundant. For example

example (x y : ℕ) (h : x = y) : y = x :=
begin
  revert x y,
  -- goal is ⊢ ∀ (x y : ℕ), x = y → y = x
  intros,
  symmetry,
  assumption
end

can be reduced to

example (x y : ℕ) (h : x = y) : y = x :=
begin
  symmetry,
  assumption,
end

Can you think of any tactic-mode proofs that include an essential/compelling use of revert?

[Yakov Pechersky]

import data.nat.basic

open nat

-- let's prove associativity without using associativity
example {m n : ℕ} : m + n.succ = m.succ + n :=
begin
  revert n,
  induction m with m hm,
  { intro n,
    rw zero_add,
    rw add_comm },
  { intro n,
    rw succ_add,
    rw hm,
    rw succ_add,
    rw succ_add,
    rw succ_add },
end

[Yakov Pechersky]

You might say, well that's just induction m with m hm generalizing n but that's exactly what the generalizing n part does, figures out what and how far do we need to revert and then intro.

[Alex J. Best]

The first example

example (x : ℕ) : x = x :=
begin
  revert x,
  -- goal is ⊢ ∀ (x : ℕ), x = x
  intro y,
  -- goal is y : ℕ ⊢ y = y
  reflexivity
end

in #tpil is mathematically redundant yes, but is demonstrating that revert can be used to rename variables.

[Yakov Pechersky]

example {m n k l x y z : ℕ} : m + n.succ = m.succ + n :=
begin
  -- here we have lots of extra variables that may or may not have been used in other hypotheses
  induction m with m hm generalizing n,
  { -- notice that we don't have to intro anything, not `n` nor any of the extraneous `k l x y z`
    rw zero_add,
    rw add_comm },
  { -- notice that we _do_ have to intro `n`, since it was generalized,
    -- but not any of the extraneous `k l x y z`
    rw succ_add,
    rw hm,
    rw succ_add,
    rw succ_add,
    rw succ_add },
end

example {m n k l x y z : ℕ} (h : m = x + y + z) : m + n.succ = m.succ + n :=
begin
  -- here we have lots of extra variables, some which are used in other hypotheses
  induction m with m hm generalizing n,
  { -- notice that we don't have to intro anything, not `n` nor any of the extraneous `k l x y z`
    rw zero_add,
    rw add_comm },
  { -- notice that we _do_ have to intro `n`, since it was generalized,
    -- but not any of the extraneous `k l x y z`
    -- and now our induction hypothesis is broken because of the blocking `h`
    rw succ_add,
    rw hm, -- won't work
    rw succ_add,
    rw succ_add,
    rw succ_add },
end