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.
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 }.
*)