如何在Coq中实现forall

在试图理解如何在JS或Ruby中实现implement forall时，我很有兴趣知道它是如何在Coq中实际实现的。也许这将有助于揭示一些问题。通过在谷歌上搜索，我似乎找不到这个定义。主要是在源代码中寻找某个地方的链接。

浏览 32提问于2019-03-01得票数 0

1回答

删除Coq中大小列表的最后一个元素

考虑以下大小列表的类型定义：| nil: forall {A: Set}, listn 0 A我试图为init定义listn函数，它删除了最后一个元素。init (x::[]) = [] init (

浏览 6提问于2022-03-19得票数 1

回答已采纳

1回答

如何将Coq中的“0<d”替换为“in”？

、

如何在Coq中用0 < d代替S d'假设？在Coq中，我有一些恼人的假设，即0 < d，我需要替换它来应用euclid_div_succ_d_theorem来证明euclid_div_theorem作为推论。Theorem euclid_div_theorem : 0 < d -> exists q r : natTheorem euclid_div_succ

浏览 0提问于2016-11-30得票数 3

回答已采纳

1回答

嵌套归纳类型的归纳原理

、

我注意到，我一直在为嵌套(有时相互)的归纳类型重新定义非常相似的归纳原则，因为Coq自动生成的归纳原则太弱了。Coq自动生成T_ind P C1 -> forall t : T, P tforall P : T -> Prop,

浏览 1提问于2017-11-03得票数 4

回答已采纳

1回答

点态可判定性是否意味着完全可判定性？

、

它是否认为，如果我可以为每个特定的P n n__确定一个命题，那么我也可以决定是否forall n, P n？感觉它应该可以通过n进行一些归纳，但是我如何在Coq中证明这一点呢？Lemma dec_forall: (forall n, decidable (P n)) -> decidable (forall

浏览 0提问于2018-04-06得票数 3

2回答

Coq需要什么才能为归纳类型生成淘汰组合器？

Coq的Finite_sets库具有归纳类型，指定某些集合是有限的：| Empty_is_finite : Finite(Empty_set U) forall A:Ensemble U,Lemma Finite_dec (A:Typ

浏览 0提问于2016-09-29得票数 3

2回答

如何在Coq中导入模块？

、、

我在从Coq中的模块导入定义时遇到了问题。我是Coq的新手，但无法使用该语言的参考手册或在线教程解决这个问题。我有一个模块，它定义了有限集的签名和公理，我打算在另一个模块中实现。Axiom axiom_emptyset : forall A : Set, forall a

浏览 1提问于2011-10-26得票数 14

回答已采纳

2回答

Coq中普遍量化的方法

那么，现在我想知道:在具有普遍量化命题的Coq中，这种方法可以推断吗？ : nat, FunctionAntecedent n .Coq < Conjecture QuantifiedMajor : forall n

浏览 4提问于2014-05-06得票数 0

3回答

类型乘积的内射性有意义吗？

、

如何在Coq中证明以下几点？ Goal forall (A B : Type), (A*A = B*B)%type -> A = B. 如果它是不可证明的，那么它可以安全地添加为公理吗？

浏览 28提问于2019-12-26得票数 1

2回答

我如何证明一个存在主义目标，要求在Coq中有一个特定的函数？

、

对这里的coq来说是全新的。如果没有这样的功能，我怎么能反驳呢？所以，我想知道的是：一般来说，我如何构造一个函数来为一个存在主义目标提供见证？(我还想证明所有内射函数都有一个左逆)

浏览 2提问于2021-06-24得票数 1

回答已采纳

1回答

在Coq中构建类层次结构？

、、、

我可以使用类型类在Coq中天真地构造代数结构的层次结构。我在寻找有关Coq的类型类的语法和语义的资源时遇到了一些麻烦。然而，我相信下面是半群，么半群和交换么半群的正确实现： op_associative: forall x : A, op x id = x我真

浏览 1提问于2011-11-03得票数 10

回答已采纳

1回答

提升Coq中的existentials

这个引理能在Coq中被证明吗？Lemma liftExists : forall (P : nat -> nat -> Prop), -> exists(f : nat -> nat), forall n:nat, P n (f n).如果Coq不能证明这个引理，那么forall n:nat, exists p:nat, P n p的含义是什么？在构造性数学中，它意味

浏览 17提问于2019-03-01得票数 1

回答已采纳

3回答

如何在Coq中证明命题的可扩充性？

下面的定理能在coq中被证明吗?如果不能，为什么不能。Theorem prop_subst: (P <-> Q) -> ((f P) <-> (f Q))如何在Coq中证明这样的定理？

浏览 2提问于2012-06-17得票数 7

1回答

如何在Coq中表示子集关系？

、

如何在Coq中描述一个集合Y是另一个集合X的子集Definition subset (Y X:Set) : Prop :=有没有一种在Coq中定义subset的简单方法？

浏览 6提问于2016-07-24得票数 5

回答已采纳

1回答

在依赖类型的表达式中重写术语失败，原因未知

Lemma lemma : forall e : t, x = y. intro e; trivial.End foo.当您用rewrite prop替换rewrite prop2时，coq失败并出现隐含错误。然而，在我的观点中，coq应该在重写步骤之后产生forall e : t, True。有人能帮我吗？

浏览 0提问于2011-11-17得票数 3

1回答

m) =假-> m <= n( Coq )？

、

如何在Coq中证明forall n m : nat, (n <? m) = false -> m <= n？执行SearchAbout ltb会产生ltb_lt: forall n m : nat, (n <? m) = true <-> n < m，但我不知道如何应用它，因为它只处理(n <?

浏览 0提问于2015-01-25得票数 1

回答已采纳

1回答

如何证明或伪造“`forall (P，q:支柱)，(P -> Q) -> (Q -> P) -> P=q.”？

、、、、

我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。我认为这可能是因为coq证明了独立性(我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知)，coq使得证明1=2 ->假是不可能的。但是，如果是这样的话，为什么还要消除证据的内容呢？Theorem iff_eq : forall (P Q : Prop), (P -> Q) -> (Q ->

浏览 0提问于2014-10-26得票数 8

回答已采纳

2回答

Coq中的“elim”是如何作用于存在量词的？

、

我对Coq在处理存在主义量化的过程中感到困惑。我有一个谓词P和一个假设HH : exists n, P n(Some goal)elim H.然而，在淘汰之后，当前的目标变成它看起来像是Coq将一个存在量词转换为一个通用量词。如果“forall”1和“存在”1不是等价的，那么Coq为什么要进行这样的

浏览 3提问于2015-06-03得票数 3

回答已采纳

2回答

Coq:使用带替换的及物性

、、

我想在Coq中证明这个引理：b : Typeg : a -> b______________________________________(1/1)(forall x : a, g x = h x) -> forall x : a, f x = h x 我知道Coq.Relations.Relation_Definiti

浏览 4提问于2014-04-02得票数 5

回答已采纳

2回答