Coq:两个等价setoid之间的重写
Coq是一个交互式定理证明助理，用于形式化验证和证明数学定理。它基于构造性类型论，提供了丰富的逻辑和证明工具，可以用于验证各种数学和计算机科学领域的定理。
在Coq中，重写是一种基本的推理技术，用于在等价的setoid（即具有等价关系的类型）之间进行转换。重写允许我们根据等价关系的定义，将一个表达式替换为另一个等价的表达式，从而简化证明过程。
重写在形式化验证中具有广泛的应用场景，例如证明等价性、简化表达式、化简证明目标等。通过使用Coq的重写机制，我们可以确保证明的正确性，并且可以自动化一些繁琐的证明步骤。
腾讯云提供了一系列与云计算相关的产品，其中与Coq相关的产品可能包括云服务器、容器服务、人工智能平台等。这些产品可以帮助用户在云上部署和管理Coq环境，提供高性能的计算和存储资源，以及强大的人工智能算法和工具支持。
以下是一些腾讯云产品的介绍链接，可以了解更多相关信息：
- 云服务器（ECS）：提供可扩展的计算资源，用于部署和运行Coq环境。 链接：https://cloud.tencent.com/product/cvm
- 容器服务（TKE）：提供容器化的部署和管理环境，方便用户快速搭建Coq环境。 链接：https://cloud.tencent.com/product/tke
- 人工智能平台（AI Lab）：提供丰富的人工智能算法和工具支持，可用于辅助Coq的验证和证明过程。 链接：https://cloud.tencent.com/product/ailab
请注意，以上链接仅供参考，具体的产品选择应根据实际需求和情况进行。
相关·内容
1回答
我很难理解类别的以下Coq定义(定义了)，这涉及到Setoid。我不明白为什么需要Setoid，也不明白它在这里扮演的角色。
Class Category O `{!Arrows O} `{∀ x y: O, Equiv (x ⟶ y)}
`{!CatId O} `{!CatComp O}: Prop :=
{ arrow_equiv :> ∀ x y, Setoid (x ⟶ y)
; comp_proper :> ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z)
; comp_assoc :>
浏览 0提问于2016-11-06得票数 3
1回答
我想系统地删除所有可能出现在我的假设和目标中的双重否定。我知道~~A -> A不是直觉逻辑的一部分，但我所选的课程是经典的，所以我不介意。
我知道上述公理可以被Coq.Logic.Classical_Prop.NNPP访问，但是这个公理无助于从更复杂的句子中删除双重否定，比如例如
H : ~ ~ A \/ (B /\ ~ C)
最好我能在H上使用Ltac战术，这样它就能转化为
H1 : A \/ (B /\ ~C)。
任何帮助写这样的策略或任何其他建议都是非常感谢的。
浏览 3提问于2018-10-29得票数 1
回答已采纳
我不能用Ssreflect用setoids重写。虽然我不认为这些信息与解决问题相关，但我在coq：中使用了这个范畴理论的公式。
据我所知，如果能够解决合适的RewriteRelation Typeclass实例，defined的重写可以使用用户定义的等价关系。
Context { x y : obj[C]}.
About RewriteRelation.
(* ∀ A : Type, crelation A → Prop *)
Instance equivrw : (@RewriteRelation (x ~> y) (@equiv (x ~> y) (homset x y))
浏览 2提问于2020-02-02得票数 1
我有两个setoid和bisimilar： lang_iff的定义 Definition lang := str -> Prop.
Definition lang_iff (s1 s2: lang): Prop :=
forall (s: str),
s \in s1 <-> s \in s2. setoid lang_setoid Add Parametric Relation: lang lang_iff
reflexivity proved by lang_iff_refl
symmetry proved by lang_iff_sym
trans
浏览 24提问于2021-02-01得票数 0
回答已采纳
1回答
有时，我需要在不破坏鉴别器的前提下，在一个分支中应用简化。
From Coq Require Import Setoid.
Lemma true_and :
forall P, True /\ P <-> P.
Proof.
firstorder.
Qed.
Goal (forall (b:bool) P Q, if b then True /\ P else Q).
intros.
Fail rewrite (true_and P).
Abort.
在本例中，rewrite失败(setoid_rewrite也失败)，建议注册以下内容
"subrelat
浏览 2提问于2021-04-20得票数 4
1回答
我想证明对于任何自然数，n+1都大于0。
定义我自己的大于函数，这样可以很好地工作：
Fixpoint my_gt (n : nat) (m : nat) : bool
:= match n with
| O => false
| S n' => match m with
| O => true
| S m' => my_gt n' m'
end
end.
Lemma GT1: forall n, my
浏览 4提问于2014-04-25得票数 0
1回答
我要证明以下定理：
Theorem T5:
forall s t, (forall u, OoS s u <-> OoS t u) -> s = t.
我目前的背景和目标是：
1 subgoal
s, t : Entity
H : forall u : Entity, OoS s u <-> OoS t u
______________________________________(1/1)
(forall v : Entity, OoS s v <-> OoS s v \/ OoS t v) /\
(forall v : Entity, OoS
浏览 10提问于2022-05-29得票数 0
回答已采纳
1回答
我有一个简单的列表引理，它说n::l = [n]++l，它的证明如下所示。
Lemma cons_to_app : (forall (n: nat) (l: list nat), n :: l = [n] ++ l).
Proof.
simpl. reflexivity.
Qed.
现在我想使用这个证明，重写cons term，::，它们出现在证明目标中的任何地方。
Lemma easy_lemma : forall (n : nat) (xs ys : list nat), (n::xs) ++ (n::ys) = (n::xs) ++ ([n] ++ ys).
我想将(n::ys)重
浏览 27提问于2019-06-21得票数 1
回答已采纳
下面是一个更大的证明的简化片段，它捕获了有问题的行为。
Section foo.
Parameter t : Type.
Parameter x : t.
Parameter y : t.
Parameter prop : x = y <-> True.
Parameter prop2 : x = y.
Lemma lemma : forall e : t, x = y.
rewrite prop2.
intro e; trivial.
Qed.
End foo.
当您用rewrite prop替换rewrite prop2时，coq
浏览 0提问于2011-11-17得票数 3
2回答
我试图使用以下语法定义一个名为isVector的实体
Require Export Setoid.
Require Export Coq.Reals.Reals.
Require Export ArithRing.
Definition Point := Type.
Record MassPoint:Type:= cons{number : R ; point: Point}.
Variable add_MP : MassPoint -> MassPoint -> MassPoint .
Variable mult_MP : R -> MassPoint ->
浏览 0提问于2018-11-24得票数 1
回答已采纳
我已经尝试了很长一段时间来解决以下问题。
Require Import
Coq.Classes.Morphisms
MathClasses.interfaces.abstract_algebra
MathClasses.interfaces.vectorspace
MathClasses.misc.workaround_tactics
MathClasses.theory.setoids
MathClasses.theory.groups.
Lemma f_equiv' `{Equiv A} `{f : A -> A} :
f = f -> f
浏览 5提问于2022-09-02得票数 1
回答已采纳
我在使用setoid_rewrite策略重写时遇到了问题。在下面的实例声明中，我期望setoid_rewrite fmapComp将fmap iso ∘ fmap inv重写为fmap (iso ∘ inv)。然而，Coq报告说，在重写期间“没有取得任何进展”：
Instance functorsPreserveIsomorphisms
`{C : Cat o η} `{D : Cat u ρ}
{a b : o} {φ : o → u} (F : Functor C D φ) (I : a ≅ b) : φ a ≅ φ b.
Proof.
apply (Build_Isomorp
浏览 8提问于2011-11-14得票数 4
回答已采纳
我试图从字段的公理中直接证明简单的字段属性。在对Coq的原生字段支持()进行了一些实验之后，我决定最好简单地写下这10个公理，并使其自成体系。当我需要在我自己的==操作符中使用==时，我遇到了一个困难，这个操作符自然无法工作。我意识到我必须添加一些公理，我的==是自反的，对称的，传递性的，但是我想知道这是否就是它所需要的？或者有一种更简单的方法来将rewrite与用户定义的==一起使用？这是我的Coq代码：
Variable (F:Type).
Variable (zero:F).
Variable (one :F).
Variable (add: F -> F -> F).
Va
浏览 0提问于2019-05-12得票数 2
回答已采纳
给定任何编程语言，只要存在标准库函数，我们很可能就应该使用它，而不是编写自己的代码。人们会认为，这一建议同样适用于Coq。然而，我最近强迫自己使用same_relation谓词的Relation模块，我留下的感觉是更糟的。所以我肯定遗漏了什么，所以我的问题。为了说明我的意思，让我们考虑一下可能的关系：
Require Import Relations. (* same_relation *)
Require Import Setoids.Setoid. (* seems to be needed for rewrite *)
Inductive rel1 {A:Type} : A
浏览 6提问于2016-06-18得票数 3
回答已采纳
1回答
如何将Coq中的nat转换为q (Rational)？
我想写这样的东西：
Require Import Coq.QArith.QArith.
Open Scope Q_scope.
Definition a := 2/3.
当我尝试这样做时，Coq告诉我：
Error: The term "2" has type "nat" while it is expected to have type "Q".
浏览 2提问于2015-09-22得票数 1
回答已采纳
2回答
我正在试验Coq字段模块，试图从字段公理中直接证明以下简单的标识：forall v, 0v == v。我看到0和==都有现有的符号，所以我尝试了(但失败了)：
(***********)
(* IMPORTS *)
(***********)
Require Import Coq.setoid_ring.Field_theory.
(*********************)
(* forall v, 0v == v *)
(*********************)
Lemma mul_0_l: forall v,
("0" * v "=="
浏览 2提问于2019-05-10得票数 1
回答已采纳
2回答
我基于公理证明了字段的一些基本性质，现在我继续定义向量空间的公理。特别是，Field.v包含以下行：
(***********)
(* IMPORTS *)
(***********)
Require Import Setoid Morphisms.
Variable (F:Type).
Variable (zero:F).
Variable (one :F).
Variable (add: F -> F -> F).
Variable (mul: F -> F -> F).
Variable (eq: F -> F -> Prop).
我在一个名为V
浏览 0提问于2019-05-18得票数 1
回答已采纳
1回答
我有一个引理的形式FnEquivInner f g暗示outer t (bind t f) === outer t (bind t g) (完整的例子张贴在下面)。
我希望了解我需要为outer编写什么样的outer实例，在本例中，它允许我执行一个rewrite，以便在outer调用中用g替换f。
通常，如何编写模式非平凡的Proper实例？
Require Import Setoid.
Require Import Morphisms.
Section PROPERINSTANCE.
Variable T: Type.
Variable inner: T -> (T -&
浏览 0提问于2018-06-22得票数 2
回答已采纳
我遇到了一种使用setoid_replace的奇怪情况，其中表单的一个验证步骤：
setoid_replace (a - c + d) with b by my_tactic
在Error: No matching clauses for match goal中失败，但在该策略中附加额外的idtac之后：
setoid_replace (a - c + d) with b by (my_tactic; idtac)
证明成功了。我对idtac的理解是，它本质上是一种禁止操作。为什么idtac的存在在这里产生了不同的影响？
这是完整代码。我正在使用Coq 8.4pl6通过验证将军。
Requir
浏览 3提问于2015-07-07得票数 3
回答已采纳
1回答
传统上，Haskell中的函子应该支持同一性和构图规律。在Agda中，这些法律应该正式化，但是标准库只提供RawFunctor的(即没有法律的fmap )。在函子正规化的过程中，出现了几个问题：
函子一般应该支持同余吗？
是的:在任意的Setoid或只是Relation.Binary.PropositionalEquality.setoid上
是的:函子应该接受或提供Function.Equality.Π吗？
否:身份法应支持哪些身份功能？所有这些(即(id′ : A → A) → id′ ≗ id)？
否:函数应该如何要求一个支持同余的函子？
不:什么(真实世界？)函子不
浏览 5提问于2014-03-05得票数 1
1回答
函数是否有一种方法来要求两个Setoids，其中第一个Setoid中的相等意味着后者中的相等？当然，这需要两个Setoid共享它们的Carrier，而Carrier不是一个参数，而是一个记录字段。类型检查器拒绝了请求Carrier等式的天真尝试：
f : {S₁ S₂ : Setoid _ _} → Setoid.Carrier S₁ ≡ Setoid.Carrier S₂ →
({x y : Setoid.Carrier S₁} → Setoid._≈_ S₁ x y → Setoid._≈_ S₂ x y ) → ...
这不起作用，因为我们在等式证明上不匹配模式，因此不同的Car
浏览 3提问于2014-01-16得票数 1
回答已采纳
我要证明以下定理：
Theorem T14 : forall s t u,
S u s t <-> S u t s.
其中S的定义如下：
Definition S u s t := forall v,
((ObS u v) <-> (ObS v s \/ ObS v t)).
我使用的第一种策略是：
Proof.
intros s t u.
unfold S.
我现在的目标是：
1 subgoal
s, t, u : Entity
______________________________________(1/1)
(forall v : Entity
浏览 8提问于2022-04-20得票数 0
回答已采纳
1回答
在Coq中表示n m : nat是相邻偶数的一种可能的方法是归纳地定义这种关系，从0和2开始。
Inductive adj_ev : nat -> nat -> Prop :=
| ae_0 : adj_ev 0 2
| ae_1 : forall ( n m : nat ), adj_ev n m -> adj_ev m ( S ( S m ) )
| ae_2 : forall ( n m : nat ), adj_ev n m -> adj_ev m n.
ae_0表示0和2是相邻的偶数。ae_1指出，如果某些n m : nat是相邻的偶数，那么m和m + 2也是
浏览 4提问于2014-07-16得票数 1
回答已采纳
1回答
我正在使用agda的开发版本，它现在与基本标准库版本1.3不兼容。
wmacmil@w:~/.agda$ agda --version
Agda version 2.6.2-41b6b25
一个基本的failure.agda文件，
module failure where
open import Data.String
失败：
Checking failure (/home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/failure.agda).
Checking Data.String
浏览 3提问于2020-09-17得票数 1
回答已采纳
我只是从Coq开始，现在正试图证明一些在“小普罗弗”中的东西。我遇到的一个定理是：
Theorem equal_swap : forall (A: Type) (x:A) (y:A),
(x = y) = (y = x).
然而，我无法证明这一点。我试着找出如何用eq_sym重写方程的右侧，但我无法将它应用于目标的一个表达式。
我该如何证明这个定理？
浏览 0提问于2019-05-02得票数 0
回答已采纳
2回答
我已经证明了许多从实公理开始的定理，现在我想把自然法定义为Reals的一个子集，并重用所有已证明的定理。怎么做呢？下面是一个人工的MRE，它使用适当的coq设计实践编译：
01 (* CReal Definitions *)
02 Parameter CReal: Set.
03 Parameter creal_add : CReal -> CReal -> CReal.
04 Axiom creal_comm: forall x y:CReal, creal_add x y = creal_add y x.
05
06 (* CNat Definitions *)
浏览 6提问于2020-03-18得票数 0
回答已采纳
3回答
与功能扩展作斗争
、、
我用Coq编程已经有几个月了。特别是，我对函数式编程证明很感兴趣，因为函数无处不在(光学、状态单等)。从这个意义上说，处理功能扩展已经变得非常重要，尽管非常烦人。为了说明这种情况，让我们假设一个简单的Monad (只定义了一个定律)：
Class Monad (m : Type -> Type) :=
{ ret : forall {X}, X -> m X
; bind : forall {A B}, m A -> (A -> m B) -> m B
}.
Notation "ma >>= f" := (bind ma f) (at
浏览 1提问于2018-03-28得票数 2
回答已采纳
我正在使用。
我想打印setoid_rewrite当前可用的setoid和态射，以便更好地了解重写失败时缺少哪种关系或函数。有什么办法吗？
浏览 0提问于2016-07-09得票数 2
回答已采纳
假设我定义了这个集合。
Inductive Set_1 : Set :=
| Constr_1 : Set_1
| Constr_2 : Set_1.
有可能证明这一说法吗？
(Constr_1 = Constr_2) = False
如果是这样，我应该使用什么策略？这可能对autorewrite很有用。
浏览 2提问于2013-01-15得票数 1
回答已采纳
我试图使用类型类来实现代码重用，但在子类型类定理中应用父类型类公理时，我遇到了setoid错误。我用下面的相等和加法操作做了一个MRE： Require Import Setoid.
(* Equality *)
Parameter CEq : forall A, A->A->Prop.
Arguments CEq [A] _ _.
Notation "x ¦ y" := (CEq x y) (at level 70, no associativity).
Axiom ceq_reflexivity: forall A, forall a:A, a¦a.
Axi
浏览 13提问于2020-03-30得票数 0
回答已采纳
给出以下公理：
Definition Axiom1 : Prop := forall (a b:Type) (f g: a -> b),
(forall x, f x = g x) -> f = g.
Definition Axiom2 : Prop := forall (a:Type) (B:a -> Type) (f g: forall x, B x),
(forall x, f x = g x) -> f = g.
可以很容易地证明，Axiom2是比Axiom1更强大的公理
Theorem Axiom2ImpAxiom1 : Axiom2 -&
浏览 5提问于2018-01-14得票数 1
回答已采纳
我们可以将Coq中的分配给Prop、Set和每个Type_i吗？我只在Coq的库中看到了的定义，所以也许我们首先需要大基数的定义。
根据证明无关的语义，例如暴露的，Set和Type_i形成一个递增的序列。这可以在Coq中得到证明吗？
由于不可预测性，Prop看起来更复杂。证明无关意味着我们识别同一P : Prop的所有证明，并将Prop本身解释为{false, true}对。因此，Prop的基数应该是2。但是，对于任何两个证明p1 p2 : P，Coq不接受eq_refl p1作为p1 = p2的证明。因此，Coq并不能完全识别p1和p2。另一方面，不可预测性意味着对于任何A : Type和P
浏览 13提问于2018-08-28得票数 4
回答已采纳
1回答
如何让Coq识别出两种类型，每种类型都是从使用相同参数从模块函子创建的模块中导入的，但出现在不同的模块中，它们实际上是相同的类型？
极小例子
Module Type S.
End S.
Module F (s : S).
Inductive foo : Type := a.
End F.
Module G (s : S).
Include F s.
End G.
Module H (s : S).
Include F.
End H.
Module I (s : S).
Module G := G s.
Module H := H s.
(* This is a type error
浏览 1提问于2020-05-25得票数 2
回答已采纳
Coq是8.10.2版本，我使用jwiegley创建的库。
定义了目标为欧氏空间，箭头为参数函数(P，->，A，->，B)的范畴。参数P是任意欧氏空间，而不是范畴对象。
这是我写的代码。类别类的定义是
Require Import Coq.Reals.Reals.
Require Import Category.Theory.
Inductive Euc:nat -> Type:=
|RO : Euc 0
|Rn : forall n:nat, R -> Euc n -> Euc (S n).
Record SuperEuc := {
dim : nat;
}
浏览 2提问于2020-08-09得票数 1
回答已采纳
我正在用Coq证明一些关于超滤光片的基本事实，我的许多证明最终都达到了我必须证明目标的阶段，例如
(False -> False) = True
或
False /\ P = False
或
True
或者其他一些琐碎的重言之词。simpl和auto似乎都没有做任何事情，所以我如何解决这些Prop目标？
浏览 0提问于2021-03-16得票数 0
回答已采纳
我正致力于用coq规范群论。我有两个档案：
V-包含群的定义和定理
groups_Z.v -包含Z群的定理和定义。
第五组：
Require Import Coq.Setoids.Setoid.
Require Import Coq.Lists.List.
Require Import PeanoNat.
Class Semigroup G : Type :=
{
mult : G -> G -> G;
assoc : forall x y z:G,
mult x (mult y z) = mult (mult x y) z
}.
浏览 3提问于2021-01-26得票数 0
回答已采纳
2回答
在HOTT和COQ中，人们无法证明UIP，即
\Prod_{p:a=a} p= refl
但可以证明：
\Prod_{p:a=a} (a，p) = (a，参a)
为什么这个定义是这样的？是因为一个人想要有一个很好的同伦解释吗？还是有什么自然的，更深层次的原因来定义这个定义？
浏览 7提问于2017-10-25得票数 4
回答已采纳
我是coq的初学者。
我不知道intros [=]和intros [= <- H]是什么意思。我找不到一个简单的解释。有人能给我解释一下这两个吗？
问候
浏览 1提问于2021-06-21得票数 1
这应该是一个简单的问题。我是Coq的新手
我想在Coq中定义异或(据我所知，它不是预定义的)。重要的部分是允许多个命题(例如Xor A、B、C、D)。
我还需要这两个属性：
(Xor A1 A2 ... An)/\~A1 -> Xor A2... An
(Xor A1 A2 ... An)/\A1 -> ~A2/\.../\~An
我目前在为未定义数量的变量定义函数时遇到了问题。我试着手动定义两个、三个、四个和五个变量(这就是我需要的数量)。但是，证明这些性质是一件痛苦的事情，而且效率似乎非常低。
浏览 0提问于2011-07-20得票数 5
回答已采纳
我正在尝试定义具有多个参数而不是商类型的函数。使用currying，我可以将问题简化为在逐点产品setoid上定义函数：
module Foo where
open import Quotient
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (proof-irrelevance)
private
open import Relation.Binary.Product.Pointwise
open import Data.Product
_×-q
浏览 2提问于2012-05-13得票数 8
回答已采纳
1回答
我在Coq中寻找一个不同的等式证明的例子。
这意味着：
给出了一些T型和两个元素x，y:t和两个证明，p1，p2 : x=y和p1<>p2。
浏览 2提问于2017-04-28得票数 6
回答已采纳
1回答
我正在读“代数驱动的设计”这本书，在第二章中，我开始设计一个简单的代数系统，如下所示： data Tile
haskell :: Tile
sandy :: Tile
cw :: Tile -> Tile
∀ (t :: Tile).
cw (cw (cw (cw t))) = t 然后它就从那里开始积累。所以我想如果我可以使用一个证明助手来跟随它会很好。 我看到有人用Coq这样做，我认为在here中也可以这样做，但我不知道如何定义一个公理，就像Coq示例(Axiom cw : Tile -> Tile.)中定义的那样。 请记住，我对在这里实际实现函数并不感兴趣，我只需
浏览 12提问于2021-08-07得票数 0
回答已采纳
我使用了从Coq到OCaml的提取，其中有Z、N、positive类型。
我不需要在int of OCaml中提取它。
那么提取后的类型是：
type positive =
| Coq_xI of positive
| Coq_xO of positive
| Coq_xH
type coq_N =
| N0
| Npos of positive
type coq_Z =
| Z0
| Zpos of positive
| Zneg of positive
我在OCaml中有一个程序，其中一些函数使用OCaml类型的string。
在我的OCaml程序中，我需要编写一些转换类型的函数：st
浏览 1提问于2014-09-02得票数 2
回答已采纳
在文件SemiRing.v中，我定义了一些类：
(** Setoids. *)
Class Setoid := {
s_typ :> Type;
s_eq : relation s_typ;
s_eq_Equiv : Equivalence s_eq }.
Existing Instance s_eq_Equiv.
Module Import Setoid_Notations.
Infix "==" := s_eq.
End Setoid_Notations.
Instance Leibniz_Setoid (A : Type) : Setoid.
浏览 0提问于2014-02-21得票数 0
回答已采纳
1回答
问题是，如果我知道forall x, f x ≡ g x (其中≡是一些等价关系，而f，g，是函数)，那么正确的Proper实例是什么，它将允许我用更大的条件用g重写通过等价关系联系起来的f？
假设功能扩展是可用的，如果需要的话--我猜这是必需的吗？
一些示例代码可以更好地演示这个问题：
Require Import Setoid.
(** Feel free to assume FunExt *)
Require Import FunctionalExtensionality.
Section FOOBAR.
Variable T: Type.
Variable f: T ->
浏览 0提问于2018-06-20得票数 2
回答已采纳
是否有一种方法可以方便地使用EqReasoning的多个实例化，其中底层的Setoid不一定是语义相等的(即不能使用≡-Reasoning )？≡-Reasoning之所以方便，是因为类型参数是隐式的，它通过自动选择语义相等来唯一地确定正在使用的Setoid。当使用任意的Setoid时，没有这样的唯一选择。然而，许多结构提供了一种标准的方法来提升Setoid
Data.Maybe和Data.Covec有一个setoid成员。
Data.Vec.Equality.Equality提供了足够的定义来为Vec编写规范的Setoid提升。有趣的是，在Relation.Binary.Vec.Po
浏览 7提问于2014-01-17得票数 1
回答已采纳
我正在学习同伦型理论(HoTT)及其与COQ的关系。尤其是路径归纳法中的同一性概念对我来说仍然是神秘的。
因此，我用COQ做了一些实验。
让我们从使用路径归纳的标准相等类型的简单引理开始：
Lemma eq_sym: forall (x y:nat), x = y -> y = x.
intros.
apply (match H in (_ = y0) return y0 = x with eq_refl => eq_refl end).
Defined.
现在让我们看看这是否是COQ "eq“类型的特殊处理。因此，让我们用类似的对称引理定义一个新的相等类型(仅适用于nat
浏览 0提问于2016-02-01得票数 0
回答已采纳
2回答
用归纳法证明了Coq中的两个阶乘函数是等价的。
大小写n = 0比较简单，但归纳情况比较复杂。我明白了，如果我能把(visit_fac_v2 n' (n * a))重写成n * (visit_fac_v2 n' a)，我就完事了。然而，将这一想法转化为Coq会给我带来麻烦。
如何在Coq中证明这一点呢？
Fixpoint fac_v1 (n : nat) : nat :=
match n with
| 0 => 1
| S n' => n * (fac_v1 n')
end.
Fixpoint visit_fac_v2 (n a
浏览 6提问于2016-11-13得票数 2
回答已采纳
在我看来，在ssreflect中，当我们进行依赖模式匹配时，隐式构造函数字段会变成显式字段，而设置各种隐式选项并不会影响这种行为。
以下代码适用于Coq 8.6：
Require Import Coq.Unicode.Utf8.
Set Implicit Arguments.
Set Contextual Implicit.
Inductive Vec (A : Type) : nat → Type :=
nil : Vec A 0
| cons : ∀ {n}, A → Vec A n → Vec A (S n).
Fixpoint append {A n m}(xs : Vec
浏览 38提问于2017-03-17得票数 3
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
实时音视频
即时通信 IM活动推荐
腾讯云开发者
