腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
1
回答
如
何在
Coq
中
销毁
一个
函数
(
如
H
:~ (
forall
x
:
X
,
p
x
))?
coq
我一直在尝试证明
Coq
中
的
一个
引理,像这样, Goal
forall
(
X
: Type) (
p
:
X
-> Prop), - intros [
x
B]
浏览 18
提问于2021-04-30
得票数 0
2
回答
Coq
中
的“elim”是如何作用于存在量词的?
coq
、
first-order-logic
我对
Coq
在处理存在主义量化的过程
中
感到困惑。我有
一个
谓词
P
和
一个
假设
H
H
: exists n,
P
n(Some goal)elim
H
.然而,在淘汰之后,当前的目标变成
浏览 3
提问于2015-06-03
得票数 3
回答已采纳
1
回答
使用两个类型为
Coq
依赖类型的列表进行模式匹配
coq
、
dependent-type
我定义了这个
函数
。 Inductive Euc:nat -> Type:=|Rn :
forall
{n:nat}, R -> Euc n -> Euc (S n).如何让
Coq
知道Euc 0是Euc A
浏览 18
提问于2020-09-09
得票数 0
回答已采纳
1
回答
如何与复杂的模式-匹配推理?
coq
Coq
允许编写复杂的模式匹配,但随后对它们进行分解,以便其内核能够处理它们。Require Import List. Import ListNotations.打印f显示
Coq
存储了
一个
更复杂的版本。| _ :: C :: _ => 2 : list bar -> nat问题是,在操作f的证明
中
,
浏览 0
提问于2019-09-17
得票数 2
回答已采纳
2
回答
我如何证明
一个
存在主义目标,要求在
Coq
中有
一个
特定的
函数
?
coq
、
proof
对这里的
coq
来说是全新的。如果没有这样的功能,我怎么能反驳呢?(我会假设通过
一个
矛盾,但我会如何提出
一个
矛盾的假设?)A, B : Set
H
: ∀ b : B, ∃ a : A, f a = b __
浏览 2
提问于2021-06-24
得票数 1
回答已采纳
1
回答
在
Coq
中将随意列表转换为依赖类型列表
coq
、
dependent-type
我在
Coq
中
对list的定义如下: Variable A : Set.In environment
P
: A -> Prop
P
_d
浏览 20
提问于2019-03-14
得票数 3
回答已采纳
1
回答
为什么在
Coq
中
,反演不能用在
一个
普遍限定的假设上?
coq
Theorem not_exists_dist :
forall
(
X
:Type) (
P
:
X
-> Prop), inver
浏览 3
提问于2014-12-22
得票数 1
回答已采纳
1
回答
Coq
中
的"intro ->“是如
何在
上下文中工作的?
coq
我感兴趣的是依赖型定理证明器是如
何在
上下文中进行替换的。我在
Coq
中找到了
一个
叫做"intro ->“的东西,如下所述:
x
,y,z: nat y=z ->
x
=z
x
,z: nat
H
:
x
=z
x
=z 在"intros ->“的应用程序之后。我不知道将
H
:
x
浏览 4
提问于2021-06-28
得票数 0
回答已采纳
1
回答
最大隐式参数与非最大隐式参数的用途
coq
一个
比另
一个
新吗?最大隐式参数只需要创建{},而必须使用Arguments或Implicit Arguments来指定非最大参数。这是否意味着最大隐式参数应该是首选的?
浏览 0
提问于2016-05-13
得票数 6
3
回答
如
何在
Coq
中
证明命题的可扩充性?
coq
我试图证明
一个
关于Prop的替换定理,但我失败得很痛苦。下面的定理能在
coq
中被证明吗?如果不能,为什么不能。Theorem prop_subst: (
P
<-> Q) -> ((f
P
) <-> (f Q))如
何在
Coq
中
证明这样的定理?
浏览 2
提问于2012-06-17
得票数 7
1
回答
Coq
HoTT -如何正确地将定义放入定理
中
?
coq
、
type-theory
如
何在
将定义保留在定理内的同时删除警告? (
h
:
forall
x
:A,
P
x
x
idpath) :
forall
(
x
y:A) (
p
:
x
=
浏览 0
提问于2017-11-17
得票数 1
回答已采纳
1
回答
Coq
中量词的DeMorgan定律
coq
、
quantifiers
、
first-order-logic
、
demorgans-law
我很难用德摩根定律来表示量词,特别是我试着应用
Coq
.Logic.Classical_Pred_Type.的
Coq
.Logic.Classical_Pred_Type,并搜索了StackOverflow (,),但都没有解决这个问题Theorem t3:
forall
(T: Type),
forall
<em
浏览 5
提问于2019-07-04
得票数 0
回答已采纳
1
回答
介绍模式示例(
p
1 &.& pn)不起作用
coq
我正在阅读
Coq
(8.5
p
1)参考手册, Goal
fora
浏览 5
提问于2016-06-24
得票数 1
回答已采纳
1
回答
使用不依赖于匹配值的单个分支重写匹配
coq
我想展示以下内容: match
H
in (_ = y) return y with end= exist (fun n' : nat => n' < n)
x
0 l 在我的上下文中,我有:
H
: ltn n = ltn n
x
0 : nat l :
x
0 < n 哪里 Definition
浏览 40
提问于2020-01-14
得票数 1
回答已采纳
1
回答
如何使用Streicher_K_公理
equality
、
coq
也许是为了展示
一个
简单的事实:Axiom SK:Streicher_K_on_ A
x
(fun
p
:
x
=
x
=> (eq_refl
x
) =
p
).Lemma single_proof :
forall
(y:A)(u
浏览 0
提问于2017-11-11
得票数 4
回答已采纳
1
回答
用
coq
证明列表
中
的所有元素
coq
我如何证明
H
和我的目标对于列表
中
的所有元素都是相同的?
X
: Typel : list
X
______________________________________(1/1)
forall
b :
X
, In b l ->
P</em
浏览 3
提问于2016-09-23
得票数 0
回答已采纳
1
回答
证明一系列步骤终止
coq
、
lambda-calculus
我有
一个
小系统可以重写lambda术语。它具有通常(三)确定性的逐值调用重写规则。我没有把他们列在这里。Variable Term: Type.| StepNone :
forall
t, StarStep
浏览 4
提问于2016-12-15
得票数 1
回答已采纳
1
回答
混淆范畴理论
coq
、
category-theory
; proof_of_src:
forall
f g
h
:A, product f g = Some
h
-> source
h
= source f ; proof_of_idl:
forall
a f:A,我认为这是
一个
同时
浏览 3
提问于2017-07-23
得票数 2
回答已采纳
1
回答
coq
谓词逻辑
中
的证明
coq
、
predicate
、
proof
、
predicates
试图在
coq
中
证明以下内容:证明全称量词分布在合取∀
x
∈A,
P
x
∧Qx⇐⇒(∀
x
∈A,
P
x
)∧(∀
x
∈A,Qx上Parameter (A : Type).Parameter (
P
Q : A -> Prop).Lemma II3: (
forall
x
: A,
P
x
/\ Q
x
)
浏览 2
提问于2018-03-16
得票数 1
2
回答
Coq
证明辅助器
中
的依赖型问题
coq
、
dependent-type
Inductive WF (env : Env) : Exp -> Prop :=| WFVar :
forall
n, In n env -> WF env (EVar n)
Forall
(从根本上说,每个变量和
函数
符号都必须在环境
中
定义。现在,我想定义
浏览 5
提问于2017-04-17
得票数 4
回答已采纳
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
EM算法是炼金术吗?
关于php对抗安全软件
传说中的推土机距离基础,最优传输理论了解一下
最大熵模型原理小结
高手总结!C51编程经验三则
热门
标签
更多标签
云服务器
ICP备案
实时音视频
即时通信 IM
对象存储
活动推荐
运营活动
广告
关闭
领券