Not equal nats

Stream: new members

[GabrielT]

Is there a more succinct way to prove that 2 natural numbers are not equal? This is what I've done:

-- Axiom 2.3
axiom zero_is_not_succ : ∀ m : ℕ', succ m ≠ zero

-- Axiom 2.4
axiom succ_elim {m n : ℕ'}: succ m = succ n -> m = n

theorem three_not_eq_two : 3 ≠ 2 := by
  by_contra h
  have h2 : 1 = 0 := succ_elim (succ_elim h)
  exact zero_is_not_succ zero h2
  qed

But I don't see that scaling very well to cases like the following:

theorem big_neq : 200 ≠ 199 := by
  by_contra h
  have h2 : 1 = 0 := ???
  exact zero_is_not_succ zero h2
  qed

I've been trying to build something like foldl with succ_elim but couldn't find a way to do it.

[Siddhartha Gadgil]

If it is specific natural numbers, then you can use by decide as the problem is decidable.

[Siddhartha Gadgil]

Also note that your first axiom is a theorem in the library: Nat.succ_ne_zero in the linbrary. The second can be proved too:

open Nat in
theorem succ_elim {m n : ℕ}: succ m = succ n -> m = n := by
  intro h
  injection h

[Frédéric Dupuis]

theorem big_neq : 200 ≠ 199 := by norm_num

would be the usual way to do this.

[GabrielT]

thanks @Siddhartha Gadgil and @Frédéric Dupuis! I'll check those out. Btw, I've been trying to write Terence Tao's Analysis 1 book in lean just for fun (and learning). I was trying to define everything from scratch and got curious how you would normally solve something like that, should've probably mentioned that

[Siddhartha Gadgil]

It is more idiomatic in Lean to define natural numbers as an inductive type. The axioms are consequences of the inductive definition.

A bunch of examples related to what you are trying is at https://github.com/siddhartha-gadgil/proofs-and-programs-2023/blob/main/PnP2023/Lec_01_11/NatLe.lean and as docs at https://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/doc/PnP2023/Lec_01_11/NatLe.html
In particular you can see how repeat and first can be used in similar situations.

[Kyle Miller]

@GabrielT I'm on my phone so didn't test it in Lean, but I'd expect this to work:

theorem three_not_eq_two : 3 ≠ 2 := by
  intro h
  cases h

The cases tactic knows about constructors and their injectivity.

[GabrielT]

oh nice! that worked beautifully @Kyle Miller

[GabrielT]

@Siddhartha Gadgil yes, I defined it inductively https://github.com/gabriel128/analysis_in_lean/pull/1/files#diff-81023a9288ace0a16002f75395faf42e1020e962b663c600c8add2529bdd3189L7 I only copied a small portion of what I had just to get the minimal reproducible instance.

[GabrielT]

I got an idea from what @Siddhartha Gadgil shared and ended up solving it like this

-- Axiom 2.3
axiom zero_is_not_succ : ∀ m : ℕ', succ m ≠ zero

-- Axiom 2.4
axiom succ_elim: ∀ (m n : ℕ'), succ m = succ n -> m = n

lemma ne_succ_intro {m n : ℕ'}: m ≠ n -> succ m ≠ succ n := by
  contrapose!
  apply succ_elim
  qed

macro "not_eq" : tactic =>
  `(tactic | repeat (first | apply zero_is_not_succ | apply ne_succ_intro))

theorem three_not_eq_two : 500 ≠ 39 := by
  not_eq
  qed

thanks all for the help!

[Eric Wieser]

You should probably not be adding new axioms on top of an inductive type

[Eric Wieser]

Both axioms are true as theorems:

-- Axiom 2.3
theorem zero_is_not_succ : ∀ m : ℕ', succ m ≠ zero := fun.

-- Axiom 2.4
theorem succ_elim : ∀ (m n : ℕ'), succ m = succ n -> m = n := @Natu.succ.inj

[GabrielT]

I only did it because that's presented as an axiom in Terence Tao's book, but I get your point. It was actually straight forward to prove, I might transform the rest of the axioms to lemmas

lemma succ_elim: ∀ (m n : ℕ'), succ m = succ n -> m = n := by
  intro h h1 h2
  cases h2
  rfl
  done

[Eric Wieser]

Note that Lean generates that lemma for you as Natu.succ.inj, which is how I prove it above.

[GabrielT]

yeah I was going to ask you that, where does inj come from? is that documented somewhere?

[Eric Wieser]

If you're going to follow an axiomatic presentation, I recommend avoiding inductive and doing everything axiomatically. Otherwise you're using a mixture of the axioms from the source and the axioms that lean gives you, and you have the worst of both worlds (doesn't follow the source material or guarantee soundness).

[Eric Wieser]

GabrielT said:

yeah I was going to ask you that, where does inj come from? is that documented somewhere?

It's generated by the inductive keyword (using a proof like yours), I'm afraid I don't know where it's documented

[Eric Wieser]

You can #print Natu.succ.inj to see the proof

[GabrielT]

yeah I've been trying to avoid using inductive and defined induction as an axiom

axiom math_induction (n : ℕ') (P: ℕ' → Prop) (hzero : P zero): (P n → P (succ n)) -> P n

which is what the book does. However I might probably have used some things that use inductive behind the scenes

[Eric Wieser]

If you use axiom ℕ' : Type as well then you should be clear of any accidental use of inductive