如何表示归纳关系中的一个元素不能从Coq中的另一个元素派生？
在Coq中，表示归纳关系中一个元素不能从另一个元素派生的方法是使用不可派生关系（Inference rules）或者排斥中间子句（Disjunction）。
不可派生关系是一种用于定义无法从一个元素到另一个元素的派生关系的方式。通过明确规定这样的关系是不存在的，我们可以排除某些不合法的推理。
排斥中间子句是一种逻辑推理中的方法，用于排除某些不合法的情况。在表示归纳关系时，通过排斥中间子句，可以阻止从一个元素派生出另一个元素。
以一个简单的例子来说明，假设我们有一个归纳类型Nat，表示自然数，其中包括0和后继（successor）操作。我们希望表示0不是任何自然数的后继。
使用不可派生关系的方法，我们可以定义一个性质NoSuccessor，表示一个自然数没有后继：
Inductive Nat : Type :=
| Z : Nat
| S : Nat -> Nat.
Inductive NoSuccessor : Nat -> Prop :=
| NoSuccessorZ : NoSuccessor Z.这样，NoSuccessor Z 表示 0 没有后继。
使用排斥中间子句的方法，我们可以定义一个归纳类型Not，表示不成立的命题。然后，我们可以使用排斥中间子句来排除一个元素是另一个元素的后继的情况：
Inductive Nat : Type :=
| Z : Nat
| S : Nat -> Nat.
Inductive Not (P : Prop) : Prop :=
| Not_intro : P -> Not P -> Not P.
Inductive NotSuccessor (n : Nat) : Prop :=
| NoSuccessor : Not (exists n', S n' = n) -> NotSuccessor n.这样，NotSuccessor Z 表示 0 不是任何自然数的后继。
这里介绍了两种表示归纳关系中一个元素不能从另一个元素派生的方法。具体选择哪种方法取决于具体的情况和需求。
相关·内容
在Coq标准库中，我可以找到一个引理，说明inl和inr是注入吗？也就是，forall (A B : Type)(x y : A), inl B x = inl B y -> x = y，类似于右边的情况.我自己证明这一点没有问题，但这些似乎是非常有用和重要的引理，我不得不想象它们已经在标准库的某个地方了。
浏览 3提问于2015-09-10得票数 2
回答已采纳
1回答
我想证明在Coq中减法不通勤，但我被卡住了。我相信我想在Coq里证明的声明是写在forall a b : nat, a <> b -> a - b <> b - a上的
到目前为止，这是我的证据。
Theorem subtraction_does_not_commute :
forall a b : nat, a <> b -> a - b <> b - a.
Proof.
intros a b C.
unfold not; intro H.
apply C.
我想我可以用C : a <> b来反驳a =
浏览 0提问于2017-05-18得票数 1
回答已采纳
1回答
我注意到，我一直在为嵌套(有时相互)的归纳类型重新定义非常相似的归纳原则，因为Coq自动生成的归纳原则太弱了。下面是一个非常简单的示例：
Require Import Coq.Lists.List.
Inductive T : Set :=
| C1 : T
| C2 : list T -> T.
Section T_nested_ind.
Variable P : T -> Prop.
Hypothesis C1_case : P C1.
Hypothesis C2_case : forall l : list T, Forall P l -> P (C2
浏览 1提问于2017-11-03得票数 4
回答已采纳
1回答
在做了很多教程之后，尝试创建我的第一个Coq定义。想知道如何定义像字母表这样简单的东西，如果定义是：
Σ是一个字母表当且仅当它是一组有限的非空符号。
得到了这么多：
Require Import Coq.Lists.ListSet.
Definition alphabet := set.
但是，您如何指定“必须是有限的、非空集”部分？
浏览 4提问于2015-07-19得票数 2
回答已采纳
我想证明莱玛·RnP_eq。 From mathcomp Require Import ssreflect.
Require Import Coq.Program.Equality.
Definition func {n m l o:nat}
(I:t R 0 -> t R m -> t R l)(J:t R n -> t R l -> t R o):=
(fun (x:t R n)(a:t R m) => J (snd (splitat 0 x)) (I (fst (splitat 0 x)) a)).
Lemma deriveP_eq (n
浏览 19提问于2020-10-26得票数 1
回答已采纳
我有一个术语重写系统( A，→)，其中A是一个集合，→是A上的一个嵌入二进制关系，给定A的x和y，x→y表示x降为y。
为了实现一些属性，我只使用来自Coq.Relations.Relation_Definitions和Coq.Relations.Relation_Operators的定义。
现在，我要将以下属性正式化：
a0 a1→.
我怎样才能在Coq中实现这一点呢？
浏览 1提问于2017-05-14得票数 3
回答已采纳
我在一些教程中读到if a then b else c代表match a with true => b | false => c end。但是，前者非常奇怪地不检查a的类型，而后者当然确保a是一个布尔值。例如,
Coq < Check if nil then 1 else 2.
if nil then 1 else 2
: nat
where
?A : [ |- Type]
Coq < Check match nil with true => 1 | false => 2 end.
Toplevel input, characters 33-
浏览 1提问于2017-12-25得票数 4
回答已采纳
1回答
我假设Coq会在某一时刻转向LCF方法。在过去，我对感到好奇。我在一篇总结了现有文献的硕士论文中找到了对Isabelle/Pure的一些很好的描述。
我想知道是否有关于Coq内核的描述，涵盖了它的逻辑和实现方面。
浏览 0提问于2020-03-06得票数 0
我想把我之前写的Maude代码翻译成Coq，因为Coq比Maude有更强大的表达式。
我不知道如何表示以下代码：
如上所示，GuardPostfix1，GuardPostfix有三个子类： GuardPostfix2和GuardPostfix3.
我使用归纳类型来表示GCcomponent。但是，在定义类型GuardPostfix1 GComponent时，GComponent1有两个构造函数，分别使用构造函数和GuardPostfix2。
如何在Coq中定义这些类型？
浏览 0提问于2018-02-03得票数 1
1回答
在我的Coq研究中经常会出现这样的证明状态：
1 goal
n : nat
IHn : fib_v1 n <= fib_v1 (S n)
______________________________________(1/1)
fib_v1 (S n) <= fib_v1 (S (S n))
Coq抱怨说它不能把n和S n统一起来，S n和S (S n)不能统一。在纸和笔中，很容易在目标中引入象征性的操作，比如t = S n，甚至n = S n，那么归纳假设就会变得适用。在Coq看来不是这样的。在这样的情况下，一个人是如何前进的？
浏览 2提问于2022-04-27得票数 1
1回答
1 subgoal
a, b : Tipe
H : TApp a b = a
______________________________________(1/1)
False (其中TApp是一个构造函数) 在Idris中，可以用\Refl => impossible来证明这一点，但我还没有设法在Coq中为它编写任何证明。 有没有简单的方法来证明这一点？
浏览 16提问于2019-04-01得票数 1
回答已采纳
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
回答已采纳
1回答
我知道Coq允许定义相互递归的归纳类型。但是有没有一种方法可以用Coq编写递归定义呢？
例如，我想将一个定义写为：
Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).
上述定义中的重要部分是myDefinition B，它在另一个参数上递归调用相同的定义。在Coq中可以这样做吗？
浏览 5提问于2020-11-04得票数 1
我试图在Isabelle/HOL中形式化业务规则，但是业务规则涉及一些变量的值的更改，比如if x=5 => x=6。=>不是通常的含义，因为x是一个世界中的5(解释、语义域)，在执行规则之后x是6，并且它已经是一个不同的世界(不同的解释、赋值函数、语义域)。因此，从技术上讲，is x=5 => x=6不是一阶逻辑的公式，也不是伊莎贝尔/霍尔的高阶逻辑公式。更有可能的是，它是动态/动作逻辑[rule1](x=5)=(x=6)中的公式(定义了当rule1应用于某些世界的公式时，在另一个世界中产生真实的公式(动态/动作逻辑本质上是一种模态逻辑，这里可以应用克里普克/可能的世界语义
浏览 3提问于2020-07-03得票数 0
回答已采纳
在Coq我有
Definition f (s:Unit) : tt=tt := match s with tt => idpath end.
Definition g (p:tt=tt) : Unit := match p with idpath => tt end.
我想证明forall (p:tt=tt), (f o g) p = p。
我想使用HoTT书中1.12.1中描述的路径归纳来完成它。
显然，对于p是idpath的情况，我们可以证明
assert( (f o g) idpath = idpath).
simpl.
reflexivity.
但是，如何使用Coq中的路径
浏览 1提问于2017-11-16得票数 0
回答已采纳
我从Coq开始，并试图将正式化。我在引理4.13：
Lemma preservation : forall (Sigma : prog_sig) (Gamma : context) (p : program)
(s : stack) (h h' : heap) (e : expr) (c : type0) (v : val),
(* 4.1 *) has_type Sigma Gamma e c ->
(* 4.2 *) eval p s h e v h' ->
(* 4.3 *) mem_consistant_stack h s Gamma -&g
浏览 0提问于2017-10-11得票数 0
2回答
在coq中使用哪个向量库？
、、、、
我想知道，在coq中是否有一个常用的向量库，即按其类型的长度索引的列表。
有些教程引用了Bvector，但是当我试图导入它时却找不到它。
有Coq.Vectors.Vectordef，但是定义的类型是t，这让我觉得它是为内部使用的。
对于那些不想使用自己的库的人来说，什么是最好的或最常见的做法？标准库中的向量我错了吗？还是我又错过了另一个自由战士？还是人们只是使用列表，并与其长度的证据一起使用？
浏览 10提问于2017-02-17得票数 6
回答已采纳
2回答
我试图证明在一个术语上应用空代换等于给定的术语。代码如下：
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Arith.EqNat.
Require Import Recdef.
Require Import Omega.
Import ListNotations.
Set Implicit Arguments.
Inductive Term : Type :=
| Var : nat -> Term
| Fun : string ->
浏览 26提问于2017-08-31得票数 2
回答已采纳
我正在用Coq开发一个谷歌库。到目前为止，这个项目进行得很顺利。然而，我有一个问题:我能在Coq中得到宇宙的继承者吗？
我可以通过lsuc在Agda中得到宇宙的继承者。Coq似乎是唯一的运算符max(_,_)。通过Print命令，我可以看到类似于Type@{(Top.9)+1}的东西，其中包括_+1，但是我不能使用这个符号。
浏览 4提问于2020-04-02得票数 2
回答已采纳
2回答
什么是归纳谓词？
、、
你如何解释归纳谓词？它们是用来干什么的？他们背后的理论是什么？它们只存在于依赖型系统中，还是在其他系统中？它们在某种程度上与GADT有关吗？在Coq中，为什么默认情况下它们是真的？
这是Coq的一个例子：
Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))
你将如何使用这个定义？这是一种数据类型还是一个命题？
浏览 7提问于2014-04-11得票数 5
回答已采纳
1回答
我试图用Coq编写一个程序来解析一个相对简单的上下文无关语法(一种括号)，而我的一般算法是解析器可能返回字符串的其余部分。例如，解析"++]>><<"应该返回CBTerminated [Incr Incr] ">><<"，然后，假设解析"++>><<“的解析器能够获取">><<”并继续进行。
所以很明显，字符串较小，但令人信服的Coq则是另一回事。它给了我错误
parseHelper的递归定义是不正确的...。递归调用parseHelper的主体参数
浏览 4提问于2016-05-26得票数 5
回答已采纳
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回答
我想在Coq中实现如下代码：
Inductive IT :=
| c1 : IT
| c2 (x:IT) (H:
match x as x return Prop with
| c1 => True
| c2 y => False
end): IT.
但是不可能匹配未定义的类型。如何克服这一障碍？
(在使用term之前，我需要检查它的一些属性。例如，目的-在构造更大的公式之前检查子公式的正确性。)
浏览 13提问于2018-08-24得票数 1
回答已采纳
我正致力于在Coq中正式化，但是对于具有非均匀类型参数的归纳数据类型，我很难通过归纳法来证明。
让我简单介绍一下我正在处理的数据类型。在Haskell中，我们将自由选择函子编码为GADT：
data Select f a where
Pure :: a -> Select f a
Select :: Select f (Either a b) -> f (a -> b) -> Select f b
这里的关键是第二个数据构造函数中的存在类型变量b。
我们可以将这个定义转换为Coq：
Inductive Select (F : Type -> T
浏览 0提问于2019-07-08得票数 5
回答已采纳
3回答
我正在使用Coq Proof Assistant实现一个(小型)编程语言的模型(扩展Bruno De Fraine，Erik Ernst，Mario Südholt的Featherweight Java实现)。在使用induction策略时，不断出现的一件事是如何保留类型构造函数中包装的信息。
我有一个子类型属性，实现为
Inductive sub_type : typ -> typ -> Prop :=
| st_refl : forall t, sub_type t t
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub
浏览 2提问于2010-12-23得票数 16
回答已采纳
1回答
我希望使用这些符号来表示谓词测试，如下所示：
Variable A B : Type.
Inductive test : A -> B -> A -> B -> Prop :=
| test1 : forall a1 a2 b1 b2,
a1 \ b1 || a2 \ b2
where "c1 '\' st '||' c2 '\' st'" := (test c1 st c2 st')
.
但是，Coq有一个错误：
为什么这个表示法在Coq中不能被接受？
浏览 0提问于2018-02-02得票数 2
回答已采纳
1回答
我定义了一个嵌套归纳数据类型，并为它定义了一个自定义归纳原则。然而，来自我正在使用的库的自动化策略(具体地说，用于de Bruijn索引的DBLib )期望归纳是基于通常的归纳原理的。既然我从来没有打算使用最初生成的归纳原理，那么有没有办法替代自动生成的原理呢？或者，如果没有，有没有办法暂时关闭这种自动生成？
浏览 10提问于2018-08-06得票数 2
回答已采纳
在Coq中，可以归纳地定义自然数如下：
Inductive nat :=
| zero : nat
| succ : nat -> nat.
我想知道是否有可能以类似的方式归纳地定义整数？我可以这样做
Inductive int :=
| zero : int
| succ : int -> int
| pred : int -> int.
但是我想在int的定义中断言succ(pred x) = x和pred(succ x) = x，我不知道如何做到这一点。
浏览 2提问于2021-02-16得票数 0
回答已采纳
在纸上推理的时候，我经常用归纳的方式对某些列表的长度进行论证。我想用Coq将这些参数正规化，但似乎没有任何方法可以对列表的长度进行归纳。
我应该如何进行这样的归纳呢？
更具体地说，我试图证明。在理论上，我通过对w长度的归纳法证明了这一点。我的目标是在Coq中把这个证明正式化。
浏览 7提问于2017-08-25得票数 7
回答已采纳
我想证明一些关于自然数不包括0的东西。因此，我对属性P的基本情况是P1而不是P0。 我正在考虑在goal中使用n >= 0作为假设，但是在Coq中有其他方法可以做到这一点吗？
浏览 19提问于2019-04-30得票数 0
回答已采纳
3回答
我想知道是否有办法在Coq定理的证明过程中引入一个全新的变量？
对于完整的示例，请考虑关于列表长度均匀度的以下属性。
Inductive ev_list {X:Type}: list X -> Prop :=
| el_nil : ev_list []
| el_cc : forall x y l, ev_list l -> ev_list (x :: y :: l).
现在，我想证明，对于任何列表l，如果它的length是偶数，那么ev_list l保持：
Lemma ev_length__ev_list': forall X (l : list X), ev
浏览 3提问于2015-10-08得票数 4
回答已采纳
1回答
是否有任何函数/命令来获取/检查一个自由变量(例如n:U )是否存在于一个术语/表达式e中，使用Coq？请分享。
例如，我想在Coq中声明这个"n不出现在e的自由名称中“。
谢谢,
威拉亚特
浏览 6提问于2012-07-16得票数 1
1回答
我正在尝试使用Omega在Coq中进行证明。我花了很多时间在上面，但什么也没想到。我不得不说，我是Coq的新手，所以我对这种语言并不自在，也没有太多的经验。但我正在努力。
下面是我要证明的代码：
Require Import Arith Omega.
Fixpoint div2 (n : nat) :=
match n with
S (S p) => S (div2 p)
| _ => 0
end.
Fixpoint mod2 (n : nat) :=
match n with
S (S p) => mod2 p
| x => x
end.
浏览 0提问于2012-12-04得票数 3
1回答
我正在努力实施以下措施：
[]()
[]()
使用诱因，t取决于e，反之亦然。我如何在Coq中实现它？当我还没有定义e时，我不能使用它。
浏览 1提问于2020-06-30得票数 0
回答已采纳
我有一个归纳定义--在计算之后--打印警告“忽略递归调用”。这个定义似乎运作得很好。不过，我仍然很好奇，为何要发出这个警告。下面是一个很小的例子。
Inductive testor :=
| Constr1 : list testor -> testor
| Constr2 : testor -> testor.
我认为罪魁祸首是第一个构造函数中的list testor。另一方面，如果没有第二个构造函数，则不会给出警告。
Q：为什么发出警告？这是否意味着对归纳定义施加限制？
我用的是Coq 8.5。
浏览 6提问于2016-06-02得票数 3
回答已采纳
1回答
我在Coq中做了一个练习，试图证明如果一个列表等于它的相反，它是一个回文。下面是我如何定义回文的方法：
Inductive pal {X : Type} : list X -> Prop :=
| emptypal : pal []
| singlpal : forall x, pal [x]
| inducpal : forall x l, pal l -> pal (x :: l ++ [x]).
下面是定理：
Theorem palindrome3 : forall {X : Type} (l : list X),
l = rev l -> pal l.
浏览 4提问于2017-03-25得票数 2
回答已采纳
我试图定义一个新的表示法范围，并在Coq中添加表示法。我正在遵循Coq手册()中这个页面的指导。
我定义了我的新范围
Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.
稍后，我想将"*“作为infix操作符添加到作用域中。我做这件事
Infix "*" := concat (at level 40 , left associativity) : myHoTT_scope.
其中，concat是一个已经定义的函数。Coq接受所有这些。它不会引发错误或警告。但是，如果我跑
Locate "
浏览 13提问于2022-01-29得票数 1
回答已采纳
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
回答已采纳
我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。
Inductive True2 : Prop :=
| One : True2
| Two : True2.
Lemma True_has_one : forall (t0 t1 : True), t0 = t1.
Proof.
intros.
destruct t0. destruct t1.
reflexivity.
Qed.
Lemma not_True2_has_one : (forall (t0 t
浏览 0提问于2014-10-26得票数 8
回答已采纳
考虑以下代码：
Require Import FMapAVL.
Require Import Coq.Structures.OrderedTypeEx.
Module NatMap := FMapAVL.Make(Nat_as_OT).
Inductive ttree (K : Type) (V : Type) :=
| tleaf : ttree K V
| tnode : ttree K V -> K -> V -> ttree K V -> nat -> ttree K V.
Inductive test :=
| test1 : test
| tes
浏览 0提问于2018-04-15得票数 3
回答已采纳
1回答
我试图用一个构造函数定义一个数据类型，该构造函数接受一个列表，并包含有关这个列表的命题。
这样做很好：
Require Import Coq.Lists.List.
Import ListNotations.
Inductive Foo := MkFoo : list Foo -> Foo.
这也是如此：
Inductive Foo := MkFoo : forall (l : list Foo), Foo.
但这是失败的
Inductive Foo := MkFoo : forall (l : list Foo), l <> [] -> Foo.
使用
在&
浏览 0提问于2018-05-07得票数 2
回答已采纳
Coq标准库有两个类模块的子集，一个固定在Coq.Classes.RelationClasses中，另一个固定在Coq.Classes.CRelationClasses中。后者似乎是最近才添加的(2012)。 我肯定遗漏了一些明显的东西，因为它们看起来都很像我。 它们存在的原因是什么？
浏览 11提问于2019-06-03得票数 1
回答已采纳
1回答
我注意到Coq对支持和类型的平等性综合了不同的归纳原则。有人对此有什么解释吗？
平等被定义为
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
相关的归纳原则有以下几种类型：
eq_ind
: forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P y
现在，让我们定义一个eq的Type吊坠：
Inductive eqT {A:Type}(x:A):A->Type:= eqT_refl:
浏览 4提问于2016-09-25得票数 5
回答已采纳
有时我会编写基于on概念的代码，比如类和接口。例如，一个学生对象有两个nat编号，一个是他的学生号，另一个是他的GPA。
public class Student {
// The private instance variables
private int studentNumber;
private int GPA;
}
有没有办法在Coq中编码这些概念？感谢您的指导。
浏览 10提问于2018-02-11得票数 1
回答已采纳
2回答
我对Coq非常陌生，但是对于我的项目，我必须使用Coq中的联合查找数据结构。Coq中是否有联合查找(不相交集)数据结构的任何实现？
如果没有，有人能提供一个实现或一些想法吗？不一定要很有效率。(不需要进行路径压缩或所有花哨的优化)我只需要一个可以容纳任意数据类型(或者nat (如果太难)并执行：、union、和find )的数据结构。
提前感谢
浏览 5提问于2021-03-14得票数 3
( 1)我认为在不进行模式匹配的情况下，可以使用归纳类型。(仅使用_rec、_rect、_ind )。它是不透明的，复杂的，但可能的。( 2)是否有可能使用具有模式匹配的共进类型？
从共归纳型到同归纳型构造子域的结合都存在着一个函数。Coq是否显式地生成它？如果是，如何重写“hd”？
Section stream.
Variable A : Type.
CoInductive stream : Type :=
| Cons : A -> stream -> stream.
End stream.
Definition hd A (s : stream A) : A
浏览 2提问于2016-11-25得票数 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
回答已采纳
我正在从软件基金会提供的资源中学习coq。在证明鸽子洞原理的过程中，我试图定义一个函数，从列表中提取子序列，这样里面就没有重复的元素。以下是我的定义：
Fixpoint norepeat_subseq {X : Type} (l : list X) : list X :=
match l with
| [] => []
| n :: t => match (In n t) with
| False => n :: norepeat_subseq t
| _ => norepeat_subseq t
浏览 8提问于2022-11-25得票数 0
1回答
我正在研究Coq上的排列，定义如下：
Definition Tperm := list (nat* nat).
我有一个Tperm -> nat -> nat类型的act函数，它返回通过排列传递的自然参数的图像。我还有一个Tperm -> list(nat)类型的atoms函数，它返回由排列修改的所有自然数。
所以现在，我必须证明这个引理：Lemma act_atoms: forall pi a, ~act(pi)(a) = a -> In a (atoms(pi)).
我已经在pi上通过归纳开始了证明，但在证明了第一个子目标后被卡住了。任何帮助都将不胜感激。下面是动作
浏览 2提问于2016-11-05得票数 1
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
