Help with formalizing recursive definitions from Tao's A1

Stream: new members

[Peter Hansen]

I'm working on formalizing Proposition 2.1.16 (Recursive definitions) from Tao's Analysis I in Lean. The proposition states:

Proposition 2.1.16 (Recursive definitions).
Suppose for each natural number $n$, we have some function $f_n: \mathbf{N} \rightarrow \mathbf{N}$ from the natural numbers to the natural numbers. Let $c$ be a natural number. Then we can assign a unique natural number $a_n$ to each natural number $n$, such that $a_0=c$ and $a_{n++}=f_n\left(a_n\right)$ for each natural number $n$.

I've created a TaoNat class to capture Tao's axioms and proved the existence of recursive sequences:

import Mathlib.Tactic
import Mathlib.Logic.Basic

class TaoNat (N : Type u) where
  -- Axiom 2.1: Zero exists
  zero : N

  -- Axiom 2.2: Successor function
  succ : N → N

  -- Axiom 2.3: Zero is not a successor
  zero_not_succ' : ∀ n : N, succ n ≠ zero

  -- Axiom 2.4: Successor is injective
  succ_injective' : ∀ {n m : N}, succ n = succ m → n = m

  -- Axiom 2.5: Induction principle
  induction_principle' : ∀ (P : N → Prop),
    P zero ∧
    (∀ n : N, P n → P (succ n)) →
    ∀ n : N, P n

postfix:max "⁺⁺" => TaoNat.succ

instance {n : ℕ} [TaoNat ℕ₀] : OfNat ℕ₀ n where
  ofNat := by
    induction n with
    | zero => exact TaoNat.zero
    | succ _ ih => exact ih⁺⁺

namespace TaoNat

variable {ℕ₀ : Type*} [TaoNat ℕ₀] (n : ℕ₀)

theorem induction_principle  {P : ℕ₀ → Prop} (H : P 0 ∧ ∀ n : ℕ₀, P n → P n⁺⁺) (m : ℕ₀) : P m := ‹TaoNat ℕ₀›.induction_principle' P H m
alias Axiom₅ := induction_principle

@[elab_as_elim]
protected theorem induction {N : Type u} [TaoNat N] {motive : N → Prop}
  (zero : motive 0)
  (Succ : ∀ (n) (_ : motive n), motive n⁺⁺) : ∀ n, motive n :=
  λ n ↦ induction_principle ⟨zero, λ _ ↦ Succ _⟩ n

variable {X : Sort*} {ℕ₀ : Type u} [TaoNat ℕ₀] (zero : X) (motive : ℕ₀ → X → X)

theorem Exist_Rec_fn : ∃! (An : ℕ₀ → X), (An 0 = zero) ∧ (∀ n, An n⁺⁺ = motive n (An n)) := sorry

protected noncomputable def rec_fn : ℕ₀ → X := Classical.choose (Exist_Rec_fn zero motive)

/-- The initial value of the value sequence -/
theorem rec_fn_zero : TaoNat.rec_fn zero motive 0 = zero :=
  (Classical.choose_spec (Exist_Rec_fn zero motive)).1.1

/-- The recursive step for the value sequence -/
theorem rec_fn_succ (n : ℕ₀) :
    TaoNat.rec_fn zero motive n⁺⁺ = motive n (TaoNat.rec_fn zero motive n) :=
    (Classical.choose_spec (Exist_Rec_fn zero motive)).1.2 _

/-- The value sequence is unique -/
theorem rec_fn_unique (h : ℕ₀ → X)
    (h₁ : h 0 = zero) (h₂ : ∀ n, h n⁺⁺ = motive n (h n)) :
    h = TaoNat.rec_fn zero motive := (Classical.choose_spec (Exist_Rec_fn zero motive)).2 _ ⟨h₁, h₂⟩

end TaoNat

Questions:

1. Does my ´TaoNat class´ faithfully represent Tao's axioms? Are there better ways to capture these axioms in Lean?

2. How can I make this result more practical to use? Currently, I'm using Classical.choose which makes the function noncomputable. Is there a better way to define recursive sequences from an axiomatic approach?

Any input and suggestions would be appreciated.

[Julian Berman]

I was waiting for someone else who knows more to give you a tip, but since no one has yet -- the small amount I know is that some of what you have in TaoNat will butt up against Lean's type theory.

(PS why did you make TaoNat a typeclass?)

[Julian Berman]

By which I mean, I think the two axioms at the end there are "not needed" and you can somehow even prove them already -- because when Lean gives you a new inductive type it generates some stuff "automatically", one of which is this thing called a recursor which you find in ... .recOn I think.

[Julian Berman]

In particular if you look at Lean's own definition of Nat you'll see it doesn't have some of the Peano axioms -- there's a post by Kevin on the Xena project blog which I think explains some of this, I'll try to find it -- but basically when you have an inductive type with separate constructors you already get "no succ is equal to zero", that' a property of any inductive type that unique constructors give you new terms.

[Julian Berman]

Not sure if you know any of the above, but I think it seems relevant to your question.

[Julian Berman]

Maybe the post I am recalling is https://xenaproject.wordpress.com/2021/04/03/induction-and-inductive-types/

[Kevin Buzzard]

Isn't the point here that we're not using the inductive keyword and so we have to put some axioms in? This is how Peano did it originally (although he started at 1). I like Lean's approach (ie the CIC approach) much better. Make recursion an axiom and you can prove all three of the axioms in the definition above.

[Kevin Buzzard]

The answer to "can I make it computable" is almost certainly "no" because at some point you have to move from the Prop world into the Type world and this is exactly what choice does for you.

[Kevin Buzzard]

But my answers to the original questions are: 1. yes I think it does, although of course it doesn't provide you with a model for the axioms (you could make an instance : TaoNat ℕ := sorry to prove that your axioms are consistent, for example). 2. you're never going to get a computable Nat.rec out of this set-up. The best way is to make recursion an axiom.

Code style comment: we don't use \lam usually, it's fun in Lean 4.

[Kevin Buzzard]

  induction_principle' : ∀ (P : N → Prop),
    P zero →
    (∀ n : N, P n → P (succ n)) →
    ∀ n : N, P n

would be more idiomatic in a functional language (avoid the \and because you don't need it)

[Kevin Buzzard]

I don't know how to fill in the sorry because when I realised that it was much much easier to go the other way around I just adopted that approach (although I'm aware there's a proof in Tao's book, I just never read it). In the Natural Number Game I prove zero_not_succ' and succ_injective' using recursion rather than the other way around.

[Peter Hansen]

Thanks for the detailed responses!

I get that using inductive would be more practical (and give us computability), but I wanted to stick close to Tao's axiomatic approach. The book presents these as axioms and leaves deriving the recursion principle as an exercise - there's even a challenge version that doesn't use ordering.

I went with a typeclass because I thought of these axioms as defining what it means to be "natural numbers" - kind of like an interface that different implementations (like ℕ) could satisfy. This way, proofs would work with any implementation that meets these requirements. I kept the ∧ structure in the induction principle to match Tao's presentation, even though it might not be the most Lean-like way to write it.

I guess this axiomatic approach means giving up computability (because of classical choice), but for what I'm trying to do - following Tao's argument - I'm okay with that trade-off.

[Kevin Buzzard]

I would say that P -> Q -> R reads "If P, and if Q, then R", so I would dispute your insistence on ∧ and you'll find it a mild pain to work with later, but only a mild pain. The point about the inductive def

inductive Nat0
| zero : Nat0
| succ : Nat0 -> Nat0

is that it is exactly the inductive definition of the naturals: it says "zero is a natural, the successor of a natural is a natural, and that's it" (i.e. definition ends there, i.e. the only way to make naturals is zero and succ, i.e. if you can do something for zero and for succ then you've done it for all naturals, i.e. the principles of induction and recursion). But you seem to understand well what you're doing and how it differs. I think it would be good to try and fill in that sorry, you can check that Tao is right. Within the context of type theory it seems strange to deduce recursion from induction but you seem to be well aware of what you're getting into.

[Kevin Buzzard]

One thing going for the Lean approach is that you assume just one axiom (recursion) and now it's quite fun to deduce all the others (for example you use recursion to define a function pred with pred 0 = 37 and pred (n+1) = n, and then prove pred (succ n) = n (by definition) and deduce that succ is injective from that). Proving recursion from induction will be a much harder challenge, I would imagine. Keep us posted!

[Mario Carneiro]

actually it's not exactly one axiom, because you also need the computation rules for the recursor in order to deduce things like zero != succ n from the recursor

[Daniel Weber]

Kevin Buzzard said:

The answer to "can I make it noncomputable" is almost certainly "no" because at some point you have to move from the Prop world into the Type world and this is exactly what choice does for you.

If we can compute the natural N -> Nat function then we can do whatever we want with it (Nat -> N is easy). If N doesn't have decidable equality then this function isn't computable, but if it does then it can be computed with docs#Nat.find

[Kevin Buzzard]

I should think that defining TaoNat -> Nat is as hard as constructing the general recursor (it's the universal instance).

[Peter Hansen]

Kevin Buzzard said:

I would say that P -> Q -> R reads "If P, and if Q, then R", so I would dispute your insistence on ∧ and you'll find it a mild pain to work with later, but only a mild pain.

Yeah, P -> Q -> R does seem nicer to apply than P ∧ Q -> R. That also why derived a version with the ´@[elab_as_elim]´ attribute. I was just afraid that it was somehow dishonest and somehow misrepresentative.

And luckily, Tao was right. It took a couple of hundreds lines of code to prove the existence of the claimed sequence doing Tao's "challenge" version, where we do not rely on any ordering.

But the more I think about, I am inclined to abandon my TaoNat class going forward with the book and just define them inductively. I am not sure which approach I find most intuitive. As you explained, it is appealing to basically say - everything there is to say about the naturals can be said in terms of zero and succ. But guess I have not yet totally convinced myself how the remaining axioms follow from the recursion principle alone. I guess I better finally get around to playing the Natural Numbers Game.

Daniel Weber said:

Kevin Buzzard said:

The answer to "can I make it noncomputable" is almost certainly "no" because at some point you have to move from the Prop world into the Type world and this is exactly what choice does for you.

If we can compute the natural N -> Nat function then we can do whatever we want with it (Nat -> N is easy). If N doesn't have decidable equality then this function isn't computable, but if it does then it can be computed with docs#Nat.find

So TaoNat ℕ := could be made computable? Or am I misunderstanding something?

[Mario Carneiro]

There is no interesting computational content in TaoNat ℕ so yes it could be made computable