Zulip Chat Archive

Stream: new members

Topic: Example of an essential use of revert


view this post on Zulip 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?

view this post on Zulip 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,
    rw zero_add,
    rw add_comm },
  { intro n,
    rw succ_add,
    rw hm,
    rw succ_add,
    rw succ_add,
    rw succ_add },
end

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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`
    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

Last updated: May 12 2021 at 23:13 UTC