这个问题是参考或解释的请求.主要思想是:如果我从Coq的标准库中添加每个公理怎么办？它会引起矛盾还是相互调整好？除了标准的Coq库之外,还有哪些关于Coq的可靠信息来源.(我看过九十年代,八十年代的一堆论文.显然有很多类型理论的变体.哪一个适用于当代的Coq？或者我应该认为"所有已知的东西都可以在https://coq.inria.fr找到/ refman /,在https://sympa.inria.fr/sympa/arc/coq-club/1993-12/和标准库中.")
(A)您是否知道纸张或其他来源,证明某些公理可以正确添加到Coq？这里适当地意味着扩展系统将是以前OR的保守扩展将被认为是安全加强.
(B)就个人而言,我对这些公理感兴趣:
0)ex2sig(它是否一致？)
Axiom ex2sig : forall (A:Type) (P:A->Prop), @ex A P -> @sig A P.
1)LEM
2)功能扩展性
Axiom functional_extensionality_dep : forall {A} {B : A -> Type},
forall (f g : forall x : A, B x),
(forall x, f x = g x) -> f = g.
3)选择
Theorem choice :
forall (A B : Type) (R : A->B->Prop),
(forall x : A, exists y : B, R x …我想查看我的证明中使用的所有公理。获取此类信息的最简单方法是什么？我将使用哪些命令、脚本或工具？我对所有公理或所有使用过的公理感兴趣。
我定义了一种 s 表达式及其打印函数。
Inductive sexp : Set :=
K : string -> (list sexp) -> sexp
.
Fixpoint sexpprint (s:sexp) : list string :=
match s with
K n l => ["("%string]++[n]++(concat (map sexpprint l))++[")"%string]
end.
（是的，我知道它可以只是字符串，而不是字符串列表，但是 Coq 有少量用于处理字符串的定理，但有大量用于处理列表的定理。）
(* more usual function
Fixpoint sexpprint (s:sexp) :string :=
match s with
K n l => ("(":string)++n++(String.concat "" (map sexpprint l))++")"
end.
*)
我一直在试图证明这个定理：
Theorem sexpprint_inj s1 s2:
sexpprint s1 = sexpprint s2 -> s1 = s2.
也许有一些来源可以帮助我计划定理的证明？（书籍/文章/代码）如何证明？（也许我需要一种特殊的归纳原理，你能表述一下它的说法吗？）
我还定义了深度函数，它可能会有所帮助
Fixpoint depth …我想在Coq中使用标准符号,例如"x∈{x}".但有问题:
1)Curly braces在Coq中有特殊含义,因此会发生以下情况:
Notation " x ? y " :=(tin x y) (at level 50).
Notation " { x } ":=(Sing x).
Check fun x => (x ? { x }).
(*error: Unknown interpretation for notation "_ ? { _ }". *)
如何正确定义这种表示法？
2)如果第一个问题无法解决,还有另一个问题.(这里我决定在符号中使用附加符号'''.)
Notation " { x }` ":=(Sing x).
Check fun x => (x ? { x }`).
(* fun x : Ens => x ? {x }` *)
现在我应该
a)在第一个大括号之后添加一个空格或
b)删除最后一个x字母后的无意空格.
我该怎么做这些动作？
即使在非常简单的情况下，我也要等到Coq完成其计算。
我了解“异步和并行的证明处理”，但是我想我的代码具有固有的弊端，因此我想对证明/证明样式的最佳实践获得一些参考或建议。例如：
尝试使用定义而不是定理，
使用编译器。使用并行处理。使用更好的硬件。
不要使用占位符，填写每个参数，例如（@functionname var1 ... varn）
用分号（;）代替句点（。）
使用“部分”中的“定义”代替“ set（f：= term）”要快得多。在证明中。（可能是因为每个“设置”都有额外的打印时间。甚至要检查是否为空。）
如何加快Coq？（如果我在上面的项目中有错误，请说。它们是根据我的实践得出的。）
什么是计算的最关键阶段以及如何使用它们？