腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
1
回答
如
何在
精
益
理论
中
证明
(∀
x
,
p
x
∨
r
)↔(∀
x
,
p
x
)∨
r
?
我的
证明
如下,但它是错误的,我不知道如何纠正这一点 assume h : ∀
x
,
p
x
∨
r
, assume a: α, (assumehl:
p
a, or.inl hl) show
p
a ∨
r
,
浏览 16
提问于2020-02-01
得票数 1
回答已采纳
1
回答
如何从
精
益
中
的基本原理
证明
(∀
x
,
p
x
)→(∃
x
,
p
x
?
、
在“
精
益
中
的定理
证明
”4.4
中
,从第一原则
证明
这个基本含义的
证明
击败了我到目前为止的所有尝试: open classicaltheorem T08
R
: (¬ ∀
x
,
p
x</e
浏览 21
提问于2020-02-02
得票数 2
回答已采纳
1
回答
如
何在
精
益
学习
中
证明
r
→(∃
x
:α,
r
)
、
、
、
我试图
证明
逻辑语句
r
→ (∃
x
: α,
r
),其中
r
是Prop (命题或语句),α是Type。我已经通过书中的练习
证明
了
精
益
中
的一些东西,但我被困在了这一点上。由于不存在类型为α的
x
,无人居住的α不会使这句话成为一种错误的陈述吗?我最大的“尝试”是希望
精
益
的讲述者能填上我需要的东西, theorem t5_2:
r
→ (∃
x
: α,
浏览 8
提问于2019-11-25
得票数 0
回答已采纳
1
回答
如
何在
精
益
学习
中
通过归纳简化
证明
?
、
我想用归纳法简化
精
益
理论
中
的一个
证明
。 我在Lean
中
定义了一个具有3个构造函数的归纳类型,并在此类型上定义了一个二元关系。我之所以包含这些公理,是因为Lean不让我将它们作为rel的构造器。: rel Fintype.a Fintype.b|
r
3 : ∀
p
: Prop, (¬
p</
浏览 33
提问于2019-04-29
得票数 0
1
回答
如何
证明
精
益
中
的分布性(命题有效性属性6)?
、
、
在经历了大多数练习,并在
精
益
手册第3章末尾的
精
益
中
解决/
证明
了前五个命题有效性/性质之后,我仍然无法理解以下含义(
证明
性质6所需的含义之一): theorem Distr_or_L (
p
q
r
:Prop) : (
p
∨ q) ∧ (
p
∨
r
) →
p
∨ (q ∧
r
) := intros pqpr,
浏览 13
提问于2020-01-16
得票数 1
回答已采纳
1
回答
精
益高尔夫:列表游戏Lv2 (is_in_append,is_in_rev)
、
标题是对自然数博弈的敬意,这是一个很好的交互式教程,用来
证明
精
益
中
自然数的某些特性。 这里将重用Lv1
中
使用的定义。:
x
出现在l1 ++ l2
中
当且仅当
x
出现在l1
中
或
x
出现在l2
中
。is_in_rev:如果
x
出现在l
中
,
x
出现在rev l
中
。简单地说,is_in
x
l的值包含了
x
出现在l<
浏览 0
提问于2021-10-13
得票数 9
1
回答
精
益
选择的定义
、
在
中
,“选择”是根据以下原则实施的:axiom choice {α : Sort u} : nonempty α → α 在我看来,这些东西似乎是不一样的。有人能详细说明一下吗?
浏览 0
提问于2019-02-19
得票数 2
回答已采纳
3
回答
GNU Prolog的同义检验器
、
、
、
或(3 power 2) mul (
X
plus 2) equals (9 mul
X
) plus 18.作为结果,我期望的是布尔答案,
如
“是/否”、“等于/不同”、“
证明
已找到/未能找到
证明
”或类似的。
P
.
P
.S .
如
@larsman所指出,根据的说法,没有办法
证明
“所有
浏览 8
提问于2011-08-14
得票数 2
回答已采纳
2
回答
如何知道RDF图是否是倾斜的?
、
、
G1 :_:
X
foaf:knows _:Y _:
X
foaf:knows ex:bob_:
X
foaf:knows ex:bob _:
X
foaf:knows _:
X
提前谢谢。
浏览 6
提问于2020-02-05
得票数 3
回答已采纳
2
回答
如
何在
精
益
中
定义偏序集?
、
、
、
我希望在
精
益
定理
证明
器
中
证明
。首先,我需要定义像偏序集这样的东西,这样我就可以定义infimum/上界。在
精
益
中
是如何做到这一点的?提到了setoid,它们是具有关联的等价关系的类型。
浏览 5
提问于2016-03-27
得票数 1
回答已采纳
1
回答
如
何在
不消除类型的情况下在Coq
中
证明
时在道具上进行模式匹配
、
、
、
、
我试图
证明
排序列表的尾部是在Coq中排序的,使用模式匹配而不是策略:match H in Sorted _ (h::t) return Sorted _ t withinductive i
浏览 17
提问于2017-07-11
得票数 1
回答已采纳
1
回答
Lean
证明
助手中交换环的幂等元
、
、
嗨,我试着在
精
益
证明
助理做一些数学,看看它是如何工作的。我决定和交换环的幂等元一起玩应该很有趣。以下是我尝试过的:definition KR : Type := \Sigma
x
: A,
x
*
x
=
x
A : Type,⊢ has_mul A 所以Lea
浏览 7
提问于2016-06-07
得票数 3
回答已采纳
1
回答
如何执行多个存在消除,所有这些都共享一个单一的多变量通用量化假设?
、
精
益
文档显示了以下两个仅包含单个变量的示例:variables (α : Type) (
p
q : α → Prop) show Q, from h3 h) 在这两种情况下,通用假设(前一个例子
中
的h2,后一个例子
中
的hw )仅依赖于一个变量。现在假设我们得到(我转述一下原
浏览 11
提问于2020-02-29
得票数 1
回答已采纳
1
回答
当相关类型被Idris
中
的lambda抽象时,我如何
证明
一个“看似显而易见”的事实?
、
、
=
p
p
<+> q = Parser (\s => parse
p
s ++(Parser q) (Parser
r
) = ?-- Goal: ---------- {hole4} : Parser (\s =>
p
s ++ q s ++
r
s) =Parser (\s => (<
浏览 3
提问于2014-08-07
得票数 14
回答已采纳
1
回答
如何用Isar
证明
淘汰规则?
以下是一个简单的
理论
:datatype t2 = D | E t1 | F | G "
R
A B" (
x
= D ⟹
P
) ⟹ (⋀z.
x
= E z ⟹
R
⇧+⇧+ z y ⟹
P
) ⟹
P
" using
浏览 2
提问于2018-12-13
得票数 1
回答已采纳
1
回答
精
益
Mergesort利用不断增长的有根据关系
、
、
我试图在
精
益
中
创建mergesort定义,并创建了以下代码: | [] := [] else y :: (merge (
x
::def sndhalf {α: Type} (xs: list α): list α
浏览 1
提问于2018-12-30
得票数 3
回答已采纳
1
回答
销毁策略失败,只能清除为道具
y:b), j
x
= j y ->
x
= y) -> Embeddingdef restrict {a b:Sort u} (
r
:a -> a -> Prop) (e:Embedding b a) (
x
y: b) : Prop := destructmatch e with | Em
浏览 19
提问于2020-03-08
得票数 0
回答已采纳
1
回答
逻辑如
何在
Coq
中
编码?
你可以用元
理论
介绍一个逻辑的公理和规则以及关于它们的理由。例如,您可以在Isabelle发行版的IFOL.thy中看到直观一阶逻辑的编码。All :: ‹('a ⇒ o) ⇒ o› (binder ‹∀› 10) andwhere spec: ‹(∀
x
.
P</em
浏览 1
提问于2020-08-24
得票数 1
回答已采纳
2
回答
如
何在
Coq中使用定义?
有时候,当我
证明
某件事时,我有一个假设
P
x
y,我知道我有一个类似
R
x
:= exists y,
P
x
y的定义。我想加入假设
R
x
,但我不知道怎么做。我试着使用pose proof (
R
x
),但是我得到了某种类型的Prop。有办法吗?
浏览 37
提问于2022-08-04
得票数 0
回答已采纳
1
回答
不同等式
证明
的示例
、
我在Coq
中
寻找一个不同的等式
证明
的例子。给出了一些T型和两个元素
x
,y:t和两个
证明
,
p
1,
p
2 :
x
=y和
p
1<>
p
2。
浏览 2
提问于2017-04-28
得票数 6
回答已采纳
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
EM算法是炼金术吗?
椭圆曲线加解密及签名算法的技术原理及其Go语言实现
从零到壹学习密码学第十七讲:椭圆曲线加解密
UG数控加工编程中的多次分刀加工总结,值得快收藏!
SPSS也能编程?
热门
标签
更多标签
云服务器
ICP备案
实时音视频
即时通信 IM
对象存储
活动推荐
运营活动
广告
关闭
领券