腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
2
回答
/\:
证明
如果
(A,
B
) = (
C
,
D
)
则
A=
C
Coq
B
=
D
coq
、
theorem-proving
正如标题所示,我找不到足够的工具来解决这个微不足道的问题: p : (A,
B
) = (
C
,
D
)A =
C
/\
B
=
D
我怎么
证明
呢?
浏览 31
提问于2019-12-19
得票数 1
回答已采纳
3
回答
如果
(和
b
b
c
= orb
c
)在
coq
中,我如何
证明
b
=
c
?
coq
、
proof
、
proof-of-correctness
我是新来的,我想
证明
这一点. forall (
b
c
: bool),intros
b
c
.destruct
b
.simpl. reflexivity.但即使我这么做了,我
浏览 0
提问于2015-08-30
得票数 4
回答已采纳
1
回答
(A ->
B
) /\ (
C
->
D
) <:(A /\
C
) -> (
B
/\
D
)?
subtype
、
type-theory
(A ->
B
) /\ (
C
->
D
)是(A /\
C
) -> (
B
/\
D
)的一个亚型吗?
如果
不是,反例是什么? (为了澄清,我在这里使用/\作为交叉口。)
浏览 8
提问于2020-04-16
得票数 1
回答已采纳
1
回答
记录平等的
Coq
战术?
coq
、
coq-tactic
在
Coq
中,当试图
证明
记录相等时,是否有一种将其分解为所有字段相等的策略?例如,有没有一种策略可以将这种情况减少到a =
c
/\
b
=
d
呢?请注意,一般来说,任何一个a
b
<
浏览 1
提问于2014-07-06
得票数 7
回答已采纳
1
回答
Coq
中的反例
证明
coq
、
proof
、
quantifiers
、
negation
在
证明
了命题和谓词演算中的数十个引理(有些比另一些更具有挑战性,但通常仍然可以在intro-apply-destruct自动驾驶仪上
证明
)之后,我碰到了一个起始w/ ~forall的引理,并立即陷入困境显然,我对
Coq
缺乏理解和知识。所以,我要求用一种低级的
Coq
技术来
证明
一般形式的语句。exists A [
B
].., ~(
C
-> <em
浏览 2
提问于2016-03-01
得票数 4
回答已采纳
2
回答
构造函数的分解相等
coq
、
coq-tactic
经常在
Coq
中,我发现自己做了以下工作:我有一个
证明
目标,例如:我只需要
证明
a =
b
,因为其他的一切都是一样的,所以我做了:rewrite H.完成了证据。 但是,在我的证据的最下面,让那些人在我身边闲逛似乎是不必要
浏览 3
提问于2016-05-27
得票数 6
回答已采纳
1
回答
你能在
Coq
中枚举归纳类型的所有值吗?
types
、
coq
、
induction
有没有办法在
Coq
中枚举有限归纳类型的值?Inductive state := A |
B
|
C
|
D
| E.有没有办法通过这个定义,以编程方式获得对A、
B
、
C
、
D
和E的访问?我知道在
证明
中,我可以使用induction策略来
证明
每种情况,但我希望能够循环类型的值。
浏览 17
提问于2019-12-01
得票数 1
3
回答
类型乘积的内射性有意义吗?
coq
、
dependent-type
如何在
Coq
中
证明
以下几点? Goal forall (A
B
: Type), (A*A =
B
*
B
)%type -> A =
B
.
如果
它是不可
证明
的,那么它可以安全地添加为公理吗?
浏览 28
提问于2019-12-26
得票数 1
4
回答
组合对象数组({a:a,
b
:
b
,
c
:
c
},{a:a,
d
:
d
,
c
:
c
})到({a:a,
b
:
c
,
d
:
c
})
javascript
、
jquery
、
underscore.js
我有一个数据列表,我需要对其进行转换和“透视”,以将一列转换为多列。 我拥有的对象列表如下所示: var list = [ "date": "2016-05-31", "value": 10{ "action": "run",}, "date":
浏览 44
提问于2016-07-16
得票数 0
回答已采纳
1
回答
Ensemble的标准笛卡尔乘积结构是什么?
coq
、
cartesian-product
、
set-theory
我在
Coq
.Sets.Ensemble中对集合使用Ensemble类型。这个库定义了Union和Intersection,但我找不到任何笛卡尔乘积的结构。我试着像这样构造一个引理: Lemma cartesian_inclusion : forall A
B
C
D
: Ensemble U, Included U A
C
/\ IncludedU
B
D
-> Included (U * U) (A,
B
) (
C</e
浏览 14
提问于2019-05-19
得票数 2
回答已采纳
3
回答
选择子项重写的惯用方法
coq
假设我们有一个形式的结论:a +
b
+
c
+
d
+ e。replace (a +
b
+
c
+
d
+ e)by now rewrite &l
浏览 1
提问于2017-06-13
得票数 6
回答已采纳
1
回答
不能使用PeanoNat.Nat.add_assoc来
证明
coq
但是当我创建一个定理并尝试使用它时,它会产生一个错误: a +
b
+
c
+
d
+ e = f. 为什么找不到定理呢?
浏览 1
提问于2019-06-13
得票数 1
回答已采纳
3
回答
链接JQ if:
如果
A,
则
B
,
C
,其他
D
端
json
、
bash
、
jq
、
swap
food.fruit[] | select(.type=="banana") | .count = 0 empty' 我无法将其输送到下一行,因此我不确定这里应该使用哪个操作符--
如果
支持这种功能的话
浏览 5
提问于2021-02-18
得票数 3
回答已采纳
2
回答
解方程a+
b
+
c
+
d
=a*
b
*
c
*
d
algorithm
、
math
然而,O(N^4)算法需要很长的时间,因为A、
B
、
C
和
D
的每个值的范围都是(0,2000)。所以我们可以说A<=
B
<=
C
<=
D
我想使我的算法更快地将它转换成O(n^3)解。为此,我使用A、
B
和
C
来考虑某些因素,以使算法运行得更快一些(剪枝)。但是主要的问题是关于
D
的搜索,我已经读过一些类似问题的解,他们从A+
B
+
C
=A*
B
*
C
导出
D</
浏览 2
提问于2014-08-09
得票数 1
回答已采纳
2
回答
B
到
D
管道?-A&
B
,
C
,
C
,
D
bash
、
pipe
是否有一种方法可以重写命令结构A &&
B
||
C
|
D
,以便将
B
或
C
输入到
D
中?例如: 📷
浏览 0
提问于2017-04-17
得票数 14
回答已采纳
1
回答
如何写出A ::
B
::
C
=>
D
给出A ::
B
::
C
和(A,
B
,
C
) =>
D
?
scala
、
shapeless
假设我有一个HList类型的A ::
B
::
C
和一个函数(A,
B
,
C
) =>
D
。如何以最简单和最惯用的方式编写函数A ::
B
::
C
=>
D
?
浏览 4
提问于2015-03-02
得票数 4
回答已采纳
2
回答
MiniKanren有"not“操作符吗?
clojure
、
logic-programming
、
negation
、
clojure-core.logic
、
minikanren
例如,如何表示Prolog的
如果
a为真而
c
为假,
则
b
为真(Prolog使用否定作为失败,即
如果
不能
证明
not(
c
)被认为是
证明
的) Prolog的not也适用于非地面表达式a(X,
d
(Y)) :-
b
(
d
(X),
d
(Y)), not(
c
(
d
(X)))
浏览 5
提问于2017-08-11
得票数 5
回答已采纳
1
回答
搜索
Coq
库
coq
我试图
证明
Coq
中的n <= 2^n,我忽略了一个必须存在于某个地方的简单引理:更广泛地说,我如何在
Coq
库中搜索像这样的引理?Require Import
Coq
.Arith.PeanoNat. (* exponential function *) (***
浏览 8
提问于2020-05-09
得票数 1
回答已采纳
1
回答
为什么使用
Coq
的setoid_replace "by“子句需要额外的idtac?
coq
)Require Import QArith. a ==
b
->
b
+
d
== a +
c
->
c
==
d
. Proof.Lemma test_rearrange a
b
c
浏览 3
提问于2015-07-07
得票数 3
回答已采纳
1
回答
如何使用
Coq
交互定理验证器运行Frama插件?
coq
、
frama-c
以下是swap示例表单WP插件教程;@ ensures A: *a == \old(*
b
) ; return;这是我用
coq
在上面运行frama的结果;[kernel] ParsingFRAM
浏览 5
提问于2016-04-13
得票数 2
回答已采纳
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
Ctrl键与字母A、B、C、D、E、F、G、H和I的不解情缘!
车赢门:基于逆向效益链的汽车后市场D2c2b新生态
浅述 思仪 3915A/B/C/D/E/F/G/H 系列EMI测试接收机
沪A、沪B、沪C、沪D……车主的噩梦来了,你两本驾照可能都不够扣!
A:1;B:3;C:4;D:编译错误。package mainimport(
热门
标签
更多标签
云服务器
即时通信 IM
ICP备案
对象存储
实时音视频
活动推荐
运营活动
广告
关闭
领券