Help with solving Tao's Analysis Chapter 2 epilogue problem

Stream: Analysis I

[Rado Kirov]

After a bit of hiatus, I am back on working through good Lean exercises / puzzles to practice and learn the basics of formalization. Big thanks to @Terence Tao for formalizing the exercises from his Analysis book https://github.com/teorth/analysis which is proving to be at the right level of challenge for me after the NNT.

I am at the end of chapter 2 (my solutions so far are at https://github.com/rkirov/analysis), but really stuck on establishing the equivalence between a model of the axiomatic Peano and the constructive induction types one from Mathlib.

This should be an isolated reproduction - see function f and it's comment at the end. I think I should be able to handle the sorries after I get a working inverse function definition.

import Mathlib.Tactic

namespace repro
/-- The Peano axioms for an abstract type `Nat` -/
@[ext]
class PeanoAxioms where
  Nat : Type
  zero : Nat -- Axiom 2.1
  succ : Nat → Nat -- Axiom 2.2
  succ_ne : ∀ n : Nat, succ n ≠ zero -- Axiom 2.3
  succ_cancel : ∀ {n m : Nat}, succ n = succ m → n = m -- Axiom 2.4
  induction : ∀ (P : Nat → Prop),
    P zero → (∀ n : Nat, P n → P (succ n)) → ∀ n : Nat, P n -- Axiom 2.5

/-- The notion of an equivalence between two structures obeying the Peano axioms -/
class Equiv (P Q : PeanoAxioms) where
  equiv : P.Nat ≃ Q.Nat
  equiv_zero : equiv P.zero = Q.zero
  equiv_succ : ∀ n : P.Nat, equiv (P.succ n) = Q.succ (equiv n)

/-- The Mathlib natural numbers obey the Peano axioms. -/
def Mathlib.Nat : PeanoAxioms where
  Nat := ℕ
  zero := 0
  succ := Nat.succ
  succ_ne := Nat.succ_ne_zero
  succ_cancel := Nat.succ_inj.mp
  induction _ := Nat.rec

/-- One can map the Mathlib natural numbers into any other structure obeying the Peano axioms. -/
abbrev natCast (P : PeanoAxioms) : ℕ → P.Nat := fun n ↦ match n with
  | Nat.zero => P.zero
  | Nat.succ n => P.succ (natCast P n)

theorem zero_or_succ (P : PeanoAxioms) (x : P.Nat): x = P.zero ∨ ∃ n, x = P.succ n := by
  revert x
  apply P.induction
  . left
    rfl
  . intro n ih
    right
    use n

/--
The general idea is use Classical logic to and the `zero_or_succ` lemma to define a function
that can do non-computable match on x - it is either zero or a successor - and then recurse.

Using Claude I got to something that almost work using `Classical.indefiniteDescription
but it is:
1) feels too complicated? why can't I just use `match`?
2) still doesn't work because of non-terminating recursion.
--/
noncomputable def f (P: PeanoAxioms) (x : P.Nat) : ℕ :=
  Classical.indefiniteDescription (fun _ => True) ((zero_or_succ P x).elim
    (fun h_zero => ⟨0, trivial⟩)
    (fun h_succ => ⟨1 + f P (Classical.choose h_succ), trivial⟩))

/-- Note: I suspect that this construction is non-computable and requires classical logic. -/
noncomputable abbrev Equiv.fromNat (P : PeanoAxioms) : Equiv Mathlib.Nat P where
  equiv := {
    toFun := natCast P
    invFun := f P
    left_inv := by sorry
    right_inv := by sorry
  }
  equiv_zero := by sorry
  equiv_succ n := by sorry
end repro

[Aaron Liu]

You do need to use induction here

[Rado Kirov]

Isn't induction for doing Props? This is about defining an actual function from P.Nat to Mathlib.Nat so there is no Prop is sight? Am I missing something?

[Rado Kirov]

Or maybe \exists fun is the Prop to prove with induction?

[Aaron Liu]

The only way to construct the function is to use induction to show it exists, and then choice to get a function out

[Rado Kirov]

great idea, thanks!

[Rado Kirov]

Unfortunately, I also pulled master from upstream, so now I have to wait 30min for mathlib to rebuild lol

[Rado Kirov]

before I can try it

[Aaron Liu]

Did you try lake exe cache get to fetch the cache?

[Rado Kirov]

nope :) just git pull and whatever magic vscode does underneath the hood.

[Rado Kirov]

running lake exe cache get now

[Aaron Liu]

Here's my solution, in case you want to take a look:

My Solution

import Mathlib.Tactic

namespace repro

/-- The Peano axioms for an abstract type `Nat` -/
@[ext]
class PeanoAxioms where
  Nat : Type
  zero : Nat -- Axiom 2.1
  succ : Nat → Nat -- Axiom 2.2
  succ_ne : ∀ n : Nat, succ n ≠ zero -- Axiom 2.3
  succ_cancel : ∀ {n m : Nat}, succ n = succ m → n = m -- Axiom 2.4
  induction : ∀ (P : Nat → Prop),
    P zero → (∀ n : Nat, P n → P (succ n)) → ∀ n : Nat, P n -- Axiom 2.5

/-- The notion of an equivalence between two structures obeying the Peano axioms -/
class Equiv (P Q : PeanoAxioms) where
  equiv : P.Nat ≃ Q.Nat
  equiv_zero : equiv P.zero = Q.zero
  equiv_succ : ∀ n : P.Nat, equiv (P.succ n) = Q.succ (equiv n)

/-- The Mathlib natural numbers obey the Peano axioms. -/
def Mathlib.Nat : PeanoAxioms where
  Nat := ℕ
  zero := 0
  succ := Nat.succ
  succ_ne := Nat.succ_ne_zero
  succ_cancel := Nat.succ_inj.mp
  induction _ := Nat.rec

/-- One can map the Mathlib natural numbers into any other structure obeying the Peano axioms. -/
abbrev natCast (P : PeanoAxioms) : ℕ → P.Nat := fun n ↦ match n with
  | Nat.zero => P.zero
  | Nat.succ n => P.succ (natCast P n)

/-- The map from the standard natural numbers induced by the Peano axioms is injective. -/
theorem natCast_injective (P : PeanoAxioms) : Function.Injective (natCast P) := by
  intro a b hab
  induction a generalizing b with
  | zero =>
    cases b with
    | zero => rfl
    | succ b => exact (P.succ_ne (natCast P b) hab.symm).elim
  | succ a ih =>
    cases b with
    | zero => exact (P.succ_ne (natCast P a) hab).elim
    | succ b => rw [ih (P.succ_cancel hab)]

/-- The map from the standard natural numbers induced by the Peano axioms is surjective. -/
theorem natCast_surjective (P : PeanoAxioms) : Function.Surjective (natCast P) := by
  apply P.induction
  · exact ⟨0, rfl⟩
  · rintro _ ⟨n, rfl⟩
    exact ⟨n + 1, rfl⟩

/-- Any abstract `Nat`-like type is equivalent to the standard natural numbers. -/
noncomputable abbrev Equiv.fromNat (P : PeanoAxioms) : Equiv Mathlib.Nat P where
  equiv := Equiv.ofBijective (natCast P) ⟨natCast_injective P, natCast_surjective P⟩
  equiv_zero := rfl
  equiv_succ _ := rfl

/-- Any two abstract `Nat`-like types are equivalent. -/
noncomputable def PeanoAxioms.equiv (P Q : PeanoAxioms) : Equiv P Q where
  equiv := (Equiv.fromNat P).equiv.symm.trans (Equiv.fromNat Q).equiv
  equiv_zero := by rw [Equiv.trans_apply, ← (Equiv.fromNat P).equiv.eq_symm_apply.mpr (Equiv.fromNat P).equiv_zero, (Equiv.fromNat Q).equiv_zero]
  equiv_succ n := by
    rw [Equiv.trans_apply, Equiv.trans_apply, ← (Equiv.fromNat P).equiv.apply_symm_apply n,
      ← (Equiv.fromNat P).equiv.eq_symm_apply.mpr ((Equiv.fromNat P).equiv_succ ((Equiv.fromNat P).equiv.symm n)),
      (Equiv.fromNat Q).equiv_succ, (Equiv.fromNat P).equiv.apply_symm_apply]

/-- Equivalences between `Nat`-like types are unique. -/
theorem PeanoAxioms.equiv_unique (P Q : PeanoAxioms) (A B : Equiv P Q) : A = B := by
  obtain ⟨E, hE0, hE1⟩ := A
  obtain ⟨F, hF0, hF1⟩ := B
  suffices h : E = F by simp [h]
  apply Equiv.ext
  apply P.induction
  · rw [hE0, hF0]
  · intro n ih
    rw [hE1, hF1, ih]

end repro

[Aaron Liu]

It looks like Tao and I had the same idea, since my lemmas almost perfectly match what's laid out in the exercises

[Rado Kirov]

I see now, because equiv = {toFun, invFun, ...} was expanded, I assumed I had to write each from scratch but Equiv.ofBijective builds it all in one go. I can read the implementation to see what non-computable tricks it uses.

Since you already looked into the setup for this chapter, do you have any hints for the last exercise - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_2_epilogue.lean#L257-L263. I think the idea is clear, after all the equivalences we built, we have proved this result in Chapter2 for the inductive type Nats, so "just" push it through the equivalences between P and Chapter2.Nats. That said I am 100+ lines is with 3 sub-sorries, so definitely doing it wrong.

I can try to provide a smaller repro if it will help.

[Peter Hansen]

Rado Kirov said:

Since you already looked into the setup for this chapter, do you have any hints for the last exercise - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_2_epilogue.lean#L264-L269. I think the idea is clear, after all the equivalences we built, we have proved this result in Chapter2 for the inductive type Nats, so "just" push it through the equivalences between P and Chapter2.Nats. That said I am 100+ lines is with 3 sub-sorries, so definitely doing it wrong.

I did that exercise a while back. Here is a post I made about it:

https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Help.20with.20formalizing.20recursive.20definitions.20from.20Tao's.20A1

Here is the solution I ended up with:

https://github.com/Citronhat/PeanoRec/blob/main/Tao/C1/Recursion/Recursive.lean

[Rado Kirov]

Thanks for sharing. It looks like that conversation predated the skeleton code provided by Tao, so hard for me to see how to modify my problem locally.

I simplified and made a new repro for my last question below. I am really strugging to work with the Equiv class. It seems to me that it rw refuses to replace a piece of text that char for char matches what I see in the target - Equiv.equiv PeanoAxioms.zero. Also no idea why it says Equiv.equiv instead of e.equiv which is the particular equivalence I am working with.

Screenshot 2025-06-28 at 7.17.46 PM.png

import Mathlib.Tactic

namespace Chapter2

/--
  Assumption 2.6 (Existence of natural numbers).  Here we use an explicit construction of the
  natural numbers (using an inductive type).  For a more axiomatic approach, see the epilogue to
  this chapter.
-/
inductive Nat where
| zero : Nat
| succ : Nat → Nat
deriving Repr, DecidableEq  -- this allows `decide` to work on `Nat`

/-- Axiom 2.1 (0 is a natural number) -/
instance Nat.instZero : Zero Nat := ⟨ zero ⟩
#check (0:Nat)

/-- Axiom 2.2 (Successor of a natural number is a natural number) -/
postfix:100 "++" => Nat.succ
#check (fun n ↦ n++)

/--
  Recursion. Analogous to the inbuilt Mathlib method `Nat.rec` associated to
  the Mathlib natural numbers
-/
abbrev Nat.recurse (f: Nat → Nat → Nat) (c: Nat) : Nat → Nat := fun n ↦ match n with
| 0 => c
| n++ => f n (recurse f c n)

/-- Proposition 2.1.16 (recursive definitions). -/
theorem Nat.eq_recurse (f: Nat → Nat → Nat) (c: Nat) (a: Nat → Nat) :
    (a 0 = c ∧ ∀ n, a (n++) = f n (a n)) ↔ a = recurse f c := sorry
end Chapter2

namespace repro
/-- The Peano axioms for an abstract type `Nat` -/
@[ext]
class PeanoAxioms where
  Nat : Type
  zero : Nat -- Axiom 2.1
  succ : Nat → Nat -- Axiom 2.2
  succ_ne : ∀ n : Nat, succ n ≠ zero -- Axiom 2.3
  succ_cancel : ∀ {n m : Nat}, succ n = succ m → n = m -- Axiom 2.4
  induction : ∀ (P : Nat → Prop),
    P zero → (∀ n : Nat, P n → P (succ n)) → ∀ n : Nat, P n -- Axiom 2.5

/-- The notion of an equivalence between two structures obeying the Peano axioms -/
class Equiv (P Q : PeanoAxioms) where
  equiv : P.Nat ≃ Q.Nat
  equiv_zero : equiv P.zero = Q.zero
  equiv_succ : ∀ n : P.Nat, equiv (P.succ n) = Q.succ (equiv n)

/-- The Chapter 2 natural numbers obey the Peano axioms. -/
def Chapter2.Nat : PeanoAxioms where
  Nat := _root_.Chapter2.Nat
  zero := Chapter2.Nat.zero
  succ := Chapter2.Nat.succ
  succ_ne := sorry
  succ_cancel := sorry
  induction := sorry

noncomputable abbrev Equiv.fromCh2Nat (P : PeanoAxioms) : Equiv Chapter2.Nat P := sorry

/-- Trying to remove sorries in this proof. Sorries above are just for simplifying the repro. -/
theorem recurse_uniq {P : PeanoAxioms} (f: P.Nat → P.Nat → P.Nat) (c: P.Nat) :
    ∃! (a: P.Nat → P.Nat), a P.zero = c ∧ ∀ n, a (P.succ n) = f n (a n) := by
  -- basic idea, we already proved this in chapter 2 for Chapter2.Nat
  -- so we just need to use the equivalence between Chapter2.Nat and P.Nat
  -- to transfer the result.
  apply existsUnique_of_exists_of_unique
  let e := Equiv.fromCh2Nat P
  let f_lift := fun a b ↦ e.equiv.symm (f (e.equiv a) (e.equiv b))
  let c_lift := e.equiv.symm c
  let r := Chapter2.Nat.recurse f_lift c_lift
  use fun n ↦ e.equiv (r (e.equiv.symm n))
  have h1 := Chapter2.Nat.eq_recurse f_lift c_lift r
  constructor
  . simp [r]
    have hz : e.equiv.symm P.zero = _root_.Chapter2.Nat.zero := by
      apply_fun e.equiv
      simp
      -- rw [e.equiv_zero] -- why does this not work?
      sorry
    rw [hz]
    simp [Chapter2.Nat.recurse, c_lift]
  . intro a
    simp [r, Chapter2.Nat.recurse, h1]
    -- rw [← h1] -- feels like this should work
    sorry

  -- uniqueness easy enough to prove from scratch, insteadf of lifting
  intro a b h1 h2
  ext n
  revert n
  apply P.induction
  . rw [h1.1, h2.1]
  . intro n ih
    rw [h1.2 n, h2.2 n]
    apply congrArg
    exact ih


end repro

[Aaron Liu]

Rado Kirov said:

I simplified and made a new repro for my last question below. I am really strugging to work with the Equiv class. It seems to me that it rw refuses to replace a piece of text that char for char matches what I see in the target - Equiv.equiv PeanoAxioms.zero.

Really? I see Equiv.equiv Chapter2.Nat.zero

[Rado Kirov]

Yes, there is different display in the error hover tooltip and in the Lean Info. Chapter2.Nat is the particular instance of the PeanoAxioms type-class. I still expect what I am trying to prove in line 83 to be exactly the content of e.equiv_zero.

[Aaron Liu]

No, Chapter2.Nat.zero is not the same as (Chapter2.Nat).zero

[Aaron Liu]

It's kind of confusing that they have such similar names

[Aaron Liu]

On one side is just Chapter2.Nat.zero and on the other side is @repro.PeanoAxioms.zero repro.Chapter2.Nat

[Rado Kirov]

wow, great find. Ultimately all these definitions boil down to the same inductive type constructor, but Lean keeps them unexpanded until they are simplified. Down to one sorry left!

[Rado Kirov]

:partying_face: With that observation, I finally finished the proof - https://github.com/rkirov/analysis/blob/4683dde93a979ea428cafd6954155aab7fafa9c6/analysis/Analysis/Section_2_epilogue.lean#L271-L277. Thanks for the help!

Two final q:

• what does the @ mean when you write @repro.PeanoAxioms.zero?
• to get around all the indirection confusion I replaced rw [h] with have h2 := h; simp at h; rw [h2]. It made sure everything is expressed in "lowest terms", is this a common way to some similar problems? Is there anything more ideomatic?

[Peter Hansen]

Rado Kirov said:

Thanks for sharing. It looks like that conversation predated the skeleton code provided by Tao, so hard for me to see how to modify my problem locally.

Ah, I had missed the part that you were working specifically from a setup made by Tao. The solution I shared follows the path hinted by Tao in the setup for Exercise 3.5.12 in the book. But I think I can see why he did not recommend this path to be taken for formalization in Lean. Is takes lot of lines of code to show recursion from induction this way. But it has the slight charm of being proven completely independent from the built-in naturals.

[Ruben Van de Velde]

@ makes implicit arguments explicit

[Rado Kirov]

ah of course, I thought for a second it has to do something with the namespace or type-class resolution.

[Dan Abramov]

I went with a similar solution but via Mathlib naturals: https://github.com/gaearon/analysis-solutions/blob/c2060150c1d145de27ded493ff3c5aadd748a7c6/analysis/Analysis/Section_2_epilogue.lean#L222

[Rado Kirov]

Nice, I did Chapter2.Nats' because originally thought I can use theorem Nat.recurse_uniq from 2.1 directly, but actually end up not using it and Mathlib.Nats are probably easier.

[Notification Bot]

This topic was moved here from #new members > Help with solving Tao's Analysis Chapter 2 epilogue problem by Johan Commelin.