Introduce ordering relation

Stream: lean4

[kvanvels]

I am a newbie and I am trying to introduce a "less than" function on my home-grown implementation of the natural numbers. This is what (in pertinent part)

inductive ℕ where
  | zero : ℕ
  | succ : ℕ → ℕ
  deriving Repr

def add (m n : ℕ) : ℕ :=
  match n with
  | ℕ.zero => m
  | ℕ.succ l => ℕ.succ (add m l)

instance : Add ℕ where
  add := add

def mylt (m n : ℕ) : Prop :=
  ∃ l : ℕ, (n + l = m ∧ l ≠ ℕ.zero)

instance : LT ℕ where
  lt := mylt

example (n : ℕ) : ℕ.zero < ℕ.zero.succ :=
  sorry --i don't know what I can do here.

The example is just trying to show that zero is less and one.

It seems like I am defining LT incorrectly somehow. I would have expected that it would "rewrite" the goal
"zero < zero.succ" to the RHS of mylt. But it just leaves it as "zero < zero.succ". I think I have misunderstanding of how the LT functions are supposed to be used.

Note that If I comment out the" instance: LT \N line", then it complains about not having definition of $<$. I come from a C++ background where defining things like operator< is exactly like this, so perhaps I am still thinking in C++ mode.

The manual for lean 3 has a pretty large section
on ordering relations, but the manual for lean4 doesn't as far as I can tell. Any help will be greatly appreciated. Also I am aware that I could just use the Nat class but I want to understand the simplest things first.

[Mario Carneiro]

what you can do is assert the type of the goal is exists of something

[Mario Carneiro]

example (n : ℕ) : ℕ.zero < ℕ.zero.succ :=
  show ∃ l, _ from
  _

[Mario Carneiro]

here's another way to do it that doesn't require knowing the shape of the goal:

example (n : ℕ) : ℕ.zero < ℕ.zero.succ := by
  dsimp [LT.lt, mylt]

[Mario Carneiro]

the theorem's not going to be provable because your definition is backwards: n and m should be interchanged

[Mario Carneiro]

and here's a golfed proof of the corrected statement:

def mylt (m n : ℕ) : Prop :=
  ∃ l : ℕ, (m + l = n ∧ l ≠ ℕ.zero)

instance : LT ℕ where
  lt := mylt

example : ℕ.zero < ℕ.zero.succ :=
  ⟨ℕ.zero.succ, rfl, fun h => nomatch h⟩

[kvanvels]

Thank you for the response. I appreciate it. I am taking a break now, but will look at this soon.

[kvanvels]

Thanks, It works great. I did need to add an axiom that zero is not the successor of any other natural number, so I modified the '''fun h => nomatch h''' argument to something different.

[Jireh Loreaux]

That zero is not the successor of any other natural is an immediate consequence of the fact that the naturals are declared as an inductive type. This fact is accessed with nomatch.