Stream: new members

Topic: Example of an essential use of revert

Lars Ericson (Dec 01 2020 at 02:33):

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 (Dec 01 2020 at 02:44):

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,
{ intro n,
rw hm,
end


Yakov Pechersky (Dec 01 2020 at 02:44):

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 (Dec 01 2020 at 02:46):

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 (Dec 01 2020 at 02:51):

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
{ -- notice that we _do_ have to intro n, since it was generalized,
-- but not any of the extraneous k l x y z
rw hm,
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
{ -- 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