问题标签 [coq-tactic]
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.
coq - 记录平等的 Coq 策略?
在 Coq 中,当试图证明记录的相等性时,是否有一种策略可以将其分解为所有字段的相等性?例如,
有没有一种策略可以减少这种情况a = c /\ b = d
?请注意,一般来说,任何一个都a b c d
可能是大而复杂的证明术语(然后我可以用证明无关公理来解除)。
coq - Coq 中是否有最小的完整策略集?
我见过很多功能上相互重叠的 Coq 策略。
例如,当您在假设中有确切的结论时,您可以使用assumption
, apply
, exact
, trivial
, 或者其他。destruct
其他示例包括induction
非归纳类型(??)。
我的问题是:
是否存在完整的最小基本策略集(不包括auto
等),从某种意义上说,该集可用于证明任何 Coq 可证明的关于自然数函数的定理?
理想情况下,这个最小完整集合中的策略是基本的,因此每个人只执行一个(或两个)功能,并且可以很容易地理解它的作用。
coq - 在 Coq 中使用“apply with”而不给出参数名称?
在使用 Coqapply ... with
策略时,我看到的所有示例都涉及显式指定要实例化的变量的名称。例如,给定一个关于等式传递性的定理。
apply
对它:
请注意,在最后一行apply trans_eq with (m := 1).
中,我必须记住要实例化的变量的名称是m
,而不是o
或n
或其他一些名称y
。
对我来说,是否在定理的原始陈述中使用m n o
或x y z
使用都无关紧要,因为它们就像虚拟变量或函数的形式参数。有时我不记得我在定义定理时使用的具体名称或其他人放在不同文件中的名称。
有没有一种方法可以让我引用变量,例如通过它们的位置并使用类似的东西:
在上面的例子中?
顺便说一句,我试过了:apply trans_eq with (1 := 1).
得到了Error: No such binder.
谢谢。
coq - 如何使用 plus communtativity 和 associativity 重新排列 Coq 中的术语?
我有一个关于如何在 Coq 中重新排列术语的一般性问题。例如,如果我们有一个 term m + p + n + p
,人类可以快速将这些术语重新排列成类似的东西m + n + p + p
(隐式使用 plus_comm 和 plus_assoc)。我们如何在 Coq 中有效地做到这一点?
举一个(愚蠢的)例子,
现在,我们有
我的问题是:
如何m + n + p + p
有效地重写 LHS?
我尝试使用rewrite plus_comm at 2
,但它给出了一个错误Nothing to rewrite.
只需使用重写plus_comm
将 LHS 更改为p + m + n + p
.
也欢迎任何关于有效重写的建议。
谢谢。
coq - 可以在 Coq 中隐含使用 destruct 吗?
destruct可用于拆分and,或在 Coq 中。不过好像也可以用含蓄?例如,我想证明~~(~~P -> P)
当destruct pff.
它工作正常时,但我不知道为什么?谁能为我解释一下?
coq - 如何在 Coq 中引入新变量?
我想知道是否有办法在 Coq 中证明一个定理时引入一个全新的变量?
对于一个完整的示例,请考虑以下关于列表长度均匀性的属性。
现在我想证明对于任何列表l
,如果它length
是偶数,则ev_list l
成立:
这使:
现在,我想“定义”一个新的自由变量n
和一个假设n = length l
。在手写数学中,我认为我们可以做到这一点,然后对n
. 但是有没有办法在 Coq 中做同样的事情?
笔记。我问的原因是:
我不想将其
n
人为地引入定理本身的陈述中,就像在前面链接的页面中所做的那样,恕我直言,这是不自然的。我试过了
induction H.
,但它似乎不起作用。Coq 无法对length l
'sev
-ness 进行案例分析,也没有生成归纳假设 (IH)。
谢谢。
coq - 如何检查策略生成条款中的可兑换性?
假设我有以下策略来检查一个术语是否是文字零:
现在想象一下,我希望该策略接受更多;也许任何可以用零转换的术语。如果这是针对目标的策略,我会这样做
但这对于产生术语的策略来说是失败的:
如何检查战术产生条款中的可兑换性?在这个具体的例子中,减少或x
计算它(let xx := eval compute in x
PS:作为参考,未简化的问题是我正在尝试有效地查找一个键,该键可能与FMap
由调用序列构建的值匹配add
,并且该策略看起来像
在这个实现中,如果不是value
map 包含一个可转换为value
但在语法上不等于它的术语,则该策略将错误地返回None
.
coq - 如何将当前目标/子目标保存为“断言”引理
在证明过程中,我遇到了一种情况,即当前目标/子目标在同一定理的后期阶段证明是有用的。
是否有一种策略可以将当前目标“保存”为引理,就好像当前目标已被assert
编辑一样?
当然,我可以 assert
明确地复制并粘贴到目标,或者在当前定理之前写一个单独的引理。但我只是好奇是否存在捷径。
谢谢。
coq - 如何在 Coq 的简化过程中应用一次函数?
据我了解,Coq 中的函数调用是不透明的。有时,我需要使用unfold
它来应用它,然后fold
将函数定义/主体转回其名称。这通常很乏味。我的问题是,有没有更简单的方法来应用函数调用的特定实例?
作为一个最小的例子,对于 list l
,证明右附加[]
不会改变l
:
这留下:
现在,我需要应用一次++
(ie app
) 的定义(假设目标中还有其他++
我不想应用/扩展的)。目前,我知道实现这个一次性应用程序的唯一方法是先展开++
然后折叠它:
给予:
但这很不方便,因为我必须弄清楚要在fold
. 我做了计算,而不是 Coq。我的问题归结为:
有没有更简单的方法来实现这个一次性功能应用程序达到同样的效果?