strong_induction

gistfile1.txt

theorem Nat.not_lt_zero (n : Nat) : ¬(n < 0) := by
  intro h; rw [Nat.lt_iff] at h
  have ⟨a, h'⟩ := h.left; exact h.right (Nat.add_eq_zero n a h'.symm).left

theorem Nat.not_lt_zero' (n : Nat) : ¬(n < zero) := Nat.not_lt_zero n

theorem Nat.le_of_lt_succ {a b : Nat} : a < b++ → a ≤ b
  | ⟨⟨x, y⟩, bb⟩ => by
    have h : a + x ≠ 0 := by
      intro h'
      rw [h'] at y
      cases y
    have hxnz : x ≠ 0 := by
      intro h
      simp [h] at y
      exact bb y.symm
    have ⟨d, hd⟩ := uniq_succ_eq x hxnz
    simp at hd
    rw [← hd.left] at  y
    simp [add_succ] at y
    exact ⟨d, y⟩

/- Using structural induction, I guess what they expect you to do in the book -/
theorem Nat.strong_induction_structural {m₀:Nat} {P: Nat → Prop}
  (hind: ∀ m, m₀ ≤ m → (∀ m', m₀ ≤ m' ∧ m' < m → P m') → P m) (mX : Nat) : m₀ ≤ mX →  P mX := by
  intro h
  apply hind mX h
  induction mX with
   | zero =>
    intro m' hm'
    obtain ⟨ h₀, h₁ ⟩ := h
    exact False.elim ((not_lt_zero' _) hm'.right)
   | succ m ih =>
     intro m'' h''
     have hLe : m'' ≤ m := le_of_lt_succ h''.right
     apply hind m''
     . exact h''.left
     .
       intro m' ⟨hL, hR⟩
       apply ih
       .
         have h01 : m₀ < m'' := lt_of_le_of_lt hL hR
         have h02 : m₀ < m := lt_of_lt_of_le h01 hLe
         exact le_of_lt h02
       . exact ⟨hL, (lt_of_lt_of_le hR hLe)⟩

/- Show that for the redefined Nat, LT is well founded -/
instance lt_wfRel : WellFoundedRelation Nat where
  rel := (· < ·)
  wf  := by
    apply WellFounded.intro
    intro n
    induction n with
    | zero      =>
      apply Acc.intro 0
      intro _ h
      exact False.elim (Nat.not_lt_zero _ ‹_›)
    | succ n ih =>
      apply Acc.intro (Nat.succ n)
      intro m h
      have : m = n ∨ m < n := ((Nat.le_iff_lt_or_eq _ _).mp (Nat.le_of_lt_succ h)).symm
      match this with
      | Or.inl e => subst e; assumption
      | Or.inr e => exact Acc.inv ih e


/- The WF version using the Tao statement -/
theorem Nat.strong_induction_wf {m₀:Nat} {P: Nat → Prop}
  (hind: ∀ m, m₀ ≤ m → (∀ m', m₀ ≤ m' ∧ m' < m → P m') → P m) (m : Nat) (hm : m₀ ≤ m) : P m :=
    hind m hm <| fun m' hh => strong_induction_wf hind m' hh.left
termination_by m
decreasing_by exact hh.right

/- This is the way it's stated in Lean proper. -/
theorem Nat.strong_induction_wf' {P: Nat → Prop}
  (hind: ∀ m, (∀ m', m' < m → P m') → P m) (t : Nat) : P t :=
    hind t <| fun m' _ => strong_induction_wf' hind m'
termination_by t