gpt4 book ai didi

coq - 在 Coq 的函数定义中使用证明和见证结构

转载 作者:行者123 更新时间:2023-12-04 15:37:27 25 4
gpt4 key购买 nike

我正在尝试将一些直觉主义的概念形式化。其中之一是连续性原则。在 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 的了解还不够多,无法很好地定义它。首先,我从类(class)笔记中插入了一张关于这个定义的图片。 informal definition

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

我发现当我有一个 exists 语句时,我可以使用 Coq.Logic.ConstructiveEpsilon 库来获取 witness。我可以传递函数至少存在一个扩展的条件。基于此我创建了以下代码(这只是定义的第一部分,它将有限序列映射到分布上):

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 分支来说尤其棘手,因为这个值被接受的证据是有效的,因为见证是有效的。

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

最佳答案

我好像明白了什么:

(* 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.

关于coq - 在 Coq 的函数定义中使用证明和见证结构,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59313988/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com