## 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):

Last updated: May 08 2021 at 09:11 UTC