Proving Nat less than is well-founded

Stream: lean4

[Brandon Brown]

I'm trying to prove the well-foundedness of the less-than relation on the natural numbers using the accessibility inductive type approach, but I'm either misunderstanding how to use Acc, missing some valid moves in Lean4 or misunderstanding the proof.

I'd like to be able to prove that Acc Nat.lt x -> Acc Nat.lt (succ x) because I can then easily use that lemma to prove that ∀ x : Nat, Acc Nat. lt x (i.e. that it is well-founded), but I'm having a hard time with this.

theorem acc_succ : ∀ x : Nat, Acc Nat.lt x → Acc Nat.lt x.succ := by
  intros x h
  apply Acc.intro;
  intros y h2;
  apply Acc.inv h; -- stuck
  -- ⊢ y < x

Since I assume Acc Nat.lt x, then that means all y < x are accessible too. And since x is the immediate predecessor of x.succ, then we know that all y < x.succ are accessible, and if we should know that then we know that Acc Nat.lt (succ x)

open Nat

theorem zero_acc : Acc Nat.lt 0 := by
  apply Acc.intro
  intros y h
  apply False.elim
  cases h

theorem succ_acc {x : Nat} : Acc Nat.lt x.succ → Acc Nat.lt x := by
  intros h
  apply Acc.intro
  intros y h2
  apply Acc.inv h
  apply Nat.leSuccOfLe
  exact h2

theorem acc_succ : ∀ x : Nat, Acc Nat.lt x → Acc Nat.lt x.succ := by
  intros x h
  apply Acc.intro;
  intros y h2;
  apply Acc.inv h; -- stuck
  -- ⊢ y < x

def well_founded {α : Type _} (r : α → α → Prop) : Prop := ∀ x : α, Acc r x

theorem nat_lt_is_wf : well_founded Nat.lt := sorry

[Mario Carneiro]

Don't use Acc.inv, that's the inverse to intro so you won't get anywhere

[Mario Carneiro]

Since you are proving that nat is inductively generated by less than, the proof is naturally going to go via induction

[Mario Carneiro]

theorem Nat.eq_or_lt_of_lt_succ : m < Nat.succ n → m = n ∨ m < n := sorry

theorem acc_succ : ∀ x : Nat, Acc Nat.lt x := by
  intro x
  induction x with (apply Acc.intro; intro y h)
  | zero => cases h
  | succ n ih => ?_
  match Nat.eq_or_lt_of_lt_succ h with
  | Or.inl rfl => exact ih
  | Or.inr h' => exact ih.inv h'

[Brandon Brown]

Thanks, Mario! I wasn't familiar with the induction x with (apply Acc.intro; intro y h) syntax, but it looks like it just adds it into each case similar to generalizing, good to know
equivalent to

theorem acc_succ : ∀ x : Nat, Acc Nat.lt x := by
  intro x
  induction x with
  | zero =>
    apply Acc.intro; intro y h
    cases h
  | succ n ih => ?_
    apply Acc.intro; intro y h
    match Nat.eq_or_lt_of_lt_succ h with
    | Or.inl rfl => exact ih
    | Or.inr h' => exact ih.inv h'