3

我试图将一些直觉主义的概念形式化。其中之一是连续性原则。在 Coq 中，我将其定义为：

(* Infinite sequences *)
Definition N := nat -> nat.

(* The first n elements of a and b coincide. *)
Definition con (a b : N) n := forall i, i < n -> a i = b i.

(* Brouwers Continuity Principle *)
Axiom BCP :
  forall (R : N -> nat -> Prop),
  (forall a, exists n, R a n) ->
  (forall a, exists m n, forall b, con a b m -> R b n).

我想将其概括为所谓的点差。传播是贝尔空间的一个子集，可以被认为是一棵只有无限分支的树。判定器 o（称为扩展定律）采用有限的起始序列，如果它应该在扩展中，则返回 0。当序列 s 在展开中时，至少一个扩展 n :: s 也必须在展开中。必须接受空序列，以便传播被居住。我将其定义如下：

(* Spread law *)
Definition Spr_Law (o : list nat -> nat) :=
  o [] = 0 /\ forall s, o s = 0 <-> exists n, o (n :: s) = 0.

证明连续性原理可以推广到任意扩展的一种方法是定义一个函数，该函数将 N “收回”到由此类决策器 o 定义的扩展上。这就是我卡住的地方，因为我对 Coq 的了解还不够，无法很好地定义这一点。首先，我从课程笔记中插入了这个定义的图片。 非正式定义

问题是这个定义包括一个“最小的 m 使得 o 接受 m :: s”。这不是一般的终止程序，我不知道如何使用Function来证明此搜索将出于我们的目的而终止（它会因为传播法必须接受至少一个扩展）。

我发现Coq.Logic.ConstructiveEpsilon当我有一个存在声明时，我可以使用图书馆来获得证人。我可以将至少存在一个扩展的条件传递给该函数。基于此，我创建了以下代码（这只是定义的第一部分，它将有限序列映射到扩展上）：

Definition find_extension o s (w : exists n, o (n :: s) = 0) : nat :=
  constructive_ground_epsilon_nat (fun n => o (n :: s) = 0) (decider_dec o s) w.

(* Compute retraction for finite start sequences. *)
Fixpoint rho o (w : forall s, o s = 0 -> exists n, o (n :: s) = 0)
  (s : list nat) : list nat :=
  match s with
  | [] => []
  | n :: s => let t := rho o w s in
    if o (n :: t) =? 0
    then n :: t
    else (find_extension o t (w t {?????})) :: t
  end.

现在我遇到了真正的问题。这{?????}部分是我需要插入证明的地方o t = 0。这成立，因为 rho 只返回决策者 o 接受的序列。也许我可以让 rho 返回一个包含新序列的元组以及该序列被接受的证明（这样我可以w在递归后将其输入），但我不知道如何。请注意，这对于 else 分支来说尤其棘手，因为该值被接受的证明是有效的，因为见证是有效的。

当然，也欢迎定义点差的替代想法。我确实觉得这是可以实现的（据我所知，没有逻辑上的不一致）。

4

1 回答 1

2

我似乎想到了什么：

(* Only sequences that are accepted by o *)
Inductive spr (o : decider) :=
  | spr_s s : o s = 0 -> spr o.

(* Return smallest n such that o accepts n :: s. *)
Definition find_extension o s (witness : exists n, o (n :: s) = 0) : spr o :=
  let P := (fun n => o (n :: s) = 0) in
  let D := (decider_dec o s) in
  spr_s o
    ((constructive_ground_epsilon_nat P D witness) :: s)
    (constructive_ground_epsilon_spec_nat P D witness).

(*
To generalize BCP to spreads we first define a function that retracts the Baire
space onto an arbitrary spread given its spread law. This happens in two steps.
*)

(* Compute retraction for finite start sequences. *)
Fixpoint rho o
  (Hnil : o [] = 0)
  (Hcons : forall s, o s = 0 -> exists n, o (n :: s) = 0)
  (s : list nat) : spr o :=
  match s with
  | [] => spr_s o [] Hnil
  | n :: s =>
    match rho o Hnil Hcons s with
    | spr_s _ t Ht =>
      match eq_dec (o (n :: t)) 0 with
      | left Heq  => spr_s o (n :: t) Heq
      | right  _  => find_extension o t (Hcons t Ht)
      end
    end
  end.

(* Retraction of N onto F_o *)
Definition retract o
  (Hnil : o [] = 0)
  (Hcons : forall s, o s = 0 -> exists n, o (n :: s) = 0)
  : N -> N :=
  fun a => fun n =>
    match rho o Hnil Hcons (get (n + 1) a) with
    | spr_s _ [] _ => 0 (* not reachable *)
    | spr_s _ (rho_n :: _) _ => rho_n
    end.
于 2019-12-19T13:58:03.153 回答