问题标签 [theorem-proving]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
logic - Coq 中的证明论证
我试图在 Coq 中定义一个弱指定类型的函数。具体来说，我有一个由一组递归构造函数归纳定义的类型，并且我想定义一个函数，该函数仅在使用其中的一个子集构造参数时才定义。
更具体地说，我有以下类型定义：
现在，我有一个仅适用于地面案例的功能。（以下定义显然不起作用，但旨在表明我的意图。）
理想情况下，我想说明我的参数 x 是使用通用类型构造函数的子集构造的，在本例中为 Example_cons0。我认为我可以通过定义一个陈述这一事实的谓词并将谓词的证明作为参数传递来做到这一点。例如：
然后（按照 Robin Green 的建议）类似，
不幸的是，我不确定我将如何去做这些。我什至不确定这是在弱指定类型上定义受限函数的正确方法。
任何指导、提示或建议将不胜感激！- 李
更新：
按照 jozefg 的建议，示例函数可以定义为：
有关详细信息，请参阅他的评论。可以使用以下语法评估此函数，这也演示了证明术语在 Coq 中的表示方式：
lazy-evaluation - 惰性评估正确性和整体性 (Coq)
正如标题所示，我的问题涉及证明 Coq 中算术表达式的惰性求值的正确性和完整性。我想证明的定理共有三个：
计算只给出规范表达式作为结果
Theorem Only_canonical_results: (forall xy: Aexp, Comp xy -> Canonical y)。
正确性：计算关系保留表达式的表示
Theorem correct_wrt_semantics: (forall xy: Aexp, Comp xy -> IN (denotation x) (denotation y))。
每个输入都会导致一些结果。
Theorem Comp_is_total: (forall x:Aexp, (Sigma Aexp (fun y => prod (Comp xy) (Canonical y))))。
必要的定义可以在下面附加的代码中找到。我应该明确表示我是 Coq 的新手；更有经验的用户可能会立即注意到。可以肯定的是，我所写的大部分或什至所有背景材料都可以在标准库中找到。但是，话又说回来，如果我确切地知道从标准库中导入什么来证明所需的结果，我很可能不会在这里打扰你。这就是为什么我将我目前拥有的材料提交给你，希望有热心的人可以帮助我。谢谢！
isabelle - 伊莎贝尔：用大锤得到三个不同的结果，似乎是相同的引理
你需要这个来获得我的进口：
我有三个几乎相同的引理。
版本1：
版本2：
版本 3：
这是运行大锤的结果，仅显示e定理证明器的结果；它显示了三个完全不同的结果：
问： 为什么会这样？大锤是不确定的吗？还是伊莎贝尔的三个版本不同，所以大锤得到三个不同的输入？
geometry - 支持正方形交集的几何定理证明器
我试图自动证明/反驳一些与正方形相关的几何定理，例如“对于每 3 个 7 个不相交正方形的集合，可以从每个集合中选择 1 个正方形，使得 3 个代表是内部不相交的？”。
我尝试使用OpenGeoProver并得出以下正方形描述：
这就是我卡住的地方：如何定义简单的语句“正方形 A 和正方形 B 相交”？
在 Z3 中如何解决这个问题？
agda - Agda 中的 splitAt 平等
有人如何证明这种平等
? 基本情况很明显
但是之后
给
这
抛出错误：“拒绝解决异构约束 refl ...”。
还有这个
引发错误：“xs₁ != xs₁' 类型为 Vec A l₁...”。我写了这个定义：
但是不知道怎么用。
也许有一些来源，我可以从中了解更多关于 with-expressions 的信息？
谢谢。
prolog - SICStus prolog 中的匹配
这是我的代码，用于 Satchmo 定理证明。它做了一些统一。
要了解它是如何工作的，我们可以通过 ?- spy([satchmo]) 来做到这一点。
1-如果给定的查询是事实：
或者
该程序将证明它是事实。
2-如果喇叭位中的查询为：
该程序将证明它，因为它是喇叭规则。
3-如果非喇叭位中的查询为：
也会被证明的。
这是完美的工作。但是当我试图改变它时。我需要做另一种可以证明以下内容的匹配，而不是统一：
如果我有：
我想证明：
为此，我稍微修改了我的代码，而不是：
我放了一些非常相似的东西：
我将匹配定义为：
我知道我没有通过这一举动做任何事情，但我正在考虑修改 match 的定义以能够证明我需要什么。
我被困在这里的某个地方，看看我当前的代码。
在这里，我们可以测试子集：
这里的问题是我不知道如何通过证明来实现我的目标：
从：
可以通过更改匹配的定义来完成吗？如果没有，有没有其他方法可以做到这一点？
functional-programming - 如何提取 Isabelle 中的实例化变量？
我试图在 Isabelle 中证明以下内容：
如何获得hand的实例化值b？
monads - 在 Coq 中定义 Maybe monad
我想在 Coq 中使用类型类来定义 Maybe monad。
Monad继承Functor.
我想证明Some (f x') = fmap f (Some x')，这是单子定律之一。我使用compute,reflexivity和destruct option_functor，但我无法证明这一点。我不能fmap适当地简化。
theorem-proving - Idris 中的自定义证明者策略
如果我理解正确（主要是从applyTactic函数的存在），可以为 Idris 中的定理证明器编写自定义策略。我可以使用哪些（或在哪里）示例来学习如何做到这一点？