Prove recursive function exists using only `nat

I'm trying to prove the following in Coq:

∀ B: Type, ∀ a: B, ∀ b: nat -> B -> B, ∃ f: nat -> B, f 0 = a ∧ ∀ n: nat, f (S n) = b n (f n).

Which implies that a fairly general class of recursive functions exist. I know that I can construct that function using Fixpoint items or fix expressions, but I want to not use it, and instead use nat_ind defined with this type:

∀ P: nat → Prop, P 0 → (∀ n: nat, P n → P (S n)) → ∀ n: nat, P n

I believe this is possible since nat_ind behaves like a recursion combinator. But I didn't figured it out how to prove it. The problem is that the induction variable is inside of ∃ f guard, and I don't have access to it. I'm able to prove something like this:

∀ B: Type, ∀ a: B, ∀ b: nat -> B -> B, ∀ m: nat,
  ∃ f: nat -> B, f 0 = a ∧ ∀ n: nat, n < m -> f (S n) = b n (f n)

But it doesn't help in proving the original one I think.

Is it possible to prove the original one without using fix directly? I'm ok with using double negation and other well-known axioms if needed. Using nat_rec and nat_rect is also fine, but only as an opaque axiom. Precisely, using those are fine:

Axiom nat_rec2: ∀ P : nat → Set, P 0 → (∀ n : nat, P n → P (S n)) → ∀ n : nat, P n.
Axiom nat_rect2: ∀ P : nat → Type, P 0 → (∀ n : nat, P n → P (S n)) → ∀ n : nat, P n.

CodePudding user response：

The problem seems to be to obtain recursion from the following axiomatization of nat:

Parameter nat : Type.
Parameter O : nat.
Parameter S : nat -> nat.
Parameter disjoint_O_S : forall n, O <> S n.
Parameter injective_S : forall n n', S n = S n' -> n = n'.
Parameter nat_rect : forall P: nat -> Type, P O -> (forall n: nat, P n -> P (S n)) -> forall n : nat, P n.

Where the main issue is that the nat_rect axiom has no computational behavior, so although we might define a recursor B -> (nat -> B -> B) -> nat -> B as nat_rect (fun _ => B), we can't prove anything about it.

The solution is to first encode the graph of the desired recursive function f as a relation, and then use nat_rect to produce a dependent pair, of a value that is going to be f n with evidence that that value is in the graph of f.

Section Rec.

Context (B : Type) (a : B) (b : nat -> B -> B).

Inductive graph : nat -> B -> Prop :=
| recO : graph O a
| recS n y : graph n y -> graph (S n) (b n y)
.

Lemma graph_fun : forall n, { y | forall y', y = y' <-> graph n y' }.
Proof.
  induction n as [ | n IH ] using nat_rect.
  - exists a; split.
      intros <-. constructor.
      inversion 1; [ reflexivity | ]. contradiction (disjoint_O_S n); auto.
  - destruct IH as [y IH]. exists (b n y); split.
      intros <-. constructor. apply IH. auto.
      inversion 1; subst. contradiction (disjoint_O_S n); auto.
      apply injective_S in H0. subst.
      apply IH in H1. subst; auto.
Qed.

Theorem nat_rec : exists (f : nat -> B), f O = a /\ forall n, f (S n) = b n (f n).
Proof.
  exists (fun n => proj1_sig (graph_fun n)). split.
  - apply (proj2_sig (graph_fun O)). constructor.
  - intros n. apply (proj2_sig (graph_fun (S n))).
    constructor. apply (proj2_sig (graph_fun n)).
    reflexivity.
Qed.

End Rec.

If you have the Prop inductor nat_ind instead of nat_rect, that same technique can be adapted by also assuming the axiom constructive_indefinite_description (which actually lets you reconstruct nat_rect, but here you can more simply apply it at the beginning of graph_fun):

From Coq Require Import IndefiniteDescription.

About constructive_indefinite_description.
(*
constructive_indefinite_description :
  forall (A : Type) (P : A->Prop),
  (exists x, P x) -> { x : A | P x }.
*)