<=：如何证明对于所有n m，n <= m \/ m Coq n

文章/答案/技术大牛

发布

2回答

coq

如何证明定理le_total :对所有n m，n <= m\/m <= n.| le_S (n m : nat) (H : le n m) : le n (S m).Notation "n <= m" := (le n <em

浏览 29提问于2021-11-10得票数 1

1回答

如何证明(n，m: nat，n <？)m) =假-> m <= n( Coq )？

coq、theorem-proving

如何在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</e

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

回答已采纳

2回答

如何在Coq中证明(n = n) = (m = m)？

coq、coq-tactic

我对Coq中的证据和Prop等感到困惑。我们如何证明(n = n) = (m = m)？Theorem test: forall m n:nat, (n = n) = (m = m). Proof. intros. simpl.这只是一个例子，一般来说，如果可

浏览 2提问于2015-12-08得票数 3

回答已采纳

3回答

Coq:我如何证明对于所有的n m: nat，(n > m) -> (S >S)？

numbers、coq、proof

所以我一直在学习使用Coq，到目前为止，我一直在使用我自己定义的自然类型，所以我不是100%清楚使用默认的自然类型可以做什么。然而，程序固定点需要它，并且我最终需要利用(对人类来说显而易见的)事实，即(n > m) -> (S >S)。我似乎不能证明这一点-我运行类似这样的东西 Theorem gt_triv : forall n m : nat, n > m -> (S n) > (S m

浏览 24提问于2020-09-30得票数 0

回答已采纳

2回答

Coq中“如果m <= n那么max(m，n) = n”的证明

coq、proof

昨天我在这里问了一个关于Coq证明的问题，这个答案对我很有帮助，我能够独自解决许多练习，发现新的功能。今天我还有一个练习，那就是For all m, n, if m <= n then max(m,n) = n。我试着在我之后做自我介绍，但是我被困住了。任何帮助都将不胜感激！Fixpoint max (m n : Nat) : Nat :=

浏览 5提问于2022-10-15得票数 0

回答已采纳

1回答

证明在COQ中n<m+n或0<m

coq、proof、inequality

我试图用一个引理来证明一个更大的证明，但我找不到一种方法来证明这两件事中的一件。有人能帮帮我吗？以下是目前为止的证据： intros.

浏览 0提问于2018-07-01得票数 0

2回答

注释Coq证明

coq

我是Coq的初学者。虽然计算机为我验证了证明是令人满意的，但对于人类来说，满足Coq的证明是出了名的难以阅读。下面是一个简单的例子，假设你没有看到任何评论： Theorem add_comm : forall n m : nat,Proof.intros n m. induction m as [|<em

浏览 27提问于2021-09-06得票数 3

2回答

证明(prev n) <= m从n <= m开始

agda

n<=m : n <= m) -> (succ n) <= (succ m)lem-prev : {x y : Nat} -> x <= y -> (prev x) <= (prevy)lem-prev (s<=s t) = tlem-prev&#

浏览 3提问于2012-10-21得票数 4

回答已采纳

1回答

在Coq中定义区间函数

coq、proof

我正在尝试在Coq中定义一个名为interval的函数，该函数给定两个自然数，计算这两个自然数之间的所有自然数的列表。然而，我的定义不是原语递归的。我希望被要求证明forall m, n, true = m <= n -> S n - S m < S n - m m

浏览 1提问于2015-11-13得票数 2

1回答

我正在尝试创建一个(j : Nat) -> {auto p : So (j < n)} -> Fin n类型的Idris函数来将Nat转换为Fin n。为了让Z的用例能够工作(并输出FZ)，我试图证明0 < n的证明足以生成FZ : Fin n。但我不知道该怎么做。我愿意创建一个完全不同的函数，只要它能将Nat值转换为Fin n值(如果它们存在的话)。我的目标是拥有一些其他函数，可以将任何Nat转换为Mod n

浏览 4提问于2014-11-16得票数 2

1回答

为什么嵌套归纳策略也将归纳假设嵌套在lambda下？

coq

Theorem mult_comm : forall m n : nat,m, n : natIHm : m * n = n * m -> m * S n = <em

浏览 15提问于2019-04-09得票数 1

回答已采纳

1回答

如何证明Coq中的n+S=S (n + m)

induction、coqide

因此，我正在尝试使用“计算逻辑导论”脚本学习Coq，并给了我一个练习。证明了：“对于a，a+S=S (a + b)”。我得到了“nat_ind”的定义： (basis : p 0) foralln, p n := fix f n := match n return p

浏览 42提问于2020-05-11得票数 0

3回答

IndProp: ev_plus_plus

coq、logical-foundations

. *) even (n+m) -> even (n+p) -> even (m+p).even (m + p)Theorem ev_ev__ev : forall n m, even (n</e

浏览 1提问于2019-05-25得票数 0

回答已采纳

1回答

终止检查未能证明∃-偶数‘：∀{n :ℕ}→∃[m](2m≡n)→偶数n*

agda、termination、plfa

∃-even′ : ∀ {n : ℕ} → ∃[ m ] ( 2 * m ≡ n) → even n我已经把类型做好了。但是，对于以下函数，终止检查失败了：d

浏览 1提问于2021-04-17得票数 3

回答已采纳

2回答

证明L= {a^n ^m\ n>=m}是不规则语言

proof、pumping-lemma

有什么办法证明L= {a^n ^m\ n>=m}是一种不规则语言吗？

浏览 3提问于2020-04-16得票数 1

回答已采纳

1回答

回到5-8年后的Coq检验:如何证明(forall n，m: N，(n - (S ))= pred(n - m))？

coq

大约在5到8年前(可能是6到7年)，我用Coq写了一篇完整的泡泡类型的形式化文章。最早证实的一个词是标题中的那个，我称之为"sub_succ_r“(或者它可能是标准名称？)：那时候，这是那个引理的一个非常简单的证明：induction n m usi

浏览 0提问于2020-03-22得票数 1

回答已采纳

1回答

使用Coq来证明相对数之间的差异

coq

你如何证明：forall m n : Z, m < n -> m -n < O in Coq？非常感谢！

浏览 2提问于2012-11-01得票数 1

回答已采纳

4回答

对带有产品类型参数的谓词的归纳

coq、induction、coq-tactic

然后我就可以用归纳来证明一些虚拟的引理： foo n n' -> n = n'. intros.但是，对于带有产品类型参数的谓词： | Bar : forall n m, bar

浏览 4提问于2016-01-19得票数 2

回答已采纳

2回答

Coq中的有充分根据的递归

math、coq、proof、totality

我试图用Coq编写一个计算自然除法的函数，而且我在定义它时遇到了一些困难，因为它不是结构递归。Fixpoint sum (m :N) (n : N) : N := | O => nend.Fixpoint mult (m :N) (n : N) : N :

浏览 3提问于2015-10-23得票数 4

回答已采纳

1回答

如何证明`plus_le_compat_l :n m p，n <= m -> p+n <= p+m

coq、coq-tactic

定理如下： n <= m ->Theorem plus_le_compat_l : forall n m p, n <= <em

浏览 1提问于2021-10-04得票数 1

回答已采纳

点击加载更多