腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
2
回答
使用
Coq
证明
加法
函数
是
相联
的
ocaml
、
coq
、
addition
、
associative
、
coq-tactic
我试图
证明
一个预定义
的
加法
函数
是
关联
的
,但我被困在目标为 "plus (S x') (plus Y z) = plus (plus (S x') y) z", 但我唯一
的
假设
是
"IHx‘:表示所有y
浏览 34
提问于2021-07-22
得票数 0
1
回答
应用程序定义失败,“无法将支持与[目标]统一”
coq
、
proof
在
Coq
中,我
使用
以下方法展示了向量上
的
append
的
相联
性: Require Import
Coq
.Vectors.VectorDef Omega.下面
是
我期望用t_app_assoc
证明
的
最简单
的
目标。当然,simpl可以
证明
这一点--这只是一个例子。或者有更好
的
方法来定义它?我认为我需要一个Program Definition,因为简单地
使用
Lemma会导致
浏览 1
提问于2018-05-13
得票数 2
回答已采纳
2
回答
Coq
中自然数
的
加法
coq
Coq
的
标准库提供Peano自然数和
加法
: | O : natFixpoint add n m := | 0 => m | S p => add p (S m)新
的
加法
是否等同于旧
的
加法
?我试图通过
证明
foral
浏览 11
提问于2022-01-23
得票数 1
回答已采纳
2
回答
coq
(或一般)中
的
定理可以在不
使用
先前
证明
的
引理
的
情况下被
证明
吗?
logic
、
coq
、
proof
由于
coq
中
的
证明
是
简单
的
高度复杂
的
函数
,可以通过各种方式中
的
任何一种来构建,因此似乎有必要为每个既不涉及先前
证明
的
定理也不涉及assert语句
的
定理提供
coq
证明
。例如,在没有任何引理
的
情况下,
证明
自然数
加法
的
交换性
是
很简单
的
,即使有引理可以让它变得更简单
浏览 1
提问于2016-03-16
得票数 2
1
回答
将要操作
的
数据与
证明
操作
是
正确
的
证明
解耦
coq
但是,我不太喜欢这个代码,原因如下: (*我不知道如
浏览 4
提问于2012-09-11
得票数 3
回答已采纳
2
回答
继承(:>)结构
是
如何在
Coq
中工作
的
?
coq
、
coercion
在一个例子中,我很难理解 (18.9)
的
机制(一般
Coq
中
的
强制)。我理解,从数学上讲,在一个semiring_{mult,plus}_m中
的
乘法和
加法
运算( SemiRing )
是
一个CommutativeMonoid。另外,类SemiRing和CommutativeMonoid
是
类似于连词/\
的
谓词
函数
。就顺序而言,我们
是
首先
证明
了A
是
SemiRing,还是首先<em
浏览 4
提问于2016-11-03
得票数 3
回答已采纳
1
回答
理解在显示
证明
上
的
COQ
证明
。
coq
、
proof
我在
COQ
中
是
新
的
,我试图
证明
反例定理。Hypothesis R2: ~B. 所以我们试着:tauto. (fun H : ~ A => let H0 : B := R1 H in let H1 : False
浏览 1
提问于2018-08-23
得票数 5
回答已采纳
1
回答
利用余弦
证明
有限集
的
幂集
是
有限
的
math
、
coq
、
formal-verification
、
powerset
在试图
证明
一些事情时,我遇到了一个看起来很无辜
的
声明,但我在
Coq
中未能
证明
。我们
的
主张
是
,对于给定
的
有限集合,powerset也是有限
的
。该语句在下面的
Coq
代码中给出。我查阅了关于有限集
的
Coq
文档以及关于有限集和幂集
的
事实,但我找不到可以将powerset解构为子集并集
的
东西(这样就可以
使用
Union_is_finite构造
函数</
浏览 28
提问于2019-05-21
得票数 5
1
回答
Coq
可以做什么,而Agda/Idris不能做?
coq
、
agda
、
idris
Coq
是
一个
证明
助手,而Agda/Idris
是
编程语言(尽管它们可以被称为
证明
助手)。 我正在探索这些语言,我想知道Agda/Idris是否足以做
Coq
所能做
的
一切。那么,有没有一些证据/管理代码/IDE (Emacs)
函数
的
方法/其他
Coq
可以做而Agda/Idris不能做
的
事情呢?
浏览 21
提问于2017-12-16
得票数 9
回答已采纳
1
回答
如何设置
Coq
作为一阶逻辑
的
定理
证明
器
logic
、
computer-science
、
coq
、
coq-tactic
、
coq-plugin
据我所知,
Coq
有内置
的
一阶逻辑https://
coq
.inria.fr/tutorial/1-basic-predicate-calculus。但
Coq
不是定理
证明
者,
Coq
是
证明
助手,这意味着用户需要在每一步中提供一些提示,
Coq
应该选择什么规则/策略。存在更多
的
ore - lest组合启发式策略,但
Coq
仍然不是
证明
者。我听说
浏览 21
提问于2019-05-15
得票数 3
回答已采纳
2
回答
coq
铸造可转换型
types
、
casting
、
coq
forall n j (jn : j < n) (ln : j + 0 < n) (P: forall {x} {y}, (x<y) -> nat),jn中
的
类型似乎可以相互转换(从算术
的
角度来看)。我如何利用这一事实来
证明
上述引理?我可以很容易地
证明
assert(JL: j < n -> j + 0 < n) by auto.,但我看不出如何将其应用于类型。
浏览 2
提问于2015-11-05
得票数 3
回答已采纳
2
回答
可以用
Coq
编写C程序吗?
coq
、
coq-extraction
我知道可以将
Coq
程序提取到Haskell和OCaml程序中。有没有办法用C来做这件事? 我正在想象一个模拟C语言
的
库。也许这样
的
库会包含一组关于C结构如何与进程内存交互
的
公理,以及关于IEEE浮点数
的
公理和定理。然后,它就可以在
Coq
内建立一个C程序,以及关于这个程序
的
定理。比如说,我会
使用
这样一个库来构建一个C快速排序算法,该算法可以在GCC可编译
的
浮点数数组上工作。
浏览 6
提问于2017-10-23
得票数 8
回答已采纳
1
回答
理解赛跑和霍夫斯
haskell
、
functional-programming
、
higher-order-functions
、
currying
我目前正在学习
函数
式编程,它最重要
的
特点
是
:高阶
函数
。plusc :: Num a => a -> (a -> a)我们在多大程度上可以说这个
函数
使用
了运行,并且
是
一个HOF?编辑:基本上,我不明白
函数
的
定义如何表示
加法
(参数、
相联
性等)
浏览 0
提问于2017-05-23
得票数 0
1
回答
在
Coq
中定义整数上
的
加法
coq
在定义
Coq
中
的
整数时,我遵循
的
回答,但当试图在其上定义
加法
时,总是会出现错误“无法猜测递减参数”。我尝试过多种不同
的
定义,似乎总是会发生这种情况。有办法
证明
Coq
的
论点正在减少吗?或者我错过了一些明显
的
方法来定义
加法
。| O | S (n : nat).
浏览 2
提问于2020-09-24
得票数 1
回答已采纳
2
回答
盖丽娜有像Agda那样
的
洞吗?
coq
在
Coq
中进行验证时,能够一次
证明
一小部分,并让
Coq
帮助跟踪义务,这是很好
的
。在这一点上,我可以看到
证明
状态,以了解完成该
证明
所需
的
内容:H2: Bgoal: BDefinition ModusPonens' :
浏览 0
提问于2020-03-12
得票数 4
回答已采纳
2
回答
Coq
中普遍量化
的
方法
coq
我对
Coq
定理
证明
器很陌生。因此,我很可能已经错过了一些基本
的
东西,在阅读教程时。 在我提出我
的
问题之前,让我假设一些假设,并回顾一下我
的
想法。有了这些假设,就可以应用Consequent模型:可以根据Minor前提和Major前提构造推断Major
的
证明
。这样
的
证明
就是带有参数Minor
的
Minor
函数
的
应用。那么,现在我想知道:在具有普遍量化命题
的
Co
浏览 4
提问于2014-05-06
得票数 0
1
回答
证明
构造
函数
是
Coq
中
的
部分
函数
coq
证明
构造
函数
是
部分
函数
,可以编码为: forall i1 i2, mkA i1 <> mkA i2 -> i1 <> i2.尽管要
证明
这一点很简单,但对于每种定义
的
类型来说,这样做听起来都很奇怪。 有什么策略来对这个财产进行编码吗?或者
是
图书馆里
的
等价物?
浏览 4
提问于2017-07-21
得票数 1
回答已采纳
1
回答
Z3与
coq
的
区别
z3
、
coq
、
theorem-proving
我想知道是否有人能告诉我Z3和
coq
之间
的
区别?在我看来,
coq
是
一个
证明
助手,因为它要求用户填写
证明
步骤,而Z3没有这一要求。但似乎
coq
也有类似于Z3
的
自动策略?或者可能
coq
中
的
证明
搜索能力没有Z3那么强大?
浏览 1
提问于2012-07-18
得票数 44
回答已采纳
2
回答
并集
的
特征
函数
coq
在像
Coq
这样
的
构造性环境中,我希望析取A \/ B
的
证明
要么
是
A
的
证明
,要么
是
B
的
证明
。如果我在X类型
的
子集上重新表述,它说如果我有x在A union B中
的
证明
,那么我要么有x在A中
的
证明
,要么有x在B中
的
证明
。所以我想通过案例分析来定义一个联合
的
特征
函
浏览 10
提问于2018-11-17
得票数 2
1
回答
通过提供一个示例来
证明
存在
coq
、
proof
如果我有一个形式
的
定理:Admitted.如果我想
证明
一个
函数
是
这样my_func 0 = 0,我如何告诉
coq
确实存在这样
的
测试,因为my_func 0=0? 这没有深入
的
目标,但理解存在
证明
在
coq
中
是
如何工作
的
。
浏览 20
提问于2021-12-01
得票数 1
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
特斯拉跑车2022:价格、发布窗口、续航里程等
Python基础教程 多态和方法
Dipperin WASM虚拟机性能何以完胜以EVM?
前端专家聊JS语言家族新成员——R&B
基础知识与方法
热门
标签
更多标签
云服务器
ICP备案
实时音视频
即时通信 IM
对象存储
活动推荐
运营活动
广告
关闭
领券