我已经定义了一个符号来模拟命令式样式编程
Notation "a >> b" := (b a) (at level 50).
然而,之后,所有函数应用程序表达式都表示为">>"样式.例如,在Coq Toplevel的证明模式中,我可以看到
bs' : nat >> list
实际上它应该是
bs' : list nat
为什么Coq积极地将所有函数应用程序样式表达式重写为我的自定义">>"表示？如何将一切恢复正常,我的意思是我想看到'a >> b'被解释为'ba'而'list nat'将不会被表示为'nat >> list'？
谢谢!
我是Coq的新用户.我已经定义了一些功能:
Definition p (a : nat) := (a + 1, a + 2, a + 3).
Definition q :=
let (s, r, t) := p 1 in
s + r + t.
Definition q' :=
match p 1 with
| (s, r, t) => s + r + t
end.
我试图将p的结果破坏成元组表示.然而,coqc抱怨q:
Error: Destructing let on this type expects 2 variables.
而q'可以通过编译.如果我改变p以返回一对(a + 1,a + 2),则相应的q和q'都可以正常工作.
为什么let-destruct只允许配对？或者我在语法上有任何错误？我已经检查过Coq手册,但没有发现任何线索.
谢谢!
我在链接文件中创建了一些特殊部分，我希望它们位于不同的段中以具有不同的页面权限。
在链接描述文件中，PHDRS 命令可以指定链接文件中的段。但是，正如文档所说，除了命令中指定的之外，PHDRS 不会创建任何默认定义的段。我在ld --verbose输出中没有发现 PHDRS 命令。
有没有办法保留默认值？或者段的默认规范是什么，以便我可以在自己的链接器脚本中编写它们？
我正在调试共享库。我发现在Linux主机上启用ASLR时可以触发该错误，而禁用ASLR时该错误消失。
我想用gdb进一步调试共享库。但是我发现它总是在固定地址加载共享库，这使得bug消失了。
有什么办法可以禁用这个 gdb 的功能吗？
使用Coq时，我试图破坏对等价假设。但是我没有找到适合我的策略。
情况是：
a, b, a', b' : nat
H0 : (a, b) = (a', b')
我想破坏H0中的对以生成
H1 : a = a'
H2 : b = b'
我该如何实现？我应该使用哪种战术？还是应该定义销毁这种对的引理？
谢谢！
我的问题是:为什么'直觉'在我的例子中起作用？
我想证明
Lemma eqb_false : forall n m : nat, eqb n m = false -> n <> m.
在最后一步,我可以看到
n : nat
IHn : forall m : nat, (n =? m) = false -> n <> m
m : nat
IHm : (S n =? m) = false -> S n <> m
============================
(n =? m) = false -> S n <> S m
那么'直觉'/'firstorder'/'auto'都可以解决当前的目标.
但为什么他们工作？Coq手册说他们会进行一些搜索工作.这是否意味着它可以用其他一些简单的策略重写？
谢谢!
编辑:可以看出我在上面的证明中对n和m应用了归纳法.根据@Vinz的回答,它没有必要进行这样的归纳过程.intros在第一步和intro目标n <> m,它将产生一个矛盾的假设H.
如果我想在Haskell程序上使用Coq编写证明和算法/语义。如何从Haskell转换为Coq来做到这一点？
似乎有翻译OCaml程序的工具。但是Haskell呢？
我有两个假设
IHl: forall (lr : list nat) (d x : nat), d = x \/ In x l' -> (something else)
Head : d = x
虽然我想apply IHl在头上,因为它满足Head了IHl.然而d = x \/ In x l战术将通过简单的暗示失败apply with.
我应该使用哪种策略来实例化假设中的变量？
我注意到在C语言中,文件I/O依赖于文件描述符.但是在某些标准库函数中write(int fd, xxxx),文件描述符似乎是一个整数,而在某些其他函数中,fseek(FILE *stream, xxxx)它表示为指针.
是否int重视fd和FILE *相同？为什么C语言会留下这样的差异？
(我试图找到一个类似的问题,但失败了,虽然我的问题似乎是初步的)
我需要证明一个定理:
Theorem t : forall x, (fix f (n : nat) : nat := n) x = x.
一个非正式的证据将如此简单
f is an identity function. So the result is the same as the input.
如果我使用simpl之后intro x,什么都不会改变.Coq不会尝试使用抽象值x来评估fix-function.但是如果我对x进行归纳分析,Coq将自动评估等式的左侧并将其减少为0和S x.
为什么Coq禁止我用抽象值x来评估修复函数？