腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
1
回答
coq
中
的
模数
简化
、
、
我是
Coq
的
初学者,我被
Coq
的
一个问题困住了,我无法进一步
简化
这个问题。如果任何人有任何关于如何将问题分解为较小步骤
的
提示,那就太好了。引理是这样
的
: forall (n : N) (n0 : N), mod (2 * N.pos
浏览 6
提问于2021-10-28
得票数 2
1
回答
验证不同语言
的
Coq
证明
是否支持在不同
的
环境(例如Java、C++)
中
解释和验证
Coq
证明?一种显而易见
的
方法是在Java
中
从头开始构建一个完整
的
解释器,但我想知道最小
的
要求是什么。
浏览 11
提问于2019-03-11
得票数 2
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
浏览 0
提问于2014-06-26
得票数 0
2
回答
Coq
的
就地
简化
我想要这个目标: f (S j') = f (j' + 1) 由
Coq
自动验证。目前我要写
的
是: apply f_equal. omega.
浏览 25
提问于2020-04-07
得票数 0
回答已采纳
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
回答
简化
Coq
中
的
子公式
、
我想要解一个形式
的
方程其中*是一些复杂
的
左联想运算。目前,一切都是不透明
的
(包括*和A通过F),并且可以通过autounfold with M_db实现透明。知道我该怎么做吗?这是我目前
的
方法,但是in A或at A不起作用。而且,我
浏览 4
提问于2017-09-13
得票数 5
回答已采纳
1
回答
用一个简单
的
定理证明来理解
Coq
、
我对
Coq
非常陌生,现在我只能用一个简单
的
定理来理解
Coq
的
“理由”: andb b c = true ->
浏览 0
提问于2018-04-30
得票数 1
回答已采纳
1
回答
SSreflect不能与Emacs、
Coq
和ProofGeneral一起使用。如何在MacOS
中
安装SSreflect?
、
、
、
、
如果我执行像- From mathcomp Require Import ssreflect.这样
的
操作,它会给出以下错误。这可能是因为我安装了ssreflect,但并不完全是我想要
的
方式。 但问题是,我想要第一种工作方式,因为我有很多程序都是用这种方式编写
的
,而且似乎不符合逻辑地更改每个程序
中
的
行。这是我
的
.emacs文件
中
的
内容-(我想我可能需要添加类似于mathcomp/ssreflect
的
路径。'(
浏览 15
提问于2020-03-11
得票数 0
回答已采纳
1
回答
证明函数是如何证明
的
?
如果有人能很好地解释在以下简单情况下如何使用验证函数,这将有助于我理解“程序/校对”
的
并行性:ex1 = fun (n : nat) (H : 7 * 5 < n) => H在验证过程
中
是否执行了验证函数如何使用它
的
返回值?说ex1
的
返回值是forall n : n
浏览 1
提问于2020-05-22
得票数 1
回答已采纳
1
回答
为什么不能用
Coq
中
的
抽象值来计算固定定义
的
表达式?
非正式
的
证据很简单,就像为什么
Coq
禁止我用抽象值x计算修复函数?
浏览 1
提问于2015-07-24
得票数 3
回答已采纳
1
回答
如何
简化
Coq
中
的
实数项?
、
我试着用
Coq
做实数
的
简单证明。例如,我想证明两个非负数
的
平均值也是非负
的
。我
的
第一步是证明r1 + r2 >=0如下所示。Require Export
Coq
.Reals.R_sqrt.H1 : r1 + r2 >= 0 + 0(r1 + r2) / 2 >= 0 在假设<em
浏览 2
提问于2015-12-20
得票数 3
回答已采纳
3
回答
如何证明短时nat比较,如10000 >1西格玛类型
的
Coq
?
目前我有:Require Import
Coq
.Arith.Arith.如何证明随机高
的
数字,例如: 10000 >1?如何
简化
这个西格玛类型
的
值
的
创建?目前,我必须有单独
的
几行代码和一个证明,甚至有一个名称。。
浏览 11
提问于2022-01-06
得票数 0
回答已采纳
1
回答
关于排列
的
表示
、
、
、
、
我希望有一个归纳类型来描述排列及其在一些容器上
的
操作。很明显,根据这种类型
的
描述,算法
的
定义复杂度(根据其长度)(计算合成或逆,分解为不相交
的
循环等)。会有所不同。Inductive Permutation : nat -> Set :=| cons : forall (n k :在大小为n
的
向量上定义它
的</e
浏览 1
提问于2013-07-02
得票数 26
回答已采纳
2
回答
is_int与
模数
%1
的
差异?
is_int给出了我
的
想法,但是使用
模数
来检查它是否是整数(%1),我也得到了浮点数。</br>';}
模数
为14.2857142857,
模数
为14.4285714286等等我对
模数
的
理解有什么问题?编辑我欣赏%7是正确
的
使用
模数
在这个例子,但这是一个
简化
的
情况。
浏览 6
提问于2014-08-08
得票数 0
回答已采纳
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)我得到
的
错误信息是:取得
的
成功结果如下: Wel
浏览 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
1
回答
如何证明两个非等值单态集
的
交是空
的
我已经把证据
的
基本内容
简化
为几个陈述,即两个不同
的
单例集
的
交集是空
的
,但无法证明这个看似简单
的
事实。Require Import
Coq
.Strings.String. Example x: string := "x".
浏览 0
提问于2019-05-26
得票数 1
回答已采纳
1
回答
如何让注释在
Coq
中
的
模块签名之外可见?
、
我在
Coq
中
定义了一个模块签名,它定义了几个符号。然而,当我试图在签名之外使用这些符号时,
Coq
失败了。下面给出了我
的
代码
的
简化
版本。任何帮助都将不胜感激。
浏览 2
提问于2013-03-31
得票数 2
回答已采纳
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
Go 爬虫在大规模数据抓取中的性能如何
Python选择结构中多条件测试的简化写法
网站建设中内容的简化更利于用户体验!
Oracle开源Graphpipe:简化机器学习模型在框架中的部署
简化项目启动:项目管理软件中的立项管理流程
热门
标签
更多标签
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM
活动推荐
运营活动
广告
关闭
领券