我試圖在 Coq 中證明以下內容：
? B: Type, ? a: B, ? b: nat -> B -> B, ? f: nat -> B, f 0 = a ∧ ? n: nat, f (S n) = b n (f n).
這意味著存在一類相當普遍的遞回函式。我知道我可以使用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_recandnat_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.
uj5u.com熱心網友回復：
問題似乎是從 的以下公理化中獲得遞回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 }.
*)
轉載請註明出處，本文鏈接：https://www.uj5u.com/yidong/475119.html
下一篇：Java中 =和=1 的區別