腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
2
回答
Coq
的
就地
简化
我想要这个目标: f (S j') = f (j' + 1) 由
Coq
自动验证。目前我要写
的
是: apply f_equal. omega.有没有办法像Isabelle那样
就地
重写一个术语?
浏览 25
提问于2020-04-07
得票数 0
回答已采纳
1
回答
在
Coq
中使用自反性
我正在尝试()中
的
示例,这时我注意到要解决这个例子,请在链接中给出: andb b c = true → b = true我们正在销毁出现在c左边
的
b表示"andb“。我发现同样
的
方法没有帮助。“反身性”并没有帮助,我认为这是因为'b‘在子目标中
的
位置。
浏览 2
提问于2016-05-13
得票数 0
2
回答
Coq
中纸、剪刀、岩石作为Monoid实例
的
证明
、
、
所以在学习
Coq
的
时候,我做了一个简单
的
例子:纸,剪刀,石头。我定义了一个数据类型。Definition compose {A B C} (g : B -> C) (f : A -> B) : (A -> C) :=Class Monoid {A : Type} (dot : A ->
浏览 0
提问于2014-06-26
得票数 0
1
回答
coq
中
的
模数
简化
、
、
我是
Coq
的
初学者,我被
Coq
的
一个问题困住了,我无法进一步
简化
这个问题。如果任何人有任何关于如何将问题分解为较小步骤
的
提示,那就太好了。引理是这样
的
: forall (n : N) (n0 : N), mod (2 * N.pos
浏览 6
提问于2021-10-28
得票数 2
1
回答
SSreflect不能与Emacs、
Coq
和ProofGeneral一起使用。如何在MacOS中安装SSreflect?
、
、
、
、
如果我执行像- From mathcomp Require Import ssreflect.这样
的
操作,它会给出以下错误。这可能是因为我安装了ssreflect,但并不完全是我想要
的
方式。 但问题是,我想要第一种工作方式,因为我有很多程序都是用这种方式编写
的
,而且似乎不符合逻辑地更改每个程序中
的
行。这是我
的
.emacs文件中
的
内容-(我想我可能需要添加类似于mathcomp/ssreflect
的
路径。'(
coq
-prog-name
浏览 15
提问于2020-03-11
得票数 0
回答已采纳
1
回答
为什么不能用
Coq
中
的
抽象值来计算固定定义
的
表达式?
非正式
的
证据很简单,就像为什么
Coq
禁止我用抽象值x计算修复函数?
浏览 1
提问于2015-07-24
得票数 3
回答已采纳
1
回答
用一个简单
的
定理证明来理解
Coq
、
我对
Coq
非常陌生,现在我只能用一个简单
的
定理来理解
Coq
的
“理由”: andb b c = true ->
浏览 0
提问于2018-04-30
得票数 1
回答已采纳
3
回答
如何证明短时nat比较,如10000 >1西格玛类型
的
Coq
?
目前我有:Require Import
Coq
.Arith.Arith.如何证明随机高
的
数字,例如: 10000 >1?如何
简化
这个西格玛类型
的
值
的
创建?目前,我必须有单独
的
几行代码和一个证明,甚至有一个名称。。
浏览 11
提问于2022-01-06
得票数 0
回答已采纳
1
回答
简化
Coq
中
的
子公式
、
我想要解一个形式
的
方程其中*是一些复杂
的
左联想运算。目前,一切都是不透明
的
(包括*和A通过F),并且可以通过autounfold with M_db实现透明。知道我该怎么做吗?这是我目前
的
方法,但是in A或at A不起作用。而且,我不清楚这是正确<e
浏览 4
提问于2017-09-13
得票数 5
回答已采纳
2
回答
在
coq
中逐步
简化
?
有没有办法一步一步地
简化
呢?假设您有f1 (f2 x),这两个都可以通过单个simpl依次
简化
,是否可以将f2 x
简化
为第一步,检查中间结果,然后
简化
f1Theorem pred_length : forall nQed.Nat.pred (length (n :: l)) --> Nat.pred (S (length l)) --&g
浏览 0
提问于2016-09-07
得票数 11
回答已采纳
1
回答
如何证明两个非等值单态集
的
交是空
的
我已经把证据
的
基本内容
简化
为几个陈述,即两个不同
的
单例集
的
交集是空
的
,但无法证明这个看似简单
的
事实。Require Import
Coq
.Strings.String. Example x: string := "x".
浏览 0
提问于2019-05-26
得票数 1
回答已采纳
1
回答
我如何证明
Coq
中
的
引理?
我正在试着为下面的引理写一个
Coq
poof:Require Import FMapAVL.我无法
简化
(M.add k k m)部件。
浏览 0
提问于2017-09-22
得票数 0
1
回答
证明函数是如何证明
的
?
如果有人能很好地解释在以下简单情况下如何使用验证函数,这将有助于我理解“程序/校对”
的
并行性: Theorem ex1: forall n:nat, 7*5 < n -> 6*6 <= n.如何使用它
的
返回值?说ex1
的
返回值是forall n : nat, 7 * 5 < n -> 6 * 6 <= n类型
的
实例是正确
的
吗?
浏览 1
提问于2020-05-22
得票数 1
回答已采纳
1
回答
向量:t A n=t A (n+0)?
Require Import
Coq
.Vectors.Vector. Lemma one (A:Type)(n:nat): t A n = t A (n+0).如何将(n+0)
简化
为n?
浏览 18
提问于2020-10-06
得票数 0
回答已采纳
1
回答
关于排列
的
表示
、
、
、
、
我希望有一个归纳类型来描述排列及其在一些容器上
的
操作。很明显,根据这种类型
的
描述,算法
的
定义复杂度(根据其长度)(计算合成或逆,分解为不相交
的
循环等)。会有所不同。Inductive Permutation : nat -> Set :=| cons : forall (n k :在大小为n
的
向量上定义它
的
操作很容易,在
浏览 1
提问于2013-07-02
得票数 26
回答已采纳
1
回答
Coq
部分:需要类型类型实例
、
Require Import Relations RelationClasses. Variable A : Type. (* ... *)我怎么能要求R成为局部订单呢?
浏览 3
提问于2017-06-26
得票数 3
回答已采纳
1
回答
在依赖类型
的
表达式中重写术语失败,原因未知
下面是一个更大
的
证明
的
简化
片段,它捕获了有问题
的
行为。 Parameter t : Type. Parameter x : t.当您用rewrite prop替换rewrite prop2时,
coq
失败并出现隐含错误。然而,在我
的
观点中,
coq
应该在重写步骤之后产生forall e : t, True。有人能帮我吗?
浏览 0
提问于2011-11-17
得票数 3
1
回答
Coq
中有理表达式
的
简化
与平凡有理等价
的
证明
在下面的例子中,我可以使用哪些策略来执行rational表达式
的
简化
并证明微不足道
的
rational等价性? Require Import
Coq
.QArith.QArith.
浏览 2
提问于2015-09-23
得票数 0
回答已采纳
2
回答
无法定位库
相同
的
Linux命令在一个环境中成功,而在另一个环境中失败:我正在遭受
的
失败是Debian拉伸和
Coq
v8.5Linux, version 8.5 (June 2016)我得到
的
错误信息是:取得
的
成功结果如下: Welcome to
Coq</e
浏览 3
提问于2016-12-04
得票数 2
回答已采纳
1
回答
Coq
:使用"rewrite“或"apply”将negb (neqb true)
简化
为true?
、
、
在证明中,我希望将(negb (negb true))
简化
为true (与false类似)。我知道
Coq
的
negb_involutive过程,但由于我
的
教科书没有介绍它,我认为我应该设法只使用rewrite或apply来模仿它
的
功能。
浏览 1
提问于2016-11-15
得票数 2
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
软网推荐:就地取材用好微软的OneDrive
简化的 eggjs debug
C语言简化struct的表达
简化云中的数据管理
工具Demux——简化复杂的DAPP开发
热门
标签
更多标签
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM
活动推荐
运营活动
广告
关闭
领券