如何证明Coq中的n+S=S (n + m)
在Coq中，我们可以使用归纳法来证明等式n + S m = S (n + m)，其中n和m是自然数，S表示后继函数。
首先，我们需要定义自然数的加法操作。在Coq中，自然数是通过归纳定义的，其中0是自然数的基础，而后继函数S将一个自然数映射到下一个自然数。
接下来，我们可以使用归纳法来证明等式。归纳法是一种证明数学命题的常用方法，它分为两个步骤：基础步骤和归纳步骤。
基础步骤是证明等式对于基础情况成立的步骤。在这个例子中，我们需要证明等式对于n = 0成立，即0 + S m = S (0 + m)。根据加法的定义，0 + S m等于S m，而S (0 + m)等于S m，因此基础步骤成立。
归纳步骤是证明等式对于归纳情况成立的步骤。在这个例子中，我们假设等式对于n成立，即n + S m = S (n + m)，然后证明等式对于n的后继情况也成立，即S n + S m = S (S n + m)。
根据加法的定义，S n + S m等于S (n + S m)，而S (S n + m)等于S (S (n + m))。根据归纳假设，n + S m = S (n + m)，因此S (n + S m)等于S (S (n + m))。因此，归纳步骤成立。
综上所述，根据基础步骤和归纳步骤，我们证明了等式n + S m = S (n + m)在Coq中成立。
在腾讯云的相关产品中，可以使用腾讯云的云服务器（CVM）来搭建Coq的开发环境。腾讯云的云服务器提供了强大的计算能力和稳定的网络环境，适合进行Coq的开发和运行。您可以通过以下链接了解腾讯云云服务器的详细信息：https://cloud.tencent.com/product/cvm
相关·内容
2回答
我是Coq的初学者。 虽然计算机为我验证了证明是令人满意的，但对于人类来说，满足Coq的证明是出了名的难以阅读。下面是一个简单的例子，假设你没有看到任何评论： Theorem add_comm : forall n m : nat,
n + m = m + n.
Proof.
intros n m.
induction m as [|m Hm].
- (* n + 0 = 0 + n *)
simpl. (* n + 0 = n *)
浏览 27提问于2021-09-06得票数 3
Theorem mult_comm : forall m n : nat,
m * n = n * m.
Proof.
intros.
induction n.
- simpl. rewrite (mult_0_r m). reflexivity.
- simpl.
rewrite <- IHn.
induction m.
simpl. reflexivity.
simpl. 以上内容来自软件基金会的第二章。 1 subgoal
m, n : nat
IHn : S m * n = n * S m
IHm : m * n = n * m -> m *
浏览 15提问于2019-04-09得票数 1
回答已采纳
1回答
我正在尝试在Coq中定义一个名为interval的函数，该函数给定两个自然数，计算这两个自然数之间的所有自然数的列表。然而，我的定义不是原语递归的。下面是我的代码：
Require Coq.Program.Tactics.
Require Coq.Program.Wf.
Inductive bool : Type :=
| true : bool
| false : bool.
Fixpoint leq_nat (m:nat) (n:nat) : bool :=
match m with
| 0 => true
| S x => match n with
浏览 1提问于2015-11-13得票数 2
我是Coq的新手。我一直在通过Pierce's Logical Foundations工作。我走出了文本的范围，进入了实数，并发现自己一无所知。我想我可以证明一些简单的东西，所以我写了一些计算利息的公式。现在我想证明我的转换是正确地写在我的定理中。 我不知道如何继续，需要提示和指导！ From Coq Require Import Reals.Reals.
Definition simple_compound (A r n m : R) : R :=
A * (Rpower (1 + r / m) (m * n)).
Definition continuous_compou
浏览 20提问于2020-07-16得票数 0
回答已采纳
1回答
下面的U归纳定义被Coq接受，因为它可以看到U在M.T U -> U中的出现次数是严格为正的。
Module M.
Definition T (A : Type) : Type := unit -> A.
End M.
Module N.
Inductive U : Type :=
| c : M.T U -> U.
End N.
另一方面，Coq不接受以下U的归纳定义，因为根据M.T的定义，它可能具有非严格正的出现。
Module Type S.
Parameter T : Type -> Type.
End S.
Module N (M : S).
浏览 3提问于2018-06-30得票数 3
1回答
我有点搞不懂Coq 中关于自然数定义的后继函数的内射性是否是公理？，根据，它是公理(7)。当我查看手册页面时，我会看到以下内容：
定义eq_add_S n m (H: S=S)：n=m := f_equal pred H.
提示立即eq_add_S: core。
它看起来像一个公理(?)但令我困惑的是，在这一页的顶部写着：
它描述了关于自然数的各种引理和定理，包括Peano的算术公理(在Coq中，这些定理是可证明的)。
这句话有点模棱两可不是吗？
浏览 3提问于2019-01-16得票数 5
回答已采纳
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
我试图使用Coq的listSet创建一个set of nats。但是，我在将成员添加到集合时遇到了问题。
这是我正在运行的代码。
Require Import ListSet Nat.
Axiom eq_dec : forall x y : nat, {x = y} + {x <> y}.
Compute (set_add eq_dec 0 (set_add eq_dec 0 nil)).
运行时，输出为
=如果eq_dec为0 0，则(0 :：0)%list (0 :：0:0)%list: set
现在，我知道了为什么要在输出中获得if-else语句。这是因为我只告诉
浏览 3提问于2017-09-07得票数 1
回答已采纳
2回答
我试图在Coq中证明以下引理：
Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.
这看起来很简单，但我不知道如何完成这个证明。有谁能帮帮我吗？
谢谢。
浏览 4提问于2015-12-02得票数 2
1回答
我现在正在学习Coq，在一个更大的证明中，我被下面的子证明所困扰：
Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.
或者，一旦展开：
Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → S n ≤ m.
这里，"n≤m“的归纳定义如下：
Inductive le : nat → nat → Prop :=
| le_n : ∀ n : nat, le n n
| le_S : ∀ n m : nat, (le n m) → (le n (S m)).
我没有走多远，但我的尝试
浏览 0提问于2019-08-30得票数 2
回答已采纳
1回答
我正在努力学习coq，所以请假设我对此一无所知。
如果在coq中有一个引理开始
forall n m:nat, n>=1 -> m>=1 ...
我想在n上进行归纳，我如何在1开始归纳？目前我使用的是“归纳n”。战术它从零开始，这使得基本陈述错误，这使得它很难进行。
有什么暗示吗？
浏览 2提问于2014-11-29得票数 5
回答已采纳
1回答
Coq中递推函数的扩展
、、、
背景
据我所知，Iota约简用于减少/扩展递归函数。例如，给定简单递归函数(对自然数的阶乘)的以下应用：
((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2)
Iota约简扩展了递归调用，有效地迭代了递归函数一次：
Eval lazy iota in ((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2).
= (fun n:nat =>
match n with
浏览 0提问于2015-04-23得票数 6
回答已采纳
2回答
我正在写一篇关于使用Coq系统的快速排序算法的程序验证的论文。我已经在Coq中定义了一个快速排序，但我的主管和我自己并不是很习惯使用策略来编写实际的证明。有没有人能帮上忙呢？以下是我们到目前为止得出的结论：
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
Check (S (S (S (S O)))).
Definition isZero (n:nat) : bool :=
match n with
O => true
|S p => false
end.
Inductive Lis
浏览 1提问于2012-04-08得票数 2
在Coq中，我可以为长度为n的列表定义教堂编码： Definition listn (A : Type) : nat -> Type :=
fun m => forall (X : nat -> Type), X 0 -> (forall m, A -> X m -> X (S m)) -> X m.
Definition niln (A : Type) : listn A 0 :=
fun X n c => n.
Definition consn (A : Type) (m : nat) (a : A) (l : listn A m) :
浏览 23提问于2019-03-10得票数 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
关于如何在Coq中重新排列术语，我有一个一般性的问题。例如，如果我们有一个术语m + p + n + p，人类可以快速地将这些术语重新排列为类似于m + n + p + p (隐式使用plus_comm和plus_assoc)的术语。我们如何在Coq中有效地做到这一点？
举个愚蠢的例子，
Require Import Coq.Arith.Plus.
Require Import Coq.Setoids.Setoid.
Theorem plus_comm_test: forall n m p: nat,
m + p + (n + p) = m + n + 2 * p.
Proof. int
浏览 5提问于2015-10-07得票数 1
回答已采纳
给定过程even，我想证明所有自然数n的even (n * (S n)) = true。
使用归纳，这很容易被认为是true的情况下的n = 0。然而，(S n) * (S (S n))的情况很难简化。
我考虑过证明even (m * n) = even m /\ even n的引理，但这似乎并不容易。
而且，很容易看出，如果even n = true当且仅当。even (S n) = false。
Fixpoint even (n: nat) : bool :=
match n with
| O => true
| 1 => false
| S (S n'
浏览 9提问于2016-11-24得票数 3
回答已采纳
我想证明莱玛·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
回答已采纳
2回答
我试图用Coq编写一个计算自然除法的函数，而且我在定义它时遇到了一些困难，因为它不是结构递归。
我的代码是：
Inductive N : Set :=
| O : N
| S : N -> N.
Inductive Bool : Set :=
| True : Bool
| False : Bool.
Fixpoint sum (m :N) (n : N) : N :=
match m with
| O => n
| S x => S ( sum x n)
end.
Notation "m + n" := (sum m n) (a
浏览 3提问于2015-10-23得票数 4
回答已采纳
1回答
为了理解一般的递归Function定义是如何工作的，以及它们如何符合Coq的结构递归约束，我尝试在Peano自然数上重新实现它。我想定义递归nat -> nat函数，它可以使用任何以前的值，而不仅仅是前导函数。下面是我所做的：
Definition nat_strong_induction_set
(* erased at extraction, type specification *)
(P : nat -> Set)
(* The strong induction step. To build
浏览 7提问于2018-08-14得票数 3
回答已采纳
我在找关于nats的这个引理。我希望它已经存在于一个Coq库中，所以我不需要证明它。
forall m n : nat, (S m < n)%nat -> (n - (S m) < n)%nat
如果有图书馆，请指给我看。谢谢!
浏览 0提问于2019-04-06得票数 0
回答已采纳
1回答
我想证明的是：Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.
+是plus的表示法，定义为
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O ⇒ m
| S n' ⇒ S (plus n' m)
end.
在Agda中，我们可以做cong (n + _)来使用n + m = n + p对于任意n m。
Coq的内置策略injection和congruence看起来都很有希望，但它们只适用于构造函数。
浏览 1提问于2020-01-11得票数 0
回答已采纳
我对add的定义如下：
Fixpoint add n m :=
match n with
| 0 => m
| S p => add p (S m)
end.
在后面的文件中，我试图证明以下目标：add (S n) 0 = S n
我调用simpl命令，期望它减少
add (S n) 0到add n (S 0)。
相反，它减少了
add (S n) 0到add n 1
我怀疑simpl命令只要能够执行就会执行多个步骤。
我的问题：是否有一个命令可以使一个步骤减少，减少
add (S n) 0 = S n
至
add n (S 0) = S n
浏览 4提问于2020-06-12得票数 0
回答已采纳
如何在Coq中证明forall n m : nat, (n <? m) = false -> m <= n？
到目前为止，我已经把这个结论转化为~ n < m，由apply Nat.nlt_ge使用。
执行SearchAbout ltb会产生ltb_lt: forall n m : nat, (n <? m) = true <-> n < m，但我不知道如何应用它，因为它只处理(n <? m) = true，而不是(n <? m) = false。
浏览 0提问于2015-01-25得票数 1
回答已采纳
3回答
模上的协q归纳
、、
我是新来的coq，我真的很难运用归纳。只要我能使用图书馆的定理，或者像欧米茄这样的策略，所有这些都是“没有问题”。但一旦这些不起作用，我就被困住了。
准确地说，现在我试图证明
Lemma mod_diff : forall n m : nat, n>=m /\ m <> 0 -> (n - m) mod m = n mod m.
情况n=0，我已经有了。
Proof.
intros. destruct H as [H1 H2 ]. induction n.
rewrite Nat.mod_0_l by omega. rewrite Nat.mod_0
浏览 5提问于2015-03-21得票数 5
回答已采纳
我很难理解如何在证明中使用我在Coq中定义的一些东西。我有这段定义和功能：
Inductive string : Set :=
| E : string
| s : nat -> string -> string.
Inductive deduce : Set :=
|de : string -> string -> deduce.
Infix "|=" := de.
Inductive Rules : deduce -> Prop :=
| compress : forall (n : nat) (A : string),
浏览 6提问于2016-06-06得票数 3
回答已采纳
我无法用coq的策略来证明简单的逻辑max a b <= a+b。我该怎么解决这个问题？下面是我一直在写的代码。为了简单起见，本文证明了s_le_n，但这里没有提到它。
Theorem s_le_n: forall (a b: nat), a <= b -> S a <= S b.
Proof. Admitted.
Theorem max_sum: forall (a b: nat), max a b <= a + b.
Proof.
intros.
induction a.
- simpl. reflexivity.
- rewrite plus_Sn_m
浏览 2提问于2017-09-25得票数 1
回答已采纳
2回答
Coq的标准库提供Peano自然数和加法：
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
Fixpoint add n m :=
match n with
| 0 => m
| S p => S (add p m)
end.
我很好奇我是否更改了加法的fix_definition，比如
Fixpoint add n m :=
match n with
| 0 => m
| S p => add p (S m)
end.
新的加法是否等同于旧的加法？我试图通过证明for
浏览 11提问于2022-01-23得票数 1
回答已采纳
1回答
我试图证明一个关于以下功能的命题：
Program Fixpoint division (m:nat) (n:nat) {measure m} : nat :=
match lt_nat 0 n with
| false => 0
| true => match leq_nat n m with
| false => 0
| true => S (division (menos m n) n)
end
end.
menos是自然减法。
我在试图证明一些与组织有关的事实。我写下了一个非正式的证明，如果我首先考虑lt_nat 0 n中的案
浏览 1提问于2015-11-22得票数 4
回答已采纳
由于coq中的证明是简单的高度复杂的函数，可以通过各种方式中的任何一种来构建，因此似乎有必要为每个既不涉及先前证明的定理也不涉及assert语句的定理提供coq证明。
例如，在没有任何引理的情况下，证明自然数加法的交换性是很简单的，即使有引理可以让它变得更简单：
Theorem plus_comm' :
forall n m : nat, n + m = m + n.
Proof.
induction n.
intro m. simpl. induction m.
reflexivity.
simpl. rewrite <- IHm. re
浏览 1提问于2016-03-16得票数 2
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
回答已采纳
我的问题是:为什么‘直觉’在我的例子中起作用？
我想证明
Lemma eqb_false : forall n m : nat, eqb n m = false -> n <> m.
在最后一步，我可以看到
n : nat
IHn : forall m : nat, (n =? m) = false -> n <> m
m : nat
IHm : (S n =? m) = false -> S n <> m
============================
(n =? m) = false -> S n <> S
浏览 4提问于2015-05-19得票数 5
回答已采纳
所以我一直在学习使用Coq，到目前为止，我一直在使用我自己定义的自然类型，所以我不是100%清楚使用默认的自然类型可以做什么。然而，程序固定点需要它，并且我最终需要利用(对人类来说显而易见的)事实，即(n > m) -> (S >S)。我似乎不能证明这一点-我运行类似这样的东西 Theorem gt_triv : forall n m : nat, n > m -> (S n) > (S m).
intros. 然后我有一个假设n > m和一个目标证明(S n) > (S m)，但我似乎不能对它做任何事情(除了将它展开到S (S m) <
浏览 24提问于2020-09-30得票数 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
回答已采纳
在Coq标准库中，有一个名为comparison的枚举类型，它有三个元素Eq,Lt,Gt。这用于在ZArith中定义小于或小于等于的操作符：m < n定义为m ?= n = Lt，m <= n定义为m ?= n <> Gt。借助Hedberg定理(标准库中的UIP_dec)，我可以证明<是证明-无关的，但是当涉及到<=时，我遇到了一些问题，因为它是负面定义的。我觉得这特别令人讨厌，因为如果<=是用国际海事组织的更自然的方式(m ?= n = Lt \/ m ?= n = Eq)来定义的，那么我就可以证明证据--无关紧要。
上下文：--我正在使用一些以前
浏览 1提问于2018-04-11得票数 3
大约在5到8年前(可能是6到7年)，我用Coq写了一篇完整的泡泡类型的形式化文章。最早证实的一个词是标题中的那个，我称之为"sub_succ_r“(或者它可能是标准名称？)：
forall n m : nat, (n - (S m))%nat = pred(n - m)
那时候，这是那个引理的一个非常简单的证明：
intros n m.
induction n m using n_double_ind.
simpl.
auto.
apply sub_0_r.
Qed.
"sub__r“是断言
forall n : nat, (n - 0)%nat = n
现在，同样熟悉现代Co
浏览 0提问于2020-03-22得票数 1
回答已采纳
我如何证明这个引理：
Lemma even_plus_split n m :
even (n + m) -> even n /\ even m \/ odd n /\ odd m.
以下是唯一可以使用的库和定义：
Require Import Arith.
Require Import Coq.omega.Omega.
Definition even (n: nat) := exists k, n = 2 * k.
Definition odd (n: nat) := exists k, n = 2 * k + 1.
我是Coq的新手，对此感到困惑。你能给我一个解决方案
浏览 3提问于2018-05-02得票数 0
2回答
我在试验Coq的提取机制。我在Coq中为素数编写了一个简单的谓词，如下所示：
(***********)
(* IMPORTS *)
(***********)
Require Import Coq.Arith.PeanoNat.
(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
match m,n with
| 0,_ => false
| 1,_ => false
| _,0 => false
| _,1
浏览 0提问于2019-03-18得票数 6
回答已采纳
我试图在Agda中演示Coq提取机制和MAlonzo编译器在代码生成方面的区别。我在Agda中提出了一个简单的例子：
data Nat : Set where
zero : Nat
succ : Nat → Nat
data List (A : Set) : Set where
nil : List A
cons : A → List A → List A
length : ∀ {A} → List A → Nat
length nil = zero
length (cons _ xs) = succ (length xs)
data Fin : Nat → Set wh
浏览 2提问于2014-05-20得票数 1
回答已采纳
我试图编写一个函数，它接受自然数的列表，并将其中不同元素的数量作为输出返回。例如，如果我有列表1,2,2,4,1，函数DifElem应该输出"3“。我尝试过很多事情，最近得到的是：
Fixpoint DifElem (l : list nat) : nat :=
match l with
| [] => 0
| m::tm =>
let n := listWidth tm in
if (~ In m tm) then S n else n
end.
我的逻辑是这样的:如果m不在列表的尾部，那么在计数器中添加一个。如果是的话，不要添加到计数器中
浏览 0提问于2016-04-21得票数 7
回答已采纳
1回答
我试图在Coq中反转一个向量。我的执行情况如下：
Fixpoint vappend {T : Type} {n m} (v1 : vect T n) (v2 : vect T m)
: vect T (plus n m) :=
match v1 in vect _ n return vect T (plus n m) with
| vnil => v2
| x ::: v1' => x ::: (vappend v1' v2)
end.
Theorem plus_n_S : forall n m, plus n (S m) = S (plus
浏览 7提问于2021-12-09得票数 4
回答已采纳
我是Coq的新手。我一直在通过Pierce's Logical Foundations工作。我正在踏入一个新的领域。 我第一次尝试使用field策略。我在下面的定理中使用了它三次。两次失败，产生m <> 0%R，其中m是上下文中的一个术语。 我确信我只是无法理解正确的用法。有没有人能开导我一下？(我试过阅读this doc page，但没有获得太多理解！) From Coq Require Import Reals.Reals.
Require Import Field.
Definition simple_compound (A r n m : R) : R :=
浏览 14提问于2020-07-16得票数 0
回答已采纳
1回答
我是coq的新手，需要获取这个二叉树的叶子上的一个元素，并满足P Variable A : Set.
Variable P : A -> Prop.
Variable P_dec : forall x : A, {P x} + {~ P x}.
Inductive PTree : nat -> Set :=
| PLeafTrue : forall (n : nat) (a : A), P a -> PTree 1
| PLeafFalse : forall (n : nat), A -> PTree 0
| PNode : forall (n m
浏览 25提问于2021-01-14得票数 2
我试图在Coq中证明以下Python构造的相等性：for i, _ in enumerate(l, s)和for i in range(s, len(l) + s)
我对enumerate函数和range函数都做了递归定义，并提出了一些额外的定理来帮助我实现最初的目标，并成功地证明了它们。
但是，我被困在了中途的某个地方。我的最终目标是：[] = [s]，这显然是错误的。这就是为什么我尝试使用specialize nil_cons来使用discriminate的原因，但这并没有帮助：“找不到原始的等式。”
我肯定还有别的办法，我只是不明白。
这就是我到目前为止得到的：
Require I
浏览 6提问于2022-07-14得票数 0
回答已采纳
2回答
共归纳和依赖类型
、、
我正在尝试编写一个Coq函数，它接受一个Stream和一个谓词，并以list的形式返回该属性所针对的流的最长前缀。这就是我所拥有的：
Require Import List Streams.
Require Import Lt.
Import ListNotations.
Local Open Scope list_scope.
Section TakeWhile.
Context {A : Type} {P : Stream A -> Prop}.
Hypothesis decide_P : forall s : Stream A, {P s} + {~ P s}.
Progr
浏览 3提问于2013-07-15得票数 2
回答已采纳
1回答
下面是整数除以余数的Coq实现。当我将它提取到Haskell 时，一切都很好，。我将Coq版本与生成的Haskell版本进行了比较，并试图了解发生了什么。似乎rewrite 在这里被简单地删除了，而实际上指导这里提取的是induction、destruct、exists和specialize。在提取过程中是否有使用rewrite的场景？另外，有些变量名是保留的(如q0和m0'')，但其他变量名称更改(r0到h)是否有理由更改名称？下面是Coq代码，后面是提取的代码：
(***********)
(* IMPORTS *)
(***********)
Require Import
浏览 0提问于2019-04-28得票数 1
回答已采纳
2回答
我对Coq定理证明器很陌生。因此，我很可能已经错过了一些基本的东西，在阅读教程时。
在我提出我的问题之前，让我假设一些假设，并回顾一下我的想法。
Coq < Parameter Antecedent : Prop .
Coq < Parameter Consequent : Prop .
Coq < Conjecture Minor : Antecedent .
Coq < Conjecture Major : Antecedent -> Consequent .
有了这些假设，就可以应用Consequent模型:可以根据Minor前提和Major前提构造推断Ma
浏览 4提问于2014-05-06得票数 0
关于Coq (带有Init库)，一个非常基本的问题是:术语10是nat类型的，nat类型是归纳定义的：
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
Q1.，但"10“是S(S(...S(0)...))的”捷径“
Q2.有以下引理的最短(正式)证明吗？(不使用欧米茄)
Lemma gg : 3 <= 10.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_n.
Qed.
换句
浏览 2提问于2014-07-23得票数 2
回答已采纳
我想证明下面的引理。 Lemma AppendAndSplit {n m}(e:Euc n) (f:Euc m): # (e +++ f) = (e, f).
Proof.
induction e.
reflexivity.
remember (r:::e).
Admitted.
Lemma SplitRule {n m}(e:Euc (n+m)) : (fst (# e)) +++ (snd (# e)) = e.
Proof.
induction n.
reflexivity.
Admitted. #和+++是EucAppend和Split_Euc的符号。我能感觉到这一点，但我不知道如
浏览 13提问于2020-10-05得票数 0
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
