Ordering the natural numbers inductively

Stream: new members

[Martin Epstein]

Hello all. I have my own copy of the natural numbers called MyNat defined in the familiar way:

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

I originally defined less than or equal relation as follows:

def le (a b : MyNat) : Prop := ∃ c, b = a.add c

This worked perfectly well for me, but I thought it would be interesting to use a definition that doesn't rely on add. Here is an alternative definition that was recommended to me:

inductive le : MyNat → MyNat → Prop
  | refl (m : MyNat) : le m m
  | step (m n : MyNat) (h : le m n) : le m n.succ

I like this definition conceptually but I'm struggling to prove the most basic things with it. Can someone give me a tip on how to prove, say, zero.succ is not less than or equal to zero? For inspiration I checked my proof that zero is not a successor but turns out it's just "simp".

[Aaron Liu]

src#Nat.not_succ_le_zero

[Aaron Liu]

seems like a bunch of nofun

[Aaron Liu]

do you know what nofun does

[Martin Epstein]

I'm not familiar with nofun but I had some inspiration right after I posted.

theorem not_succ_le_zero {n : MyNat} : ¬ n.succ.le zero := by
  have eq1 : ∀ m, n.succ.le m → m ≠ zero := by
    intro m
    intro h
    induction h with
    | refl =>
      exact succ_ne_zero
    | step m h mz =>
      exact succ_ne_zero
  have eq2 := eq1 zero
  intro h
  have eq3 := eq2 h
  contradiction

[Kevin Buzzard]

Fun fact: the original version of the Natural Number Game (when it was just being passed around by Imperial students and wasn't on the web) had this definition of <= and nobody could do anything with it ;-) (which is why I changed it for the web version). You just constantly have to prove things using the recursor i.e. do induction on <=

[Robin Arnez]

Note that your proof also works without any of the haves :-)

[Kevin Buzzard]

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

namespace MyNat

inductive le : MyNat → MyNat → Prop
  | refl (m : MyNat) : le m m
  | step (m n : MyNat) (h : le m n) : le m n.succ

theorem not_succ_le_zero {n : MyNat} : ¬ n.succ.le zero := by
  rintro ⟨⟩

[Kevin Buzzard]

theorem succ_ne_zero {n : MyNat} : n.succ ≠ .zero := by
  rintro ⟨⟩

[Kevin Buzzard]

theorem not_succ_le_zero {n : MyNat} : ¬ n.succ.le zero := nofun

as Aaron said

[Kevin Buzzard]

Lean can show from what it knows about the inductive type that there aren't any cases to consider (in the sense that every case can be ruled out by the basic theory of inductive types e.g. distinct constructors gives distinct terms), so these wacky proofs work.

[Kevin Buzzard]

In Lean 3 the corresponding proofs were just . and you would get a point whenever someone asked a question on the Zulip and you could prove it with ., this was like a hole in one when it came to code golf.

[Martin Epstein]

Thanks, everyone. This gives me a lot to work with. So we have three very concise proofs of ¬ n.succ.le zero here (and my long-winded proof).

1. := nofun (Aaron)
2. := by intro; contradiction (Robin)
3. := by rintro ⟨⟩ (Kevin)

[Aaron Liu]

can't we have just define Nat.le as fun a b => Nat.ble a b = true

[Aaron Liu]

would make it a lot simpler

[Martin Epstein]

Here is another very obvious theorem: theorem not_succ_le_self (n : MyNat) : ¬ n.succ.le n

This is just another instance of "distinct constructors give distinct terms" as Prof. Buzzard put it. But once again I'm at a loss for a proof.

[Aaron Liu]

try induction n

[Aaron Liu]

src#Nat.not_succ_le_self

[Martin Epstein]

Thanks Aaron. I got this far:

theorem not_succ_le_self (n : MyNat) : ¬ n.succ.le n := by
  induction' n with n hn
  · exact not_succ_le_zero
  contrapose! hn
  sorry

This leaves us with

n : MyNat
hn : n.succ.succ.le n.succ
⊢ n.succ.le n

So I could close this out if I had the following theorem:
le_of_succ_le_succ {m n : MyNat} : m.succ.le n.succ → m.le n

But I'm struggling with this one too. I tried induction on m and n and neither quite worked.

[suhr]

You can prove it without pattern matching as well:

set_option pp.proofs true

#check Nat.le.recOn

theorem not_one_le_zero: ¬1 ≤ 0 := by
  suffices any_zero: ∀k, 1 ≤ k → k = 0 → False from
    λh ↦ any_zero 0 h rfl
  exact λk ok ↦ ok.recOn
    (λ(h: 1 = 0) ↦ Nat.succ_ne_zero 0 h)
    (λ{k} _ _ (ksz: k.succ = 0) ↦ Nat.succ_ne_zero k ksz)

theorem not_succ_le_zero {n : Nat} : ¬n.succ ≤ 0 :=
  n.recOn not_one_le_zero (λ_ h => h ∘ Nat.le_of_succ_le)

Pattern matching definitely makes proving this much easier. But you can always do it in a low-level way if you find the high-level way too confusing.

[Aaron Liu]

Martin Epstein said:

Thanks Aaron. I got this far:

theorem not_succ_le_self (n : MyNat) : ¬ n.succ.le n := by
  induction' n with n hn
  · exact not_succ_le_zero
  contrapose! hn
  sorry

This leaves us with

n : MyNat
hn : n.succ.succ.le n.succ
⊢ n.succ.le n

So I could close this out if I had the following theorem:
le_of_succ_le_succ {m n : MyNat} : m.succ.le n.succ → m.le n

But I'm struggling with this one too. I tried induction on m and n and neither quite worked.

Oh yeah you also need to prove that one too

[Aaron Liu]

it's also induction you should do that first

[Kevin Buzzard]

You should prove a<=b iff there exist c such that b=a+c as soon as possible and then just use that for everything, IMO, if all you want to do is develop API. For example if you have the b=a+c result then m.succ <= n.succ implies m<=n is immediate assuming you have enough results about addition. In NNG I develop all the basic theory for addition in "advanced addition world" e.g. x+y=0 -> x=0, a+b=a+c implies b=c etc, and this makes inequality world (the next world) relatively straightforward. I find all this struggling with induction on le much harder than the approach I adopted in NNG, although of course if you are specifically struggling for its own sake then maybe that's the point.

My take on this is that the inductive definition of <= looks very much like the inductive definition of naturals, and thinking about it with the b=a+c perspective shows you that the two constructors for inductive le are closely represented to zero and succ for c. So in some sense what you're doing is making a second more convoluted copy of the naturals with the inductive definition, and now you don't have access to any of the API you've proved for naturals because you now have this weird new copy instead. The b=a+c definition avoids this problem. That's why I think the le definition is harder to develop API for; basically you have to start again.

[Martin Epstein]

Thanks Kevin, that's a useful way to look at it. Before trying out this inductive definition I had indeed made good progress with the additive definition. I got as far as proving
1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2
This might not look like a result about ordering, but my proof using telescoping series and this only works in the natural numbers if the order properties are favorable.
I also had another definition before the additive one: m.le n \iff m.sub n = zero. This one is truly cursed ;)

I took another stab at this inductive ordering business today and finally managed to prove a good reduction theorem: le_iff_eq_or_le_pred. Note that I have a predecessor operation pred defined as

def pred : MyNat → MyNat
  | zero => zero
  | succ x => x

Here is the theorem and proof:

theorem le_iff_eq_or_le_pred {m n : MyNat} :
m.le n ↔ m = n ∨ m.le n.pred := by
  constructor
  · intro h
    induction h with
    | refl =>
      left;  rfl
    | step n h1 h2 =>
      rw [pred]
      rcases h2 with h2 | h2
      · rw [h2]; right; exact le.refl n
      right; exact h1
  intro h; rcases h with h | h
  · rw [h]; exact le.refl n
  have eq1 := le.step m n.pred h
  cases n
  case zero =>
    rw [pred] at h; exact h
  case succ n =>
    rw [pred] at eq1; exact eq1

With this I was able to prove le_of_succ_le_succ which opens a lot of doors.

[Martin Epstein]

Here is an alternative approach that doesn't use pred. It seems you can't use induction directly on m.le n.succ since the right side is not an atomic variable. But I found a workaround.

example {m n : MyNat} :
m.le n.succ ↔ m = n.succ ∨ m.le n := by
  constructor
  · have eq1 :
∀ a : MyNat, a = n.succ → m.le a → m = n.succ ∨ m.le n := by
      intro a ha h
      induction h with
      | refl =>
        left; exact ha
      | step a hm hn =>
        right
        rw [succ_inj] at ha
        rw [ha] at hm; exact hm
    exact eq1 n.succ rfl
  intro h
  rcases h with h | h
  · rw [h]; exact le.refl n.succ
  exact le.step m n h