Existence of a recursor

Stream: maths

[Patrick Johnson]

What is the best way to prove this?

example {α nat : Type} {zero : nat} {succ : nat → nat}
  (h₁ : ∀ (n : nat), zero ≠ succ n)
  (h₂ : ∀ (m n : nat), succ m = succ n → m = n)
  (h₃ : ∀ (P : nat → Prop) (n : nat),
    P zero → (∀ (n : nat), P n → P (succ n)) → P n) :
  ∃ (rec : α → (nat → α → α) → nat → α), ∀ (z : α) (f : nat → α → α),
    rec z f zero = z ∧ ∀ (n : nat), rec z f (succ n) = f n (rec z f n) :=
begin
  sorry
end

I managed to prove this in another theorem prover, but the proof is very long. The proof goes like this: first define m ≤ n to be true iff there exists a function f : nat → nat such that f zero = m, f (succ k) = succ (f k) for all k, and there exists x such that f x = n. We define m < n as m ≤ n ∧ m ≠ n. Then we prove many useful theorems about those two relations. After that, we prove that for each N : nat there exists function rec' such that rec' N z f zero = z and for all n < N, rec' N z f (succ n) = f z (rec' N z f n). Then we prove that for any N₁ N₂ n : nat, if n < N₁ and n < N₂, then rec' N₁ z f n = rec' N₂ z f n. After that, we define rec z f n as rec' (succ n) z f n and finally prove the theorem.

Is there an easier way?

[Junyan Xu]

Using zero, succ, h₁, h₂, h₃ you should be able to construct a docs#equiv with ℕ, and you can just use nat.rec. If you don't want to use the inductive type ℕ, I think you can take rec z f to be the "union" of all partial functions g satisfying g zero = z ∧ ∀ (n : nat), g (succ n) = f n (g n); you won't get rid of inductive types completely (∃, ∧ and subtypes are all inductive types in Lean), but you could avoid the more "powerful" inductive types like ℕ.