仅使用 `nat_ind` 证明递归函数存在

Question

我试图在 Coq 中证明以下内容：

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

这意味着存在相当通用的 class 递归函数。我知道我可以使用 Fixpoint 项或 fix 表达式构造该函数，但我不想使用它，而是使用用此类型定义的 nat_ind：

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

我相信这是可能的，因为 nat_ind 的行为类似于递归组合器。但是我没有想出如何证明它。问题是归纳变量在 ∃ f 守卫内部，我无权访问它。我能够证明这样的事情：

∀ 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)

但我认为这无助于证明原作。

不直接使用fix是否可以证明原件？如果需要，我可以使用双重否定和其他众所周知的公理。使用 nat_rec 和 nat_rect 也很好，但只能作为一个不透明的公理。准确地说，使用这些很好：

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.

Answer 1

问题似乎是从 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.

主要问题是 nat_rect 公理没有计算行为，因此尽管我们可以将递归 B -> (nat -> B -> B) -> nat -> B 定义为 nat_rect (fun _ => B)，但我们无法证明任何相关信息.

解决方案是首先将所需递归函数 f 的图形编码为关系，然后使用 nat_rect 生成依赖对，其值将是 f n 有证据表明该值在 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.

如果你有 Prop 电感器 nat_ind 而不是 nat_rect，同样的技术可以通过假设公理 constructive_indefinite_description （实际上可以让你重建nat_rect，但这里你可以更简单地在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 }.
*)

仅使用 `nat_ind` 证明递归函数存在

Prove recursive function exists using only `nat_ind`

recursion

coq

induction