Using `rw`

Stream: new members

[Daniel Keys]

How can one prove these using only (or mainly) rw without any tactic in mathlib or the use of succ_inj or even succ?

variables m  n : ℕ
theorem T1 ( hyp : n + 1 = m + 1 ) :  n = m  :=
begin
    sorry
end

theorem T2 (hyp : n = m + 1 )  :  n > m  :=  sorry

[Joe]

But the first one is just nat.succ_inj hyp.

What do you want to accomplish by only using rw? After all, some rewrite lemma must need nat.succ_inj.

[Daniel Keys]

Yes, it is just succ_inj. Basically what I'm saying is that I would like to know how succ_inj is proved from first principles. The first one is similar to a problem in the natural number game by Kevin Buzzard.

[Yury G. Kudryashov]

nat is defined as an inductive type, and all constructors are injective by definition.

[Mario Carneiro]

The proof of injectivity of constructors is somewhat involved. The core theorem is called nat.no_confusion, and it's defined from the recursor

[Yury G. Kudryashov]

This theorem has an unreadable type that basically says "all constructors are injective".

[Mario Carneiro]

-- first, consider the following definition:
-- def nat.injected : nat → nat → Prop
-- | 0 0 := true
-- | (m + 1) (n + 1) := m = n
-- | _ _ := false

-- which we write using the recursor because we aren't assuming
-- the equation compiler
def nat.injected (m n : nat) : Prop :=
nat.rec
  (λ n, nat.rec true (λ _ _, false) n)
  (λ m IH n, nat.rec false (λ n _, m = n) n)
  m n

-- Now we prove by cases that this follows from equality, by a one argument recursion
theorem nat.injected_of_eq {m n} (h : m = n) : nat.injected m n :=
suffices nat.injected m m, from h ▸ this,
nat.rec trivial (λ n _, rfl) m

-- And now we observe that injectivity follows:
theorem nat.succ_inj' {m n} (h : m + 1 = n + 1) : m = n :=
nat.injected_of_eq h

[Mario Carneiro]

The version you see in nat.no_confusion and nat.no_confusion_type is the same argument, but written in a way that generalizes to arbitrary inductive types

[Mario Carneiro]

-- This is also how you can show that zero is not a successor
theorem nat.succ_ne_zero' {n} (h : n + 1 = 0) : false :=
nat.injected_of_eq h

[Daniel Keys]

This helps! Where, i.e. in what file, is succ_inj defined in the LEAN source code?

[Mario Carneiro]

You can ctrl-click on things in vscode to find them, but it probably won't help much in this case. nat.succ_inj is defined in init.data.nat.lemmas, but it is just an alias:

theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m :=
nat.succ.inj_arrow H id

where nat.succ.inj_arrow is an automatically generated lemma that is created when nat itself is written down

[Mario Carneiro]

Here is the stack of definitions involved. All of these except the first are autogenerated

#print nat.succ_inj
#print nat.succ.inj_arrow
#print nat.succ.inj
#print nat.no_confusion
#print nat.no_confusion_type
#print nat.cases_on

[Kevin Buzzard]

Related: https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/