在Coq函数定义内使用证明和见证结构

Question

我正在尝试形式化一些直觉主义的观念。其中之一是连续性原则。在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).

我想将其概括为所谓的点差。散布是Baire空间的一个子集，可以将其视为仅具有无限分支的树。决策者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分支尤其棘手，因为接受此值的证据成立，因为见证人有效。

当然，也可以使用其他定义点差的想法。我确实认为这是可以实现的（据我所知，没有逻辑上的矛盾）。

我正在尝试形式化一些直觉主义的观念。其中之一是连续性原则。在Coq中，我将其定义为：（*无限序列*）定义N：= nat-> nat。 （*前n个...

Answer 1

我似乎已经弄明白了：