腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(8143)
视频
沙龙
1
回答
Coq
:
证明
不带
非
递归
构造
函数
的
归纳
类型
是
不可
驻留
的
coq
、
dependent-type
、
theorem-proving
我
是
第一次接触
Coq
和它
的
基本理论。假设有一个
归纳
类型
,它没有
非
递归
构造
函数
。
不可
能生成它
的
一个实例。但它能被
证明
吗?如果不是-这是
Coq
的
缺点还是CoC
的
特性?
浏览 20
提问于2019-05-12
得票数 2
回答已采纳
1
回答
在一般
的
构造
演算中,
构造
函数
是
不相交
的
和内射
的
吗?
functional-programming
、
coq
、
dependent-type
,它看起来像
Coq
中使用
的
归纳
构造
的
演算,对于
归纳
类型
有不相交
的
内射
构造
函数
。 在普通
的
构造
演算(例如,没有原始
归纳
类型
)中,对
类型
(例如,∏(Nat: *).∏(Succ: Nat → Nat).∏(Zero: Nat).Nat)使用模拟编码,这仍然
是
正确
的
吗?我能始终找出使用了哪个“<em
浏览 3
提问于2017-05-03
得票数 3
回答已采纳
1
回答
归纳
和CoInductive之间
的
唯一区别是对它们
的
使用进行格式良好性检查(在
Coq
中)?
coq
、
coinduction
、
corecursion
、
codata
换句话说:如果我们分别删除
归纳
和协同
归纳
数据
类型
的
终止检查和保护条件,那么
归纳
/协同
归纳
和固定/协同修复之间
的
根本区别会消失吗?我所说
的
“根本差异”指的是
Coq
核心演算
的
差异,而不是语法和证据搜索等方面的差异。 这似乎最终归结为一个关于
构造
微积分
的
问题。注意:我知道一个定理
证明
者跳过了终结性检查/
递归
/协同
浏览 2
提问于2020-12-11
得票数 1
1
回答
在具有
非
均匀
类型
参数
的
数据
类型
上进行
归纳
会产生错误
类型
的
术语。
coq
、
theorem-proving
我正致力于在
Coq
中正式化,但是对于具有
非
均匀
类型
参数
的
归纳
数据
类型
,我很难通过
归纳
法来
证明
。 Pure :: a -> Select f a这里
的
关键
是
第二个数据<e
浏览 0
提问于2019-07-08
得票数 5
回答已采纳
1
回答
不带
基数参数
的
类型
不等式
coq
怎样才能让
Coq
让我
证明
句法
类型
的
不等式?我读过
的
答案,它表明,如果假设
是
单价
的
,那么
证明
类型
不等式
的
唯一方法就是通过基数参数。我
的
理解
是
-如果
Coq
的
逻辑与单价一致,它也应该与单价
的
否定一致。虽然我知道单价
的
否定实际上
是
某些同构
类型
是
不相等<e
浏览 5
提问于2020-04-18
得票数 3
回答已采纳
2
回答
Coq
中
的
受限
归纳
类型
定义
coq
我想以某种方式限制
构造
函数
在
归纳
定义中允许接受
的
输入
类型
。这里
的
思想
是
,D通过在末尾添加一个零来加倍一个
非
零数,S采用一个以零为最后一位
的
数字,并将最后一位转换为一。这意味着以下
是
合法
的
数字:D (S 0)而以下内容则不是:D 0 有没有办法在
归纳
定义中以一种干净
的
方式实施这样
的
限制?
浏览 0
提问于2012-12-23
得票数 4
回答已采纳
1
回答
为什么嵌套
归纳
策略也将
归纳
假设嵌套在lambda下?
coq
据我所知,
Coq
策略
是
在幕后编译成一些
函数
式程序
的
,但我真的不确定这是怎么回事。我非常确定这不是我想要做
的
。 我想要做
的
是
类似下面的Idris程序。prf_add_assoc' in Refl 更具体地说,我需要prf1、prf2和prf3,它们
是
我通过
递归
调用在
Coq
中,两个
证明
卡在一个l
浏览 15
提问于2019-04-09
得票数 1
回答已采纳
1
回答
在
Coq
中通过
归纳
谓词上
的
递归
定义
函数
coq
我正在尝试在
Coq
中重新实现我
的
一些Agda代码。我
的
问题
是
,我
的
一个Agda
函数
是
由
归纳
谓词结构上
的
递归
定义
的
。在我
的
Coq
代码中,我试图遵循相同
的
风格,但有一个模式匹配限制,它不允许在Prop中分析具有
类型
的
值
的
结构,从而在Set中产生结果。我
的
问题
是
:
浏览 2
提问于2018-01-19
得票数 1
回答已采纳
1
回答
什么时候
归纳
类型
的
构造
函数
是
穷尽
的
?
coq
对于自然数nat这样
的
简单
归纳
型,很容易
证明
两个
构造
函数
(0和后继)给出了所有可能
的
自然数,eq_destruct : forall (A : Type) (x : A) (prEq : x
浏览 0
提问于2018-09-12
得票数 1
回答已采纳
2
回答
Coq
核
的
证明
技术
coq
伊莎贝尔将其核心
证明
能力建立在与高阶统一相结合
的
分辨率上。命题作为
类型
可能会占用过多
的
空间;什么将取代Huet
的
高阶逻辑统一程序?。
浏览 3
提问于2020-08-12
得票数 1
回答已采纳
1
回答
“功能性诱导”策略在
Coq
中有什么作用?
coq
、
coq-tactic
我用过functional induction来
证明
我一直在尝试。据我所知,它基本上允许对
递归
函数
的
所有参数“同时”执行
归纳
。 将来,我怎样才能知道这种策略
是
干什么
的</
浏览 0
提问于2018-01-03
得票数 3
回答已采纳
1
回答
我能
证明
关于共进型
的
“共进原理”吗?
coq
、
agda
、
dependent-type
、
type-theory
、
coinduction
我能
证明
关于共进型
的
“共进原理”吗?例如,流
类型
的
协
归纳
原理
的
伪代码如下所示:Π destruct_head : Π x : Stream A.P y) 我
的
感觉
是
,这是正确
的
,但我想不出一个方法来
证明
它在
Coq
或Agda。
浏览 4
提问于2021-08-26
得票数 1
回答已采纳
2
回答
我们如何知道所有
Coq
构造
函数
都是内射
的
和不相交
的
?
constructor
、
coq
、
injective-function
根据,所有
构造
函数
(对于
归纳
类型
)都是内射
的
和不相交
的
: ...Similar原则适用于所有
归纳
定义
的
类型
:所有
构造
函数
都是内射
的
,从不同
的
构造
函数
生成
的
值永远都不相等。对于列表,反
构造
函数
是
内射
的
,零与每个
非
空列表不同
浏览 5
提问于2015-09-19
得票数 5
回答已采纳
1
回答
Coq
:模拟
函数
延伸性定理
coq
直观地说,当两个
函数
g和h对于所有x都相等时,我们可以想象g = h,因此将所有出现
的
f g替换为f h。这就是我们所说
的
函数
延伸性。但是,在
Coq
中,默认情况下没有添加
函数
的
可扩展性,所以我们需要它,我们需要添加一个公理。然而,我想避免使用这个公理,并试图找到一个在实践中等价
的
定理,它看起来像“对于所有输出
归纳
类型
的
归纳
函数
,对于所有g和h,f g=f h”。具
浏览 1
提问于2017-11-27
得票数 1
2
回答
为什么UIP在
Coq
中
是
不可
证明
的
?为什么match
构造
泛化
类型
?
coq
如果需要的话,必须在
Coq
中以公理方式添加UIP (以及类似于公理K
的
等价物):这是令人惊讶
的
,因为从等式
的
定义来看,这是显而易见
的
,它只有一个
构造
函数
。(当然,这取决于对
Coq
中
归纳
定义包含其
类型
的
所有元素
的
解释)。当你试图
证明
UIP时,你会被困在反身子大小写上: uip_refl
浏览 5
提问于2021-12-22
得票数 3
回答已采纳
3
回答
Haskell中
的
列表
是
归纳
的
还是
归纳
的
?
haskell
、
infinite
、
idris
、
induction
、
coinduction
所以我最近读了一些关于共
归纳
的
文章,现在我想知道: Haskell列表
是
归纳
的
还是同
归纳
的
?我还听说Haskell没有区分这两种情况,但如果是的话,他们
是
如何正式区分
的
呢?关联在Idris中,其中
类型
List a严格来说是一种
归纳
类型
,因此仅为有限列表。它
的
定义类似于Haskell
的
情况。然而,Stream a
是
一种共
归
浏览 11
提问于2016-10-04
得票数 31
回答已采纳
2
回答
Coq
生成
的
归纳
原理不像我希望
的
那样。
coq
、
induction
为便于理解而编辑
的
其中一个
构造</
浏览 0
提问于2016-02-10
得票数 0
2
回答
并集
的
特征
函数
coq
在像
Coq
这样
的
构造
性环境中,我希望析取A \/ B
的
证明
要么
是
A
的
证明
,要么
是
B
的
证明
。如果我在X
类型
的
子集上重新表述,它说如果我有x在A union B中
的
证明
,那么我要么有x在A中
的
证明
,要么有x在B中
的
证明
。所以我想通过案例分析来定义一个联
浏览 10
提问于2018-11-17
得票数 2
1
回答
支柱和
类型
的
不同
归纳
原则
coq
我注意到
Coq
对支持和
类型
的
平等性综合了不同
的
归纳
原则。有人对此有什么解释吗?平等被定义为相关
的
归纳
原则有以下几种
类型
: : forall(A : Type) (x : A) (P : A -> Prop),现
浏览 4
提问于2016-09-25
得票数 5
回答已采纳
1
回答
HoTT
的
Coq
:
证明
|| P-> X || -> (P-> ||X||)
coq
、
truncation
、
homotopy-type-theory
我需要在
Coq
中
证明
,对于任何
类型
X和任何命题P(尽管我认为即使P
是
一个
类型
,它也应该是有效
的
)存在 trunc_impl:|| P-> X || -> (P-> ||X||) 其中,||_||
是
HoTT书中用来表示命题截断
的
符号。我在
类型
论中
证明
了这一陈述:一
是
利用命题截断
的
归纳
原理,假设一个H:|| P->X ||和一个p: p,H=|
浏览 14
提问于2020-08-10
得票数 0
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
【effectiveC+】01_使用explicit禁止编译器执行非预期的类型转换
请问C+11有哪些新特性?
十分钟过一遍Kotlin知识点
C+之右值引用
C+11并发编程:多线程std:thread
热门
标签
更多标签
云服务器
ICP备案
实时音视频
即时通信 IM
对象存储
活动推荐
运营活动
广告
关闭
领券