# Zulip Chat Archive

## Stream: new members

### Topic: Using `rw`

#### Daniel Keys (Jan 22 2020 at 23:45):

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 (Jan 22 2020 at 23:52):

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 (Jan 22 2020 at 23:54):

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 (Jan 22 2020 at 23:55):

`nat`

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

#### Mario Carneiro (Jan 23 2020 at 00:16):

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 (Jan 23 2020 at 00:20):

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

#### Mario Carneiro (Jan 23 2020 at 00:26):

-- 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 (Jan 23 2020 at 00:29):

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 (Jan 23 2020 at 00:31):

-- 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 (Jan 23 2020 at 00:46):

This helps! Where, i.e. in what file, is `succ_inj`

defined in the LEAN source code?

#### Mario Carneiro (Jan 23 2020 at 00:56):

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 (Jan 23 2020 at 00:58):

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 (Jan 23 2020 at 07:51):

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

Last updated: May 08 2021 at 09:11 UTC