我有以下两个定义，导致两个不同的错误消息。第一个定义由于严格的正性而被拒绝，第二个定义由于宇宙不一致而被拒绝。

(* non-strictly positive *)
Inductive SwitchNSP (A : Type) : Type :=
| switchNSP : SwitchNSP bool -> SwitchNSP A.

Fail Inductive UseSwitchNSP :=
| useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP.

(* universe inconsistency *)
Inductive SwitchNSPI : Type -> Type :=
| switchNSPI : forall A, SwitchNSPI bool -> SwitchNSPI A.

Fail Inductive UseSwitchNSPI :=
| useSwitchNSPI : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI.

在gitter上聊天显示，首先检查了Universe（内部）一致性，即第一个定义遵循此检查，但是由于严格的正性问题而失败。

据我了解严格的积极性限制，如果Coq允许非严格的积极性数据类型定义，我可以不使用而构造非终止函数fix（这很糟糕）。

为了使之更加混乱，第一个定义在Agda中被接受，第二个定义给出了严格的正错误。

data Bool : Set where
  True : Bool
  False : Bool …

有谁知道以下任何例子？

1. 关于证明助理(例如Coq)中正则表达式(可能通过反向引用扩展)的证据开发.
2. 关于正则表达式的依赖类型语言(例如Agda)中的程序.

是.v用于验证？验证？vamanos？

为什么不使用.coq扩展名？

正如标题所说,Coq可以用作模型检查器吗？我可以将模型检查与Coq证明混合使用吗？这通常吗？谷歌谈到"微积分",有没有人有这种或类似的经验？建议以这种方式使用Coq,还是应该寻找其他工具？

我无法加载CoqIde中相同文件夹中的模块.

我试图从软件基金会加载来源,我跑在包含SF sources文件夹coqide coqide或coqide ./,然后打开并运行该文件后,我得到这个错误:

Error: Cannot find library Poly in loadpath

在这一行:

Require Export Poly.

并且对于其他所有require命令都是一样的.

那么你们如何将程序从SF加载到coqide？

假设我已经在coq中证明了一些定理,后来我想在另一个定理的证明中作为假设引入它.有简洁的方法吗？

当我想要通过案例进行证明时,通常会出现对此的需求.而且我发现这样做的一种方法是对assert定理的陈述,然后立即证明它,但这看起来有点麻烦.例如,我倾向于写下这样的东西:

Require Import Arith.EqNat.

Definition Decide P := P \/ ~P.

Theorem decide_eq_nat: forall x y: nat, Decide (x = y).
Proof.
  intros x y. remember (beq_nat x y) as b eqn:E. destruct b.
    left. apply beq_nat_eq. assumption.
    right. apply beq_nat_false. symmetry. assumption. Qed.

Theorem silly: forall x y: nat, x = y \/ x <> y.
Proof.
  intros x y.
  assert (Decide (x = y)) as [E|N] by apply decide_eq_nat.
    left. assumption.
    right. assumption. Qed.

但有没有比输入整个 …

我看到了几个不同的研究小组,至少有一本关于使用Coq设计认证程序的书.关于认证计划的定义是什么,是否有共识？从我所知道的,它真正意味着该程序被证明是完整的并且类型正确.现在,程序的类型可能是非常奇特的东西,例如列表,其中包含非空的证明,排序,所有元素> = 5等等.但是,最终,是一个经过认证的程序,Coq显示的是总计和类型安全的程序,所有有趣的问题归结为最终类型中包含的内容？

编辑1

根据wjedynak的回答,我看了Xavier Leroy的论文"现实编译器的形式验证",它在下面的答案中有所联系.我认为这包含一些很好的信息,但我认为这个研究序列中的信息量更多的信息可以在Sandrine Blazy和Xavier Leroy 的C语言的Clight子集的机械化语义学中找到.这是"形式验证"论文添加优化的语言.在其中,Blazy和Leroy介绍了Clight语言的语法和语义,然后在第5节讨论了这些语义的验证.在第5节中,列出了用于验证编译器的不同策略,这在某种意义上提供了概述创建认证计划的不同策略.这些是:

1. 手动评论
2. 证明语义的属性
3. 验证翻译
4. 测试可执行语义
5. 与备用语义的等价性

在任何情况下,可能会添加一些点,我当然希望听到更多.

回到我关于认证程序定义的原始问题,对我来说仍然有点不清楚.Wjedynak提供了一个答案,但Leroy的工作实际上涉及在Coq中创建编译器,然后在某种意义上证明它.从理论上讲,它现在可以证明C程序的内容,因为我们现在可以进行C-> Coq->证明.从这个意义上讲,似乎就是我们可以做到这一点

1. 用X语言编写程序
2. Coq中的步骤1或其他证明助手工具的程序模型的形式.这可能涉及在Coq中创建编程语言的模型,或者它可能涉及直接创建程序模型(即在Coq中重写程序本身).
3. 证明一些关于模型的属性.也许这是关于价值观的证明.也许它是语句等价性的证明(例如3 = 1 + 2或f(x,y)= f(y,x)之类的东西.)
4. 然后,根据这些证明,调用原始程序认证.

或者,我们可以在校对助手工具中创建程序规范,然后证明规范的属性,而不是程序本身.

无论如何,如果有人有这些定义,我仍然有兴趣听取其他定义.

Coq 常见问题解答说功能扩展性与预测性一致Set.从这一点来看,我不完全清楚它是否与不可预测的一致Set(或者在这种情况下可能是一致性).

这些程序的设计目标是什么？每个程序提供的是另一个程序？此外,两个系统是否一致,而且,它们是否基于一些基础数学理论？

我关心的两件事:

1. 易于安装
2. 简单易学

我在搜索,我读到的内容似乎非常两极分化,我想知道他们与最客观(人性)可能的观点的区别.

我在JavaScript中实现Algorithm W(Hindley-Milner类型系统):

实现上述规则的功能是typecheck,它具有以下签名:

typecheck :: (Context, Expr) -> Monotype

它的定义如下:

function typecheck(context, expression) {
    switch (expression.type) {
    case "Var":
        var name = expression.name;
        var type = context[name];
        return inst(type);
    case "App":
        var fun = typecheck(context, expression.fun);
        var dom = typecheck(context, expression.arg);
        var cod = new Variable;
        unify(fun, abs(dom, cod));
        return cod;
    case "Abs":
        var param = expression.param;
        var env   = Object.create(context);
        var dom   = env[param] = new Variable;
        var cod   = typecheck(env, expression.result);
        return …